Documentation

Lean 4 Proof

theorem minimum_misallocation {N : ℕ}
    (w : Fin N → ℝ) (hw : ∀ n, 0 < w n) (flux : Fin N → ℝ) :
    0 ≤ ∑ n : Fin N, flux n ^ 2 / w n := by
  apply Finset.sum_nonneg
  intro n _
  exact div_nonneg (sq_nonneg _) (le_of_lt (hw n))

Dependency Graph

Location

thesis/CESProofs/Dynamics/SymmetricAdjustment.lean:86

Module Section

Results 17-25: Symmetric Adjustment and Transition Rates

In the same file