Documentation

Lean 4 Proof

theorem oscillationEnergy_nonneg {H : Fin N → ℝ} (hH : ∀ n, 0 ≤ H n)
    (ξ : Fin N → ℝ) :
    0 ≤ oscillationEnergy H ξ := by
  simp only [oscillationEnergy]
  apply mul_nonneg
  · norm_num
  · exact Finset.sum_nonneg fun n _ => mul_nonneg (hH n) (sq_nonneg _)

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/Defs.lean:209

Module Section

Core definitions for the Lean formalization of Paper 3:

In the same file