Documentation

Lean 4 Proof

theorem ces_equivalence (J : ℕ) (hJ : 0 < J) (F : AggFun J)
    (hcont : IsContinuousAgg J F)
    (hsymm : IsSymmetric J F)
    (hincr : IsStrictlyIncreasing J F)
    (hhom : IsHomogDegOne J F) :
    EquivalenceStatement J F where
  fp_implies_pm := fun hfp =>
    aggregation_fixed_point J F hcont hsymm hincr hhom hfp
  pm_implies_fp := fun ⟨ρ, hρ, hF⟩ => by
    rw [hF]
    exact powerMean_isFixedPoint hJ ρ hρ

Dependency Graph

Location

thesis/CESProofs/Foundations/Emergence.lean:472

Module Section

Emergence results from Paper 1, Sections 3-5:

In the same file