Laplacian QF

def proved Hierarchy

Documentation

Lean 4 Proof

def laplacianQF (net : ComplementarityNetwork J) (v : Fin J → ℝ) : ℝ :=
  (1 / 2) * ∑ j : Fin J, ∑ k : Fin J, net.w j k * (v j - v k) ^ 2

Dependency Graph

Used by

stronger_complementarity_more_concave laplacianQF_const networkHessian_spectralGap_bound uniform_laplacianQF_eq networkHessianQF uniform_spectralGap adding_link_increases_gap laplacianQF_nonneg spectralGap laplacianQF_zero_iff_blockConstant network_hierarchy_bridge near_decomposable_intra_approximation disconnected_zero_curvature uniform_fiedler_degenerate uniform_laplacianQF_on_perp intra_bounded_by_total qf_decomposition

Location

thesis/CESProofs/CurvatureRoles/NetworkCES.lean:75

Module Section

CES on Networks: Heterogeneous Pairwise Complementarity