Documentation

Lean 4 Proof

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

Dependency Graph

Location

thesis/CESProofs/Hierarchy/KnockoutHierarchy.lean:68

Module Section

## Corollary 4b.2: Herfindahl Predicts Cascade Risk

In the same file