Documentation

Lean 4 Proof

theorem intra_bounded_by_total (net : ComplementarityNetwork J)
    (hw : ∀ j k, 0 ≤ net.w j k)
    (P : HierarchicalPartition J N) (v : Fin J → ℝ) :
    intraLevelQF net P v ≤ laplacianQF net v := by
  rw [qf_decomposition net P v]
  linarith [interLevelQF_nonneg net hw P v]

Dependency Graph

Location

thesis/CESProofs/Hierarchy/EndogenousHierarchy.lean:225

Module Section

Endogenous Hierarchy: Network CES ↔ Spectral Hierarchy Bridge

In the same file