Documentation

Lean 4 Proof

theorem intraLevelQF_nonneg (net : ComplementarityNetwork J)
    (hw : ∀ j k, 0 ≤ net.w j k)
    (P : HierarchicalPartition J N) (v : Fin J → ℝ) :
    0 ≤ intraLevelQF net P v := by
  apply mul_nonneg (by norm_num : (0:ℝ) ≤ 1/2)
  apply Finset.sum_nonneg; intro j _
  apply Finset.sum_nonneg; intro k _
  apply mul_nonneg _ (sq_nonneg _)
  by_cases h : P.level j = P.level k <;> simp [h, hw j k]

Dependency Graph

Used by

Location

thesis/CESProofs/Hierarchy/EndogenousHierarchy.lean:103

Module Section

Endogenous Hierarchy: Network CES ↔ Spectral Hierarchy Bridge

In the same file