From 80773e609a0401407d49c168508cd507134ebb31 Mon Sep 17 00:00:00 2001 From: Bergschaf Date: Mon, 4 May 2026 17:10:34 +0200 Subject: [PATCH 1/8] Harmonic oscillator --- .../HarmonicOscillator/Solution.lean | 103 +++++++++++------- 1 file changed, 63 insertions(+), 40 deletions(-) diff --git a/Physlib/ClassicalMechanics/HarmonicOscillator/Solution.lean b/Physlib/ClassicalMechanics/HarmonicOscillator/Solution.lean index a8b9b9a9f..51275cc95 100644 --- a/Physlib/ClassicalMechanics/HarmonicOscillator/Solution.lean +++ b/Physlib/ClassicalMechanics/HarmonicOscillator/Solution.lean @@ -25,7 +25,6 @@ prove that they satisfy the equation of motion, and prove some properties of the - A. The initial conditions - A.1. Definition of the initial conditions - - A.1.1. Extensionality lemma - A.2. Relation to other types of initial conditions - A.3. The zero initial conditions - A.3.1. Simple results for the zero initial conditions @@ -80,8 +79,12 @@ We start by defining the type of initial conditions for the harmonic oscillator. -/ /-- The initial conditions for the harmonic oscillator specified by an initial position, - and an initial velocity. -/ -structure InitialConditions where + and an initial velocity. + +The `@[ext]` attribute provides an extensionality lemma for `InitialConditions`. +That is, a lemma which states that two initial conditions are equal if their +initial positions and initial velocities are equal. -/ +@[ext] structure InitialConditions where /-- The initial position of the harmonic oscillator. -/ x₀ : EuclideanSpace ℝ (Fin 1) /-- The initial velocity of the harmonic oscillator. -/ @@ -89,23 +92,6 @@ structure InitialConditions where /-! -#### A.1.1. Extensionality lemma - -We prove an extensionality lemma for `InitialConditions`. -That is, a lemma which states that two initial conditions are equal if their -initial positions and initial velocities are equal. - --/ - -@[ext] -lemma InitialConditions.ext {IC₁ IC₂ : InitialConditions} (h1 : IC₁.x₀ = IC₂.x₀) - (h2 : IC₁.v₀ = IC₂.v₀) : IC₁ = IC₂ := by - cases IC₁ - cases IC₂ - simp_all - -/-! - ### A.2. Relation to other types of initial conditions We relate the initial condition given by an initial position and an initial velocity @@ -147,7 +133,7 @@ This is useful when the natural reference point for a problem is not at time zer The conditions can be converted to the standard `InitialConditions` format (at `t=0`) using the `toInitialConditions` function. -/ -structure InitialConditionsAtTime where +@[ext] structure InitialConditionsAtTime where /-- The time at which the initial conditions are specified. -/ t₀ : Time /-- The position at time t₀. -/ @@ -155,21 +141,6 @@ structure InitialConditionsAtTime where /-- The velocity at time t₀. -/ v_t₀ : EuclideanSpace ℝ (Fin 1) -/-! - -##### A.2.1.1. Extensionality lemma - -We prove an extensionality lemma for `InitialConditionsAtTime`. - --/ - -@[ext] -lemma InitialConditionsAtTime.ext {IC₁ IC₂ : InitialConditionsAtTime} - (h1 : IC₁.t₀ = IC₂.t₀) (h2 : IC₁.x_t₀ = IC₂.x_t₀) (h3 : IC₁.v_t₀ = IC₂.v_t₀) : - IC₁ = IC₂ := by - cases IC₁ - cases IC₂ - simp_all /-! @@ -248,6 +219,13 @@ lemma x₀_zero : x₀ 0 = 0 := rfl @[simp] lemma v₀_zero : v₀ 0 = 0 := rfl +def ZeroVelocity (x : EuclideanSpace ℝ (Fin 1)) : InitialConditions where + x₀ := x + v₀ := 0 + +@[simp] +lemma ZeroVelocity.v₀_zero {x : EuclideanSpace ℝ (Fin 1)} : v₀ (ZeroVelocity x) = 0 := rfl + end InitialConditions /-! @@ -296,8 +274,18 @@ The trajectory for zero initial conditions is the zero function. lemma trajectory_zero : trajectory S 0 = fun _ => 0 := by simp [trajectory_eq] + +-- TODO sinnvoller titel +lemma trajectory_ZeroVelocity {x₀ : EuclideanSpace ℝ (Fin 1)} : + (ZeroVelocity x₀).trajectory S = fun t : Time => cos (S.ω * t) • x₀ := by + ext t i + simp only [trajectory, ZeroVelocity.v₀_zero, smul_zero, add_zero, PiLp.smul_apply, smul_eq_mul, + mul_eq_mul_left_iff] + exact Or.inl rfl + /-! + ### B.3. Smoothness of the trajectories The trajectories for any initial conditions are smooth functions of time. @@ -673,7 +661,6 @@ lemma toInitialConditions_velocity_at_t₀ (S : HarmonicOscillator) rw [← h1] ring -set_option backward.isDefEq.respectTransparency false in /-- The energy of the trajectory at time `t₀` equals the energy computed from the initial conditions at `t₀`. -/ lemma toInitialConditions_energy_at_t₀ (S : HarmonicOscillator) @@ -790,7 +777,6 @@ the velocity is zero. -/ -set_option backward.isDefEq.respectTransparency false in lemma trajectory_velocity_eq_zero_iff (IC : InitialConditions) (t : Time) : ∂ₜ (IC.trajectory S) t = 0 ↔ ‖(IC.trajectory S) t‖ = √(‖IC.x₀‖^2 + (‖IC.v₀‖/S.ω)^2) := by @@ -880,14 +866,51 @@ We give some open TODOs for the classical harmonic oscillator. -/ +end InitialConditions + +/-- +The period of a Harmonic Osciallator is `2 * π / ω`. +-/ +noncomputable def T (S : HarmonicOscillator) : ℝ := 2 * π / S.ω + +lemma T.def : S.T = 2 * π / S.ω := rfl + +lemma T.pos : 0 < S.T := by + have := S.ω_pos + rw [T.def] + positivity + +/-- +The trajectory of the harmonic oscialltor is periodic with period of `2 * π / ω`. +-/ +lemma trajectory_periodic (IC : InitialConditions) : + Function.Periodic (IC.trajectory S) S.T := by + simp only [Function.Periodic, InitialConditions.trajectory, add_val] + intro t + have h1 : Real.cos (S.ω * (t.val + S.T)) = Real.cos (S.ω * t) := + calc + _ = Real.cos (S.ω * t.val + S.ω * S.ω⁻¹ * 2 * π) := by + rw [T.def] + ring_nf + _ = Real.cos (S.ω * t.val + 2 * π) := by + rw [mul_inv_cancel₀ S.ω_ne_zero] + ring + _ = _ := by rw [Real.cos_add_two_pi] + rw [h1] + congr 3 + have h2 : S.ω * (t.val + 2 * π / S.ω) = S.ω * t.val + 2 * π := calc + _ = S.ω * t.val + S.ω * S.ω⁻¹ * 2 * π := by ring + _ = _ := by + rw [mul_inv_cancel₀ S.ω_ne_zero] + ring + rw [T.def, h2, Real.sin_add_two_pi] + TODO "For the classical harmonic oscillator find the time for which it returns to it's initial position and velocity." TODO "For the classical harmonic oscillator find the times for which it passes through zero." -end InitialConditions - end HarmonicOscillator end ClassicalMechanics From 105dfb08e179c2258cc9352e40765ffb370945e3 Mon Sep 17 00:00:00 2001 From: Bergschaf Date: Mon, 4 May 2026 17:15:49 +0200 Subject: [PATCH 2/8] remove --- .../HarmonicOscillator/Solution.lean | 16 ---------------- 1 file changed, 16 deletions(-) diff --git a/Physlib/ClassicalMechanics/HarmonicOscillator/Solution.lean b/Physlib/ClassicalMechanics/HarmonicOscillator/Solution.lean index 51275cc95..e10882be4 100644 --- a/Physlib/ClassicalMechanics/HarmonicOscillator/Solution.lean +++ b/Physlib/ClassicalMechanics/HarmonicOscillator/Solution.lean @@ -219,13 +219,6 @@ lemma x₀_zero : x₀ 0 = 0 := rfl @[simp] lemma v₀_zero : v₀ 0 = 0 := rfl -def ZeroVelocity (x : EuclideanSpace ℝ (Fin 1)) : InitialConditions where - x₀ := x - v₀ := 0 - -@[simp] -lemma ZeroVelocity.v₀_zero {x : EuclideanSpace ℝ (Fin 1)} : v₀ (ZeroVelocity x) = 0 := rfl - end InitialConditions /-! @@ -274,15 +267,6 @@ The trajectory for zero initial conditions is the zero function. lemma trajectory_zero : trajectory S 0 = fun _ => 0 := by simp [trajectory_eq] - --- TODO sinnvoller titel -lemma trajectory_ZeroVelocity {x₀ : EuclideanSpace ℝ (Fin 1)} : - (ZeroVelocity x₀).trajectory S = fun t : Time => cos (S.ω * t) • x₀ := by - ext t i - simp only [trajectory, ZeroVelocity.v₀_zero, smul_zero, add_zero, PiLp.smul_apply, smul_eq_mul, - mul_eq_mul_left_iff] - exact Or.inl rfl - /-! From 1887d33d3b2131710b88933239c2edd8ba7b0e74 Mon Sep 17 00:00:00 2001 From: Bergschaf Date: Mon, 4 May 2026 17:16:47 +0200 Subject: [PATCH 3/8] newline --- Physlib/ClassicalMechanics/HarmonicOscillator/Solution.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Physlib/ClassicalMechanics/HarmonicOscillator/Solution.lean b/Physlib/ClassicalMechanics/HarmonicOscillator/Solution.lean index e10882be4..482e43f24 100644 --- a/Physlib/ClassicalMechanics/HarmonicOscillator/Solution.lean +++ b/Physlib/ClassicalMechanics/HarmonicOscillator/Solution.lean @@ -269,7 +269,6 @@ lemma trajectory_zero : trajectory S 0 = fun _ => 0 := by /-! - ### B.3. Smoothness of the trajectories The trajectories for any initial conditions are smooth functions of time. From b3fab2b41fda9f1a17d3d9f325797e645d960a42 Mon Sep 17 00:00:00 2001 From: Bergschaf Date: Mon, 4 May 2026 17:45:48 +0200 Subject: [PATCH 4/8] golf --- .../HarmonicOscillator/Solution.lean | 23 ++++++------------- 1 file changed, 7 insertions(+), 16 deletions(-) diff --git a/Physlib/ClassicalMechanics/HarmonicOscillator/Solution.lean b/Physlib/ClassicalMechanics/HarmonicOscillator/Solution.lean index 482e43f24..496067d41 100644 --- a/Physlib/ClassicalMechanics/HarmonicOscillator/Solution.lean +++ b/Physlib/ClassicalMechanics/HarmonicOscillator/Solution.lean @@ -854,13 +854,15 @@ end InitialConditions /-- The period of a Harmonic Osciallator is `2 * π / ω`. -/ -noncomputable def T (S : HarmonicOscillator) : ℝ := 2 * π / S.ω +noncomputable def period (S : HarmonicOscillator) : ℝ := 2 * π / S.ω -lemma T.def : S.T = 2 * π / S.ω := rfl +noncomputable abbrev T := HarmonicOscillator.period -lemma T.pos : 0 < S.T := by +lemma period_eq : S.T = 2 * π / S.ω := rfl + +lemma period_pos : 0 < S.T := by have := S.ω_pos - rw [T.def] + rw [period_eq] positivity /-- @@ -870,23 +872,12 @@ lemma trajectory_periodic (IC : InitialConditions) : Function.Periodic (IC.trajectory S) S.T := by simp only [Function.Periodic, InitialConditions.trajectory, add_val] intro t - have h1 : Real.cos (S.ω * (t.val + S.T)) = Real.cos (S.ω * t) := - calc - _ = Real.cos (S.ω * t.val + S.ω * S.ω⁻¹ * 2 * π) := by - rw [T.def] - ring_nf - _ = Real.cos (S.ω * t.val + 2 * π) := by - rw [mul_inv_cancel₀ S.ω_ne_zero] - ring - _ = _ := by rw [Real.cos_add_two_pi] - rw [h1] - congr 3 have h2 : S.ω * (t.val + 2 * π / S.ω) = S.ω * t.val + 2 * π := calc _ = S.ω * t.val + S.ω * S.ω⁻¹ * 2 * π := by ring _ = _ := by rw [mul_inv_cancel₀ S.ω_ne_zero] ring - rw [T.def, h2, Real.sin_add_two_pi] + rw [period_eq, h2, Real.cos_add_two_pi, Real.sin_add_two_pi] TODO "For the classical harmonic oscillator find the time for which it returns to it's initial position and velocity." From c2377cc6415c4059d4d17187415866ae67ffc741 Mon Sep 17 00:00:00 2001 From: Bergschaf Date: Mon, 4 May 2026 18:31:09 +0200 Subject: [PATCH 5/8] golf --- .../HarmonicOscillator/Solution.lean | 25 ++++++++----------- 1 file changed, 11 insertions(+), 14 deletions(-) diff --git a/Physlib/ClassicalMechanics/HarmonicOscillator/Solution.lean b/Physlib/ClassicalMechanics/HarmonicOscillator/Solution.lean index 496067d41..a5beadfc0 100644 --- a/Physlib/ClassicalMechanics/HarmonicOscillator/Solution.lean +++ b/Physlib/ClassicalMechanics/HarmonicOscillator/Solution.lean @@ -852,32 +852,29 @@ We give some open TODOs for the classical harmonic oscillator. end InitialConditions /-- -The period of a Harmonic Osciallator is `2 * π / ω`. +The period of a harmonic oscillator is `2 * π / ω`. -/ noncomputable def period (S : HarmonicOscillator) : ℝ := 2 * π / S.ω -noncomputable abbrev T := HarmonicOscillator.period +scoped notation "T" => HarmonicOscillator.period -lemma period_eq : S.T = 2 * π / S.ω := rfl +lemma period_eq : T S = 2 * π / S.ω := rfl -lemma period_pos : 0 < S.T := by +lemma period_pos : 0 < T S := by have := S.ω_pos rw [period_eq] positivity /-- -The trajectory of the harmonic oscialltor is periodic with period of `2 * π / ω`. +The trajectory of the harmonic oscillator is periodic with period of `2 * π / ω`. -/ lemma trajectory_periodic (IC : InitialConditions) : - Function.Periodic (IC.trajectory S) S.T := by - simp only [Function.Periodic, InitialConditions.trajectory, add_val] - intro t - have h2 : S.ω * (t.val + 2 * π / S.ω) = S.ω * t.val + 2 * π := calc - _ = S.ω * t.val + S.ω * S.ω⁻¹ * 2 * π := by ring - _ = _ := by - rw [mul_inv_cancel₀ S.ω_ne_zero] - ring - rw [period_eq, h2, Real.cos_add_two_pi, Real.sin_add_two_pi] + Function.Periodic (IC.trajectory S) (T S) := fun t ↦ by + have h2 : S.ω * (t.val + 2 * π / S.ω) = S.ω * t.val + 2 * π := by + have := S.ω_ne_zero + ring_nf; field_simp + rw [InitialConditions.trajectory, add_val, period_eq, h2, cos_add_two_pi, sin_add_two_pi] + rfl TODO "For the classical harmonic oscillator find the time for which it returns to it's initial position and velocity." From f5d18b2f22111b9c9a28c57ec1d7d80ed30f44f5 Mon Sep 17 00:00:00 2001 From: Bergschaf Date: Mon, 4 May 2026 18:31:29 +0200 Subject: [PATCH 6/8] golf --- Physlib/ClassicalMechanics/HarmonicOscillator/Solution.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Physlib/ClassicalMechanics/HarmonicOscillator/Solution.lean b/Physlib/ClassicalMechanics/HarmonicOscillator/Solution.lean index a5beadfc0..858261c5e 100644 --- a/Physlib/ClassicalMechanics/HarmonicOscillator/Solution.lean +++ b/Physlib/ClassicalMechanics/HarmonicOscillator/Solution.lean @@ -870,10 +870,10 @@ The trajectory of the harmonic oscillator is periodic with period of `2 * π / -/ lemma trajectory_periodic (IC : InitialConditions) : Function.Periodic (IC.trajectory S) (T S) := fun t ↦ by - have h2 : S.ω * (t.val + 2 * π / S.ω) = S.ω * t.val + 2 * π := by + have h : S.ω * (t.val + 2 * π / S.ω) = S.ω * t.val + 2 * π := by have := S.ω_ne_zero ring_nf; field_simp - rw [InitialConditions.trajectory, add_val, period_eq, h2, cos_add_two_pi, sin_add_two_pi] + rw [InitialConditions.trajectory, add_val, period_eq, h, cos_add_two_pi, sin_add_two_pi] rfl TODO "For the classical harmonic oscillator find the time for which it returns to From 5e71e76d287e6094e07ac3d79012df0371afb51e Mon Sep 17 00:00:00 2001 From: Bergschaf Date: Mon, 4 May 2026 18:33:18 +0200 Subject: [PATCH 7/8] docstring --- .../HarmonicOscillator/Solution.lean | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/Physlib/ClassicalMechanics/HarmonicOscillator/Solution.lean b/Physlib/ClassicalMechanics/HarmonicOscillator/Solution.lean index 858261c5e..f5f46d8d7 100644 --- a/Physlib/ClassicalMechanics/HarmonicOscillator/Solution.lean +++ b/Physlib/ClassicalMechanics/HarmonicOscillator/Solution.lean @@ -841,14 +841,6 @@ lemma trajectory_velocity_eq_zero_iff (IC : InitialConditions) (t : Time) : rw [pow_ne_zero_iff ?_] apply ω_ne_zero exact Ne.symm (Nat.zero_ne_add_one 1) -/-! - -## F. Some open TODOs - -We give some open TODOs for the classical harmonic oscillator. - --/ - end InitialConditions /-- @@ -876,6 +868,14 @@ lemma trajectory_periodic (IC : InitialConditions) : rw [InitialConditions.trajectory, add_val, period_eq, h, cos_add_two_pi, sin_add_two_pi] rfl +/-! + +## F. Some open TODOs + +We give some open TODOs for the classical harmonic oscillator. + +-/ + TODO "For the classical harmonic oscillator find the time for which it returns to it's initial position and velocity." From d9c9d549b43b9b2fd399f1c31abee0031ab63fa3 Mon Sep 17 00:00:00 2001 From: Bergschaf Date: Tue, 5 May 2026 08:41:24 +0200 Subject: [PATCH 8/8] inherit doc --- Physlib/ClassicalMechanics/HarmonicOscillator/Solution.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Physlib/ClassicalMechanics/HarmonicOscillator/Solution.lean b/Physlib/ClassicalMechanics/HarmonicOscillator/Solution.lean index f5f46d8d7..8b3ae69a4 100644 --- a/Physlib/ClassicalMechanics/HarmonicOscillator/Solution.lean +++ b/Physlib/ClassicalMechanics/HarmonicOscillator/Solution.lean @@ -848,6 +848,7 @@ The period of a harmonic oscillator is `2 * π / ω`. -/ noncomputable def period (S : HarmonicOscillator) : ℝ := 2 * π / S.ω +@[inherit_doc period] scoped notation "T" => HarmonicOscillator.period lemma period_eq : T S = 2 * π / S.ω := rfl