Documentation

Lean 4 Proof

theorem laplacianQF_const (net : ComplementarityNetwork J) (α : ℝ) :
    laplacianQF net (fun _ => α) = 0 := by
  simp [laplacianQF, sub_self]

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/NetworkCES.lean:145

Module Section

CES on Networks: Heterogeneous Pairwise Complementarity

In the same file