Documentation

Lean 4 Proof

theorem uniform_effectiveLevelRho_trivial (hJ : 2 ≤ J) (ρ : ℝ)
    (P : HierarchicalPartition J 1) (n : Fin 1) :
    effectiveLevelRho (uniformNetwork J ρ) P n = ρ := by
  simp only [effectiveLevelRho, uniform_effectiveLevelCurvature_trivial hJ ρ P n]
  ring

Dependency Graph

Location

thesis/CESProofs/Hierarchy/EndogenousHierarchy.lean:407

Module Section

Endogenous Hierarchy: Network CES ↔ Spectral Hierarchy Bridge

In the same file