Documentation

Lean 4 Proof

theorem levelGeneralCurvature_le_standard
    {N : ℕ} (e : WeightedHierarchicalCESEconomy N) (n : Fin N)
    (hρ : e.ρ n < 1) (hJ : 2 ≤ e.J n) :
    levelGeneralCurvature e n ≤ levelStandardCurvature e n := by
  unfold levelGeneralCurvature levelStandardCurvature
  exact equalWeights_maximize_K hJ hρ (e.ha_pos n) (e.ha_sum n)

Dependency Graph

Used by

Location

thesis/CESProofs/Hierarchy/Defs.lean:358

Module Section

## Weighted Hierarchical CES Economy

In the same file