Documentation

Lean 4 Proof

theorem uniform_fiedler_degenerate :
    ∀ v : Fin J → ℝ, orthToOne J v → vecNormSq J v > 0 →
    laplacianQF (uniformNetwork J ρ) v / vecNormSq J v =
    spectralGap (uniformNetwork J ρ) := by
  intro v hv hvn
  -- Derive J ≥ 2 (J < 2 makes hypotheses contradictory)
  have hJ : 2 ≤ J := by
    by_contra h; push_neg at h
    have : J = 0 ∨ J = 1 := by omega
    rcases this with rfl | rfl
    · -- J = 0: vecNormSq is sum over Fin 0 = 0
      simp [vecNormSq] at hvn
    · -- J = 1: orthToOne forces v 0 = 0, so vecNormSq = 0
      have hv0 : v (0 : Fin 1) = 0 := by
        have := hv; simp [orthToOne, vecSum] at this; exact this
      simp [vecNormSq, hv0] at hvn
  rw [uniform_spectralGap hJ, uniform_laplacianQF_on_perp ρ v hv]
  field_simp

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/NetworkCES.lean:374

Module Section

CES on Networks: Heterogeneous Pairwise Complementarity

In the same file