Documentation

Lean 4 Proof

theorem near_decomposable_pointwise (net : ComplementarityNetwork J)
    (P : HierarchicalPartition J N) (ε : ℝ)
    (hnd : isNearDecomposable net P ε) (v : Fin J → ℝ) (j k : Fin J)
    (hne : P.level j ≠ P.level k) :
    net.w j k * (v j - v k) ^ 2 ≤ ε * (v j - v k) ^ 2 :=
  mul_le_mul_of_nonneg_right (hnd j k hne) (sq_nonneg _)

Dependency Graph

Location

thesis/CESProofs/Hierarchy/EndogenousHierarchy.lean:186

Module Section

Endogenous Hierarchy: Network CES ↔ Spectral Hierarchy Bridge

In the same file