Documentation

Lean 4 Proof

theorem levelGeneralCurvature_pos
    {N : ℕ} (e : WeightedHierarchicalCESEconomy N) (n : Fin N)
    (hρ : e.ρ n < 1) (hJ : 2 ≤ e.J n)
    (hH : levelHerfindahl e n < 1) :
    0 < levelGeneralCurvature e n := by
  unfold levelGeneralCurvature
  exact gen_quadruple_K_pos hJ hρ (e.ha_pos n) (e.ha_sum n) hH

Dependency Graph

Location

thesis/CESProofs/Hierarchy/Defs.lean:349

Module Section

## Weighted Hierarchical CES Economy

In the same file