Documentation

Lean 4 Proof

theorem relaxation_rate_vanishes_at_Tstar (e : NSectorEconomy N) (n : Fin N)
    (hTeq : e.T n = sectorCriticalFriction e n) :
    sectorRelaxRate e n = 0 := by
  simp only [sectorRelaxRate, hTeq]
  have hTs : sectorCriticalFriction e n ≠ 0 := by
    intro h
    simp only [sectorCriticalFriction, criticalFriction] at h
    have hK : 0 < curvatureK (e.J n) (e.ρ n) := curvatureK_pos (e.hJ n) (e.hρ n)
    have hnum : 0 < 2 * (↑(e.J n) - 1) * (e.c n) ^ 2 * e.d_sq n := by
      apply mul_pos
      · apply mul_pos
        · apply mul_pos
          · linarith
          · have hJn := e.hJ n
            have : (1 : ℝ) < ↑(e.J n) := by exact_mod_cast (show 1 < e.J n by omega)
            linarith
        · exact sq_pos_of_pos (e.hc n)
      · exact e.hd n
    rw [div_eq_zero_iff] at h
    cases h with
    | inl h => linarith
    | inr h => linarith
  rw [div_self hTs, sub_self, max_eq_left (le_refl 0), mul_zero]

Dependency Graph

Location

thesis/CESProofs/Dynamics/Relaxation.lean:194

Module Section

Results 1-7: Relaxation on the CES Potential Landscape

In the same file