Documentation

Lean 4 Proof

structure EquivalenceStatement (J : ℕ) (F : AggFun J) where
  /-- (i) → (ii): Fixed point implies power mean -/
  fp_implies_pm : IsAggFixedPoint J F → IsPowerMean J F
  /-- (ii) → (i): Power mean implies fixed point -/
  pm_implies_fp : IsPowerMean J F → IsAggFixedPoint J F

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/Emergence.lean:465

Module Section

Emergence results from Paper 1, Sections 3-5:

In the same file