Documentation

Lean 4 Proof

theorem disconnected_inter_zero (net : ComplementarityNetwork J)
    (P : HierarchicalPartition J N) (v : Fin J → ℝ)
    (hdisc : isDisconnected net P) :
    interLevelQF net P v = 0 := by
  simp only [interLevelQF, ne_eq]
  convert mul_zero (1 / 2 : ℝ)
  apply Finset.sum_eq_zero; intro j _
  apply Finset.sum_eq_zero; intro k _
  by_cases h : P.level j = P.level k
  · simp [h]
  · simp [h, hdisc j k h]

Dependency Graph

Location

thesis/CESProofs/Hierarchy/EndogenousHierarchy.lean:156

Module Section

Endogenous Hierarchy: Network CES ↔ Spectral Hierarchy Bridge

In the same file