Documentation

Lean 4 Proof

theorem relaxation_rate_nonneg (e : NSectorEconomy N) (n : Fin N) :
    0 ≤ sectorRelaxRate e n := by
  simp only [sectorRelaxRate]
  apply mul_nonneg
  · apply mul_nonneg
    · exact le_of_lt (e.hℓ n)
    · exact abs_nonneg _
  · exact le_max_left 0 _

Dependency Graph

Location

thesis/CESProofs/Dynamics/Relaxation.lean:174

Module Section

Results 1-7: Relaxation on the CES Potential Landscape

In the same file