Documentation

Lean 4 Proof

theorem stronger_complementarity_more_concave
    (net₁ net₂ : ComplementarityNetwork J)
    (hw : ∀ j k, net₂.w j k ≤ net₁.w j k)
    {c : ℝ} (hc : 0 < c) (_hJ : 0 < J) (v : Fin J → ℝ) :
    networkHessianQF net₁ c v ≤ networkHessianQF net₂ c v := by
  simp only [networkHessianQF]
  -- -(1/(J²c)) · L₁(v) ≤ -(1/(J²c)) · L₂(v)
  -- ↔ L₂(v) ≤ L₁(v)  [since -(1/(J²c)) < 0 flips inequality]
  -- ↔ Σ w₂(v_j-v_k)² ≤ Σ w₁(v_j-v_k)²  ✓ since w₂ ≤ w₁
  have hcoeff : 0 ≤ (1 : ℝ) / ((↑J : ℝ) ^ 2 * c) :=
    div_nonneg (by norm_num) (mul_nonneg (sq_nonneg _) hc.le)
  have hL : laplacianQF net₂ v ≤ laplacianQF net₁ v := by
    unfold laplacianQF
    apply mul_le_mul_of_nonneg_left
    · apply Finset.sum_le_sum; intro j _
      apply Finset.sum_le_sum; intro k _
      exact mul_le_mul_of_nonneg_right (hw j k) (sq_nonneg _)
    · norm_num
  -- neg_mul flips: -(coeff) * L₁ ≤ -(coeff) * L₂ ↔ L₂ ≤ L₁
  linarith [mul_le_mul_of_nonneg_left hL hcoeff]

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/NetworkCES.lean:241

Module Section

CES on Networks: Heterogeneous Pairwise Complementarity

In the same file