Documentation

Lean 4 Proof

theorem networkHessian_spectralGap_bound (net : ComplementarityNetwork J)
    (hw : ∀ j k, 0 ≤ net.w j k) {c : ℝ} (hc : 0 < c) (_hJ : 0 < J)
    (v : Fin J → ℝ) (hv : orthToOne J v) :
    networkHessianQF net c v ≤
    -(spectralGap net / ((↑J : ℝ) ^ 2 * c)) * vecNormSq J v := by
  -- H(v) = -(1/(J²c)) · L(v) and spectralGap ≤ L(v)/‖v‖² (by csInf_le)
  -- So L(v) ≥ spectralGap · ‖v‖², hence H(v) ≤ -(spectralGap/(J²c)) · ‖v‖²
  simp only [networkHessianQF]
  -- Factor: both sides are -(1/(J²c)) · something
  -- LHS = -(1/(J²c)) · L(v), RHS = -(spectralGap/(J²c)) · ‖v‖²
  -- Need: L(v) ≥ spectralGap · ‖v‖²
  have hJ2c : 0 < (↑J : ℝ) ^ 2 * c := mul_pos (sq_pos_of_pos (Nat.cast_pos.mpr _hJ)) hc
  by_cases hvn : vecNormSq J v = 0
  · -- v = 0 case: both sides = 0
    have hv_zero : ∀ j, v j = 0 := by
      intro j
      have := Finset.sum_eq_zero_iff_of_nonneg (fun j _ => sq_nonneg (v j))
        |>.mp (show ∑ j : Fin J, v j ^ 2 = 0 from hvn) j (Finset.mem_univ j)
      exact pow_eq_zero_iff (n := 2) (by norm_num) |>.mp this
    have hL : laplacianQF net v = 0 := by
      simp only [laplacianQF, hv_zero, sub_self, zero_pow (by norm_num : 2 ≠ 0),
                  mul_zero, Finset.sum_const_zero]
    rw [hL, hvn]; simp
  · -- v ≠ 0 case: use csInf_le
    have hvn_pos : 0 < vecNormSq J v := by
      rcases (ne_iff_lt_or_gt.mp hvn) with h | h
      · exact absurd h (not_lt.mpr (Finset.sum_nonneg (fun j _ => sq_nonneg (v j))))
      · exact h
    -- spectralGap ≤ L(v)/‖v‖² by csInf_le
    have hmem : laplacianQF net v / vecNormSq J v ∈
        (fun v => laplacianQF net v / vecNormSq J v) ''
        {v : Fin J → ℝ | orthToOne J v ∧ vecNormSq J v > 0} :=
      ⟨v, ⟨hv, hvn_pos⟩, rfl⟩
    have hbdd : BddBelow ((fun v => laplacianQF net v / vecNormSq J v) ''
        {v : Fin J → ℝ | orthToOne J v ∧ vecNormSq J v > 0}) := by
      use 0; intro r ⟨u, ⟨_, hun⟩, hr⟩
      rw [← hr]
      exact div_nonneg (laplacianQF_nonneg net hw u) (le_of_lt hun)
    have hgap_le : spectralGap net ≤ laplacianQF net v / vecNormSq J v :=
      csInf_le hbdd hmem
    -- L(v) ≥ spectralGap · ‖v‖²
    have hLge : spectralGap net * vecNormSq J v ≤ laplacianQF net v := by
      rwa [le_div_iff₀ hvn_pos] at hgap_le
    -- -(1/(J²c)) · L(v) ≤ -(1/(J²c)) · spectralGap · ‖v‖²
    -- i.e., -(1/(J²c)) * L ≤ -(spectralGap/(J²c)) * ‖v‖²
    -- Goal: -(1/(J²c)) * L(v) ≤ -(sg/(J²c)) * ‖v‖²
    -- From hLge: sg * ‖v‖² ≤ L(v)
    -- Multiply by 1/(J²c) > 0 preserving direction, then negate both sides
    have hJ2c_ne : (↑J : ℝ) ^ 2 * c ≠ 0 := ne_of_gt hJ2c
    have h1 : spectralGap net * vecNormSq J v / ((↑J : ℝ) ^ 2 * c) ≤
              laplacianQF net v / ((↑J : ℝ) ^ 2 * c) :=
      div_le_div_of_nonneg_right hLge hJ2c.le
    -- Now negate: -L/(J²c) ≤ -sg*‖v‖²/(J²c)
    -- Rewrite goal to match
    change -(1 / ((↑J : ℝ) ^ 2 * c)) * laplacianQF net v ≤
         -(spectralGap net / ((↑J : ℝ) ^ 2 * c)) * vecNormSq J v
    have lhs_rw : -(1 / ((↑J : ℝ) ^ 2 * c)) * laplacianQF net v =
                  -(laplacianQF net v / ((↑J : ℝ) ^ 2 * c)) := by ring
    have rhs_rw : -(spectralGap net / ((↑J : ℝ) ^ 2 * c)) * vecNormSq J v =
                  -(spectralGap net * vecNormSq J v / ((↑J : ℝ) ^ 2 * c)) := by ring
    rw [lhs_rw, rhs_rw]
    exact neg_le_neg h1

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/NetworkCES.lean:635

Module Section

CES on Networks: Heterogeneous Pairwise Complementarity

In the same file