Documentation

Lean 4 Proof

theorem uniform_laplacianQF_on_perp (ρ : ℝ) (v : Fin J → ℝ)
    (hv : orthToOne J v) :
    laplacianQF (uniformNetwork J ρ) v =
    (1 - ρ) * (↑J * vecNormSq J v) := by
  rw [uniform_laplacianQF_eq]
  simp only [orthToOne, vecSum, vecNormSq] at hv ⊢
  rw [hv]; ring

Dependency Graph

Used by

Location

thesis/CESProofs/CurvatureRoles/NetworkCES.lean:296

Module Section

CES on Networks: Heterogeneous Pairwise Complementarity

In the same file