Documentation

Lean 4 Proof

theorem equal_weight_single_relaxation
    {N : ℕ} (e : WeightedNSectorEconomy N) (n : Fin N)
    (hρ : e.ρ n < 1) (hJ : 2 ≤ e.J n) :
    sectorGeneralCurvature e n ≤ sectorCurvature e.toNSectorEconomy n := by
  exact sectorGeneralCurvature_le_standard e n hρ hJ

Dependency Graph

Location

thesis/CESProofs/Dynamics/Relaxation.lean:389

Module Section

## Theorem 3b.1: General-Weight Relaxation Spectrum

In the same file