harmonicFlow

formal source

 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)²]
 210  --    = (1/2m)[p² cos² + m²ω²q² sin² - 2mωpq sin cos
 211  --           + kq² cos² + kp²/(m²ω²) sin² + 2kpq/(mω) sin cos]
 212  -- Using k = mω²:
 213  --    = (1/2m)[p² cos² + m²ω²q² sin² + m²ω²q² cos² + p² sin²]
 214  --    = (1/2m)[p²(cos² + sin²) + m²ω²q²(sin² + cos²)]
 215  --    = (1/2m)[p² + k·m·q²] = p²/2m + kq²/2 = E
 216  have hmω_sq : m * ω^2 = k := by rw [hω_sq]; field_simp
 217  -- We prove the equality by direct calculation
 218  have key : ∀ (c s : ℝ), c^2 + s^2 = 1 →