Documentation

Lean 4 Proof

theorem uniform_networkHessian_eq_cesHessian (ρ c : ℝ) (v : Fin J → ℝ) :
    networkHessianQF (uniformNetwork J ρ) c v = cesHessianQF J ρ c v := by
  simp only [networkHessianQF, cesHessianQF, uniform_laplacianQF_eq]
  ring

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/NetworkCES.lean:210

Module Section

CES on Networks: Heterogeneous Pairwise Complementarity

In the same file