Documentation

Lean 4 Proof

theorem emergent_CES (J : ℕ) (F : AggFun J)
    (hcont : IsContinuousAgg J F)
    (hsymm : IsSymmetric J F)
    (hincr : IsStrictlyIncreasing J F)
    (hhom : IsHomogDegOne J F)
    (hsc : IsScaleConsistent J F) :
    IsPowerMean J F := by
  -- Step 1: Scale consistency is associativity.
  -- By the Kolmogorov-Nagumo theorem, F is quasi-arithmetic.
  have hqa : IsQuasiArithMean J F := kolmogorov_nagumo J F hcont hsymm hincr hsc
  -- Step 2: By Aczél's theorem, a homogeneous quasi-arithmetic mean is a power mean.
  exact aczel J F hqa hhom

Dependency Graph

Location

thesis/CESProofs/Foundations/Defs.lean:224

Module Section

## Emergent CES: Classical Axioms and Main Theorem

In the same file