Documentation

Lean 4 Proof

theorem qf_decomposition (net : ComplementarityNetwork J) (P : HierarchicalPartition J N)
    (v : Fin J → ℝ) :
    laplacianQF net v = intraLevelQF net P v + interLevelQF net P v := by
  simp only [laplacianQF, intraLevelQF, interLevelQF]
  rw [← mul_add]
  congr 1
  rw [← Finset.sum_add_distrib]
  apply Finset.sum_congr rfl; intro j _
  rw [← Finset.sum_add_distrib]
  apply Finset.sum_congr rfl; intro k _
  by_cases h : P.level j = P.level k <;> simp [h]

Dependency Graph

Used by

Location

thesis/CESProofs/Hierarchy/EndogenousHierarchy.lean:88

Module Section

Endogenous Hierarchy: Network CES ↔ Spectral Hierarchy Bridge

In the same file