Documentation

Lean 4 Proof

theorem near_decomposable_intra_approximation (net : ComplementarityNetwork J)
    (_hw : ∀ j k, 0 ≤ net.w j k)
    (P : HierarchicalPartition J N) {ε : ℝ} (hε : 0 ≤ ε)
    (hnd : isNearDecomposable net P ε) (v : Fin J → ℝ) :
    laplacianQF net v - intraLevelQF net P v ≤ ε * crossLevelDistQF P v := by
  have hdecomp := qf_decomposition net P v
  linarith [hierarchy_approximation_quality net P hε hnd v]

Dependency Graph

Location

thesis/CESProofs/Hierarchy/EndogenousHierarchy.lean:341

Module Section

Endogenous Hierarchy: Network CES ↔ Spectral Hierarchy Bridge

In the same file