Documentation

Lean 4 Proof

noncomputable def fiedlerVector (_net : ComplementarityNetwork J) : Fin J → ℝ :=
  open Classical in
  if h : ∃ v : Fin J → ℝ, orthToOne J v ∧ vecNormSq J v > 0 then
    Classical.choose h
  else
    fun _ => 0

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/NetworkCES.lean:118

Module Section

CES on Networks: Heterogeneous Pairwise Complementarity

In the same file