Documentation

Lean 4 Proof

theorem networkHessianQF_neg_semidef (net : ComplementarityNetwork J)
    (hw : ∀ j k, 0 ≤ net.w j k) {c : ℝ} (hc : 0 < c) (_hJ : 0 < J)
    (v : Fin J → ℝ) :
    networkHessianQF net c v ≤ 0 := by
  unfold networkHessianQF
  apply mul_nonpos_of_nonpos_of_nonneg
  · apply neg_nonpos_of_nonneg
    apply div_nonneg
    · norm_num
    · apply mul_nonneg
      · apply sq_nonneg
      · linarith
  · exact laplacianQF_nonneg net hw v

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/NetworkCES.lean:223

Module Section

CES on Networks: Heterogeneous Pairwise Complementarity

In the same file