Documentation

Lean 4 Proof

theorem laplacianQF_zero_iff_blockConstant (net : ComplementarityNetwork J)
    (hw : ∀ j k, 0 ≤ net.w j k) (v : Fin J → ℝ) :
    laplacianQF net v = 0 ↔
    ∀ j k, net.w j k > 0 → v j = v k := by
  simp only [laplacianQF]
  -- (1/2) * S = 0 ↔ S = 0 since 1/2 > 0
  have half_ne : (1 / 2 : ℝ) ≠ 0 := by norm_num
  rw [mul_eq_zero, or_iff_right_of_imp (fun h => absurd h half_ne)]
  -- S = Σ_j Σ_k w_{jk}(v_j-v_k)² = 0 ↔ each term = 0
  have hterm : ∀ j k, (0 : ℝ) ≤ net.w j k * (v j - v k) ^ 2 :=
    fun j k => mul_nonneg (hw j k) (sq_nonneg _)
  rw [Finset.sum_eq_zero_iff_of_nonneg (fun j _ =>
    Finset.sum_nonneg (fun k _ => hterm j k))]
  constructor
  · -- Forward: all inner sums = 0 → for w > 0, v_j = v_k
    intro hzero j k hwjk
    have := hzero j (Finset.mem_univ j)
    rw [Finset.sum_eq_zero_iff_of_nonneg (fun k _ => hterm j k)] at this
    have := this k (Finset.mem_univ k)
    -- w_{jk} * (v_j - v_k)² = 0 with w_{jk} > 0 → (v_j - v_k)² = 0
    rcases mul_eq_zero.mp this with h | h
    · linarith
    · rwa [sq_eq_zero_iff, sub_eq_zero] at h
  · -- Backward: block constant → each term = 0
    intro hconst j _
    apply Finset.sum_eq_zero
    intro k _
    by_cases hwjk : net.w j k > 0
    · rw [hconst j k hwjk, sub_self, sq, mul_zero, mul_zero]
    · push_neg at hwjk
      have : net.w j k = 0 := le_antisymm hwjk (hw j k)
      rw [this, zero_mul]

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/NetworkCES.lean:584

Module Section

CES on Networks: Heterogeneous Pairwise Complementarity

In the same file