Documentation

Lean 4 Proof

theorem network_curvature_conservation_ineq
    {n : ℕ} (a : Fin n → ℝ) (ha : ∀ i, 0 < a i) :
    (↑n : ℝ) ^ 2 ≤ (∑ i, a i) * (∑ i, (a i)⁻¹) := by
  have key := Finset.sum_sq_le_sum_mul_sum_of_sq_eq_mul Finset.univ
    (r := fun _ => (1 : ℝ))
    (fun i _ => (ha i).le)
    (fun i _ => (inv_pos.mpr (ha i)).le)
    (fun i _ => by simp [mul_inv_cancel₀ (ne_of_gt (ha i))])
  simp only [Finset.sum_const, Finset.card_fin, nsmul_eq_mul, mul_one] at key
  exact key

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/NetworkCES.lean:822

Module Section

## Network Scaling Results

In the same file