Documentation

Lean 4 Proof

theorem aggregation_fixed_point (k : ℕ) (F : AggFun k)
    (hcont : IsContinuousAgg k F)
    (hsymm : IsSymmetric k F)
    (hincr : IsStrictlyIncreasing k F)
    (hhom : IsHomogDegOne k F)
    (_hfp : IsAggFixedPoint k F) :
    IsPowerMean k F := by
  -- A fixed point of R_k satisfies scale consistency
  have hsc : IsScaleConsistent k F := by
    intro m n _ x; rfl
  -- By the Emergent CES theorem
  exact aczel k F (kolmogorov_nagumo k F hcont hsymm hincr hsc) hhom

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/Emergence.lean:50

Module Section

Emergence results from Paper 1, Sections 3-5:

In the same file