Documentation

Lean 4 Proof

theorem adoption_threshold {beta delta : ℝ}
    (_hbeta : 0 < beta) (hdelta : 0 < delta) :
    1 < adoptionR0 beta delta ↔ delta < beta := by
  unfold adoptionR0
  rw [one_lt_div hdelta]

Dependency Graph

Location

thesis/CESProofs/Applications/AITransition.lean:108

Module Section

Paper 6: Endogenous Decentralization and the AI Transition

In the same file