Documentation

Lean 4 Proof

theorem powerMean_isFixedPoint {J : ℕ} (hJ : 0 < J) (ρ : ℝ) (hρ : ρ ≠ 0) :
    IsAggFixedPoint J (powerMean J ρ hρ) := by
  intro x hx
  unfold aggregationOp
  suffices h : (fun i => powerMean J ρ hρ (fun _j => x i)) = x by rw [h]
  funext i
  -- Goal: powerMean J ρ hρ (fun _j => x i) = x i
  -- Case split on x i = 0 vs x i > 0
  rcases eq_or_lt_of_le (hx i) with h0 | hpos
  · -- x i = 0
    rw [← h0]
    exact powerMean_zero hJ hρ
  · -- x i > 0
    exact powerMean_symmetricPoint hJ hρ hpos

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/Emergence.lean:87

Module Section

Emergence results from Paper 1, Sections 3-5:

In the same file