Documentation

Lean 4 Proof

theorem network_hierarchy_bridge (net : ComplementarityNetwork J)
    (hw : ∀ j k, 0 ≤ net.w j k)
    (P : HierarchicalPartition J N) (v : Fin J → ℝ) :
    laplacianQF net v = intraLevelQF net P v + interLevelQF net P v ∧
    0 ≤ intraLevelQF net P v ∧
    0 ≤ interLevelQF net P v :=
  ⟨qf_decomposition net P v,
   intraLevelQF_nonneg net hw P v,
   interLevelQF_nonneg net hw P v⟩

Dependency Graph

Location

thesis/CESProofs/Hierarchy/EndogenousHierarchy.lean:208

Module Section

Endogenous Hierarchy: Network CES ↔ Spectral Hierarchy Bridge

In the same file