Documentation

Lean 4 Proof

theorem line_of_fixed_points (J : ℕ) (hJ : 0 < J) (ρ : ℝ) (hρ : ρ ≠ 0) :
    IsAggFixedPoint J (powerMean J ρ hρ) :=
  powerMean_isFixedPoint hJ ρ hρ

Dependency Graph

Location

thesis/CESProofs/Hierarchy/RenormalizationGroup.lean:258

Module Section

Renormalization Group for CES:

In the same file