Documentation

Lean 4 Proof

theorem crisis_duration_decomposition (e : NSectorEconomy N)
    (hKeff : ∀ n, 0 < sectorEffectiveCurvature e n) :
    -- Total adjustment time ≤ sum of sector timescales
    -- Each 1/λ_n is well-defined since λ_n > 0
    ∀ n, 0 < 1 / sectorRelaxRate e n := by
  intro n
  exact div_pos one_pos (landscape_structure e n (hKeff n))

Dependency Graph

Location

thesis/CESProofs/Dynamics/Relaxation.lean:354

Module Section

Results 1-7: Relaxation on the CES Potential Landscape

In the same file