Documentation

Lean 4 Proof

theorem single_level_inter_zero (net : ComplementarityNetwork J)
    (P : HierarchicalPartition J 1) (v : Fin J → ℝ) :
    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 _
  have : P.level j = P.level k := Subsingleton.elim _ _
  simp [this]

Dependency Graph

Location

thesis/CESProofs/Hierarchy/EndogenousHierarchy.lean:135

Module Section

Endogenous Hierarchy: Network CES ↔ Spectral Hierarchy Bridge

In the same file