Documentation

Lean 4 Proof

theorem uniform_effectiveLevelCurvature_trivial (hJ : 2 ≤ J) (ρ : ℝ)
    (P : HierarchicalPartition J 1) (n : Fin 1) :
    effectiveLevelCurvature (uniformNetwork J ρ) P n = 1 - ρ := by
  have hls : levelSize P n = J := by
    simp only [levelSize]
    rw [Finset.filter_true_of_mem (fun j _ => Subsingleton.elim (P.level j) n)]
    rw [Finset.card_univ, Fintype.card_fin]
  unfold effectiveLevelCurvature
  dsimp only
  simp only [hls]
  rw [if_neg (show ¬(J ≤ 1) from by omega)]
  rw [uniform_levelCoupling_trivial hJ ρ P n]
  have hne : (↑J : ℝ) * ((↑J : ℝ) - 1) ≠ 0 := by
    apply mul_ne_zero
    · exact Nat.cast_ne_zero.mpr (by omega)
    · have : (1:ℝ) < ↑J := by exact_mod_cast (show 1 < J by omega)
      linarith
  exact mul_div_cancel_left₀ (1 - ρ) hne

Dependency Graph

Used by

Location

thesis/CESProofs/Hierarchy/EndogenousHierarchy.lean:385

Module Section

Endogenous Hierarchy: Network CES ↔ Spectral Hierarchy Bridge

In the same file