Documentation

Lean 4 Proof

theorem laplacianQF_nonneg (net : ComplementarityNetwork J)
    (hw : ∀ j k, 0 ≤ net.w j k) (v : Fin J → ℝ) :
    0 ≤ laplacianQF net v := by
  unfold laplacianQF
  apply mul_nonneg
  · norm_num
  · apply Finset.sum_nonneg; intro j _
    apply Finset.sum_nonneg; intro k _
    exact mul_nonneg (hw j k) (sq_nonneg _)

Dependency Graph

Used by

Location

thesis/CESProofs/CurvatureRoles/NetworkCES.lean:133

Module Section

CES on Networks: Heterogeneous Pairwise Complementarity

In the same file