PhasePoint

formal source

 176/-! ## Concrete Example: Harmonic Oscillator -/
 177
 178/-- Phase space point (position, momentum). -/
 179structure PhasePoint where
 180  q : ℝ  -- position
 181  p : ℝ  -- momentum
 182
 183/-- Harmonic oscillator energy: H = p²/2m + kq²/2 -/
 184noncomputable def harmonicEnergy (m k : ℝ) (pt : PhasePoint) : ℝ :=
 185  pt.p^2 / (2 * m) + k * pt.q^2 / 2
 186
 187/-- Harmonic oscillator flow (exact solution). -/
 188noncomputable def harmonicFlow (m k : ℝ) (_hm : m > 0) (_hk : k > 0) : ℝ → PhasePoint → PhasePoint :=
 189  fun t pt =>
 190    let ω := Real.sqrt (k / m)
 191    { q := pt.q * Real.cos (ω * t) + pt.p / (m * ω) * Real.sin (ω * t)
 192      p := pt.p * Real.cos (ω * t) - m * ω * pt.q * Real.sin (ω * t) }
 193
 194/-- **THEOREM**: Energy is conserved along harmonic oscillator flow.
 195
 196    This is an explicit verification of energy conservation for the
 197    harmonic oscillator, showing that Noether's theorem works. -/
 198theorem harmonic_energy_conserved (m k : ℝ) (hm : m > 0) (hk : k > 0) :
 199    ∀ pt t, harmonicEnergy m k (harmonicFlow m k hm hk t pt) = harmonicEnergy m k pt := by
 200  intro pt t
 201  simp only [harmonicEnergy, harmonicFlow]
 202  set ω := Real.sqrt (k / m) with hω_def
 203  have hω_pos : ω > 0 := Real.sqrt_pos.mpr (div_pos hk hm)
 204  have hω_sq : ω^2 = k / m := Real.sq_sqrt (le_of_lt (div_pos hk hm))
 205  have hcos_sin : Real.cos (ω * t)^2 + Real.sin (ω * t)^2 = 1 := Real.cos_sq_add_sin_sq (ω * t)
 206  have hmne : m ≠ 0 := ne_of_gt hm
 207  have hωne : ω ≠ 0 := ne_of_gt hω_pos
 208  -- After expansion, the energy terms reduce using ω² = k/m and cos²+sin²=1
 209  -- E' = (1/2m)[(p cos - mωq sin)² + k(q cos + p/(mω) sin)²]