Documentation

Lean 4 Proof

theorem uniform_levelCoupling_trivial (_hJ : 2 ≤ J) (ρ : ℝ)
    (P : HierarchicalPartition J 1) (n : Fin 1) :
    levelCoupling (uniformNetwork J ρ) P n = ↑J * (↑J - 1) * (1 - ρ) := by
  simp only [levelCoupling, uniformNetwork]
  -- In Fin 1, all levels equal: conditions become j ≠ k
  have hcond : ∀ (j k : Fin J),
      (if P.level j = n ∧ P.level k = n ∧ j ≠ k
       then (if j = k then (0 : ℝ) else 1 - ρ) else 0) =
      if j ≠ k then (1 - ρ) else 0 := by
    intro j k
    have hj := Subsingleton.elim (P.level j) n
    have hk := Subsingleton.elim (P.level k) n
    by_cases hjk : j = k <;> simp [hj, hk, hjk]
  simp_rw [hcond]
  -- Count: ∑ j, ∑ k, if j ≠ k then (1-ρ) else 0 = J*(J-1)*(1-ρ)
  -- Handle inner sum first to avoid simp_rw applying at both levels
  have inner : ∀ j : Fin J,
      ∑ k : Fin J, (if j ≠ k then (1 - ρ) else (0 : ℝ)) = (↑J - 1) * (1 - ρ) := by
    intro j
    have : ∀ k : Fin J, (if j ≠ k then (1 - ρ) else (0 : ℝ)) =
        (1 - ρ) - if j = k then (1 - ρ) else 0 := by
      intro k; by_cases h : j = k <;> simp [h]
    simp_rw [this, Finset.sum_sub_distrib, Finset.sum_const, Finset.card_univ,
      Fintype.card_fin, nsmul_eq_mul, Finset.sum_ite_eq, Finset.mem_univ, ite_true]
    ring
  simp_rw [inner, Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
  ring

Dependency Graph

Used by

Location

thesis/CESProofs/Hierarchy/EndogenousHierarchy.lean:355

Module Section

Endogenous Hierarchy: Network CES ↔ Spectral Hierarchy Bridge

In the same file