diff --git a/PhysLean/ClassicalMechanics/HarmonicOscillator/Basic.lean b/PhysLean/ClassicalMechanics/HarmonicOscillator/Basic.lean index 8fb67ab8..0ff65919 100644 --- a/PhysLean/ClassicalMechanics/HarmonicOscillator/Basic.lean +++ b/PhysLean/ClassicalMechanics/HarmonicOscillator/Basic.lean @@ -6,6 +6,7 @@ Authors: Joseph Tooby-Smith, Lode Vermeulen import PhysLean.Meta.Informal.SemiFormal import PhysLean.ClassicalMechanics.EulerLagrange import PhysLean.ClassicalMechanics.HamiltonsEquations +import PhysLean.ClassicalMechanics.HarmonicOscillator.ConfigurationSpace /-! # The Classical Harmonic Oscillator @@ -109,8 +110,6 @@ structure HarmonicOscillator where namespace HarmonicOscillator -TODO "U7UG2" "Refactor the Harmonic oscillator API to be configuration space of the - harmonic oscillator." variable (S : HarmonicOscillator) @@ -180,15 +179,15 @@ of the harmonic oscillator, through the lagrangian. -/ /-- The kinetic energy of the harmonic oscillator is $\frac{1}{2} m ‖\dot x‖^2$. -/ -noncomputable def kineticEnergy (xₜ : Time → EuclideanSpace ℝ (Fin 1)) : Time → ℝ := fun t => +noncomputable def kineticEnergy (xₜ : Time → ConfigurationSpace) : Time → ℝ := fun t => (1 / (2 : ℝ)) * S.m * ⟪∂ₜ xₜ t, ∂ₜ xₜ t⟫_ℝ /-- The potential energy of the harmonic oscillator is `1/2 k x ^ 2` -/ -noncomputable def potentialEnergy (x : EuclideanSpace ℝ (Fin 1)) : ℝ := +noncomputable def potentialEnergy (x : ConfigurationSpace) : ℝ := (1 / (2 : ℝ)) • S.k • ⟪x, x⟫_ℝ /-- The energy of the harmonic oscillator is the kinetic energy plus the potential energy. -/ -noncomputable def energy (xₜ : Time → EuclideanSpace ℝ (Fin 1)) : Time → ℝ := fun t => +noncomputable def energy (xₜ : Time → ConfigurationSpace) : Time → ℝ := fun t => kineticEnergy S xₜ t + potentialEnergy S (xₜ t) /-! @@ -197,13 +196,13 @@ noncomputable def energy (xₜ : Time → EuclideanSpace ℝ (Fin 1)) : Time → -/ -lemma kineticEnergy_eq (xₜ : Time → EuclideanSpace ℝ (Fin 1)) : +lemma kineticEnergy_eq (xₜ : Time → ConfigurationSpace) : kineticEnergy S xₜ = fun t => (1 / (2 : ℝ)) * S.m * ⟪∂ₜ xₜ t, ∂ₜ xₜ t⟫_ℝ:= by rfl -lemma potentialEnergy_eq (x : EuclideanSpace ℝ (Fin 1)) : +lemma potentialEnergy_eq (x : ConfigurationSpace) : potentialEnergy S x = (1 / (2 : ℝ)) • S.k • ⟪x, x⟫_ℝ:= by rfl -lemma energy_eq (xₜ : Time → EuclideanSpace ℝ (Fin 1)) : +lemma energy_eq (xₜ : Time → ConfigurationSpace) : energy S xₜ = fun t => kineticEnergy S xₜ t + potentialEnergy S (xₜ t) := by rfl /-! @@ -213,7 +212,7 @@ On smooth trajectories the energies are differentiable. -/ @[fun_prop] -lemma kineticEnergy_differentiable (xₜ : Time → EuclideanSpace ℝ (Fin 1)) (hx : ContDiff ℝ ∞ xₜ) : +lemma kineticEnergy_differentiable (xₜ : Time → ConfigurationSpace) (hx : ContDiff ℝ ∞ xₜ) : Differentiable ℝ (kineticEnergy S xₜ) := by rw [kineticEnergy_eq] change Differentiable ℝ ((fun x => (1 / (2 : ℝ)) * S.m * ⟪x, x⟫_ℝ) ∘ (fun t => ∂ₜ xₜ t)) @@ -222,7 +221,7 @@ lemma kineticEnergy_differentiable (xₜ : Time → EuclideanSpace ℝ (Fin 1)) · exact deriv_differentiable_of_contDiff xₜ hx @[fun_prop] -lemma potentialEnergy_differentiable (xₜ : Time → EuclideanSpace ℝ (Fin 1)) (hx : ContDiff ℝ ∞ xₜ) : +lemma potentialEnergy_differentiable (xₜ : Time → ConfigurationSpace) (hx : ContDiff ℝ ∞ xₜ) : Differentiable ℝ (fun t => potentialEnergy S (xₜ t)) := by simp only [potentialEnergy_eq, one_div, smul_eq_mul] change Differentiable ℝ ((fun x => 2⁻¹ * (S.k * ⟪x, x⟫_ℝ)) ∘ xₜ) @@ -232,7 +231,7 @@ lemma potentialEnergy_differentiable (xₜ : Time → EuclideanSpace ℝ (Fin 1) exact hx.1 @[fun_prop] -lemma energy_differentiable (xₜ : Time → EuclideanSpace ℝ (Fin 1)) (hx : ContDiff ℝ ∞ xₜ) : +lemma energy_differentiable (xₜ : Time → ConfigurationSpace) (hx : ContDiff ℝ ∞ xₜ) : Differentiable ℝ (energy S xₜ) := by rw [energy_eq] fun_prop @@ -246,7 +245,7 @@ the time derivatives of the energies. -/ -lemma kineticEnergy_deriv (xₜ : Time → EuclideanSpace ℝ (Fin 1)) (hx : ContDiff ℝ ∞ xₜ) : +lemma kineticEnergy_deriv (xₜ : Time → ConfigurationSpace) (hx : ContDiff ℝ ∞ xₜ) : ∂ₜ (kineticEnergy S xₜ) = fun t => ⟪∂ₜ xₜ t, S.m • ∂ₜ (∂ₜ xₜ) t⟫_ℝ := by funext t unfold kineticEnergy @@ -264,7 +263,7 @@ lemma kineticEnergy_deriv (xₜ : Time → EuclideanSpace ℝ (Fin 1)) (hx : Con module repeat fun_prop -lemma potentialEnergy_deriv (xₜ : Time → EuclideanSpace ℝ (Fin 1)) (hx : ContDiff ℝ ∞ xₜ) : +lemma potentialEnergy_deriv (xₜ : Time → ConfigurationSpace) (hx : ContDiff ℝ ∞ xₜ) : ∂ₜ (fun t => potentialEnergy S (xₜ t)) = fun t => ⟪∂ₜ xₜ t, S.k • xₜ t⟫_ℝ := by funext t unfold potentialEnergy @@ -287,7 +286,7 @@ lemma potentialEnergy_deriv (xₜ : Time → EuclideanSpace ℝ (Fin 1)) (hx : C rw [contDiff_infty_iff_fderiv] at hx exact hx.1 -lemma energy_deriv (xₜ : Time → EuclideanSpace ℝ (Fin 1)) (hx : ContDiff ℝ ∞ xₜ) : +lemma energy_deriv (xₜ : Time → ConfigurationSpace) (hx : ContDiff ℝ ∞ xₜ) : ∂ₜ (energy S xₜ) = fun t => ⟪∂ₜ xₜ t, S.m • ∂ₜ (∂ₜ xₜ) t + S.k • xₜ t⟫_ℝ := by unfold energy funext t @@ -324,8 +323,8 @@ to make the lagrangian a function on phase-space we reserve this result for a le set_option linter.unusedVariables false in /-- The lagrangian of the harmonic oscillator is the kinetic energy minus the potential energy. -/ @[nolint unusedArguments] -noncomputable def lagrangian (t : Time) (x : EuclideanSpace ℝ (Fin 1)) - (v : EuclideanSpace ℝ (Fin 1)) : ℝ := +noncomputable def lagrangian (t : Time) (x : ConfigurationSpace) + (v : ConfigurationSpace) : ℝ := 1 / (2 : ℝ) * S.m * ⟪v, v⟫_ℝ - S.potentialEnergy x /-! @@ -346,7 +345,7 @@ lemma lagrangian_eq : lagrangian S = fun t x v => ring lemma lagrangian_eq_kineticEnergy_sub_potentialEnergy (t : Time) - (xₜ : Time → EuclideanSpace ℝ (Fin 1)) : + (xₜ : Time → ConfigurationSpace) : lagrangian S t (xₜ t) (∂ₜ xₜ t) = kineticEnergy S xₜ t - potentialEnergy S (xₜ t) := by rw [lagrangian_eq, kineticEnergy, potentialEnergy] simp only [one_div, smul_eq_mul, sub_right_inj] @@ -365,6 +364,45 @@ lemma contDiff_lagrangian (n : WithTop ℕ∞) : ContDiff ℝ n ↿S.lagrangian rw [lagrangian_eq] fun_prop +lemma toDual_symm_innerSL (x : ConfigurationSpace) : + (InnerProductSpace.toDual ℝ ConfigurationSpace).symm (innerSL ℝ x) = x := by + apply (innerSL_inj (𝕜:=ℝ) (E:=ConfigurationSpace)).1 + ext y + simp [InnerProductSpace.toDual_symm_apply] + +lemma gradient_inner_self (x : ConfigurationSpace) : + gradient (fun y : ConfigurationSpace => ⟪y, y⟫_ℝ) x = (2 : ℝ) • x := by + have h_inner : (fun y : ConfigurationSpace => ⟪y, y⟫_ℝ) = + fun y : ConfigurationSpace => ‖y‖ ^ 2 := by + funext y + simp [real_inner_self_eq_norm_sq] + calc + gradient (fun y : ConfigurationSpace => ⟪y, y⟫_ℝ) x + = (InnerProductSpace.toDual ℝ ConfigurationSpace).symm + (fderiv ℝ (fun y : ConfigurationSpace => ⟪y, y⟫_ℝ) x) := rfl + _ = (InnerProductSpace.toDual ℝ ConfigurationSpace).symm (2 • innerSL ℝ x) := by + simp [h_inner, fderiv_norm_sq_apply] + _ = (2 : ℝ) • (InnerProductSpace.toDual ℝ ConfigurationSpace).symm (innerSL ℝ x) := by + simp [map_smul] + _ = (2 : ℝ) • x := by + simp [toDual_symm_innerSL] + +lemma gradient_const_mul_inner_self (c : ℝ) (x : ConfigurationSpace) : + gradient (fun y : ConfigurationSpace => c * ⟪y, y⟫_ℝ) x = (2 * c) • x := by + calc + gradient (fun y : ConfigurationSpace => c * ⟪y, y⟫_ℝ) x + = (InnerProductSpace.toDual ℝ ConfigurationSpace).symm + (fderiv ℝ (fun y : ConfigurationSpace => c * ⟪y, y⟫_ℝ) x) := rfl + _ = (InnerProductSpace.toDual ℝ ConfigurationSpace).symm + (c • fderiv ℝ (fun y : ConfigurationSpace => ⟪y, y⟫_ℝ) x) := by + rw [fderiv_const_mul (by fun_prop)] + _ = c • gradient (fun y : ConfigurationSpace => ⟪y, y⟫_ℝ) x := by + simp [gradient, map_smul] + _ = c • ((2 : ℝ) • x) := by + simp [gradient_inner_self] + _ = (2 * c) • x := by + simp [smul_smul, mul_comm, mul_left_comm, mul_assoc] + /-! #### D.1.3. Gradients of the lagrangian @@ -374,48 +412,33 @@ position and velocity. -/ -lemma gradient_lagrangian_position_eq (t : Time) (x : EuclideanSpace ℝ (Fin 1)) - (v : EuclideanSpace ℝ (Fin 1)) : +lemma gradient_lagrangian_position_eq (t : Time) (x : ConfigurationSpace) + (v : ConfigurationSpace) : gradient (fun x => lagrangian S t x v) x = - S.k • x := by - simp only [lagrangian_eq, one_div, neg_smul] - rw [Space.euclid_gradient_eq_sum] - simp [-inner_self_eq_norm_sq_to_K] - rw [fderiv_fun_sub (by fun_prop) (by fun_prop)] - simp only [fderiv_fun_const, Pi.zero_apply, zero_sub, Fin.isValue, ContinuousLinearMap.neg_apply, - neg_smul, neg_inj] - rw [fderiv_const_mul (by fun_prop)] - simp only [inner_self_eq_norm_sq_to_K, ringHom_apply, fderiv_norm_sq_apply, Fin.isValue, - ContinuousLinearMap.coe_smul', coe_innerSL_apply, nsmul_eq_mul, Nat.cast_ofNat, Pi.smul_apply, - Pi.mul_apply, Pi.ofNat_apply, EuclideanSpace.inner_single_right, smul_eq_mul] - have hx : x = x 0 • EuclideanSpace.single 0 1 := by - ext i - fin_cases i - simp - rw [hx] - simp [smul_smul] - congr 1 - field_simp - -lemma gradient_lagrangian_velocity_eq (t : Time) (x : EuclideanSpace ℝ (Fin 1)) - (v : EuclideanSpace ℝ (Fin 1)) : + have h_grad : + gradient (fun y : ConfigurationSpace => (-(1 / (2 : ℝ)) * S.k) * ⟪y, y⟫_ℝ) x = + (2 * (-(1 / (2 : ℝ)) * S.k)) • x := by + simpa using (gradient_const_mul_inner_self (c := (-(1 / (2 : ℝ)) * S.k)) x) + have h_lag : + (fun y : ConfigurationSpace => lagrangian S t y v) = + fun y : ConfigurationSpace => (-(1 / (2 : ℝ)) * S.k) * ⟪y, y⟫_ℝ := by + funext y + simp [lagrangian_eq] + simpa [h_lag, smul_smul, mul_comm, mul_left_comm, mul_assoc] using h_grad + +lemma gradient_lagrangian_velocity_eq (t : Time) (x : ConfigurationSpace) + (v : ConfigurationSpace) : gradient (lagrangian S t x) v = S.m • v := by - simp [lagrangian_eq, -inner_self_eq_norm_sq_to_K] - rw [Space.euclid_gradient_eq_sum] - simp [-inner_self_eq_norm_sq_to_K] - rw [fderiv_fun_sub (by fun_prop) (by fun_prop)] - simp only [fderiv_fun_const, Pi.zero_apply, sub_zero, Fin.isValue] - rw [fderiv_const_mul (by fun_prop)] - simp only [inner_self_eq_norm_sq_to_K, ringHom_apply, fderiv_norm_sq_apply, Fin.isValue, - ContinuousLinearMap.coe_smul', coe_innerSL_apply, nsmul_eq_mul, Nat.cast_ofNat, Pi.smul_apply, - Pi.mul_apply, Pi.ofNat_apply, EuclideanSpace.inner_single_right, smul_eq_mul] - have hx : v = v 0 • EuclideanSpace.single 0 1 := by - ext i - fin_cases i - simp - rw [hx] - simp [smul_smul] - congr 1 - field_simp + have h_grad : + gradient (fun y : ConfigurationSpace => ((1 / (2 : ℝ)) * S.m) * ⟪y, y⟫_ℝ) v = + (2 * ((1 / (2 : ℝ)) * S.m)) • v := by + simpa using (gradient_const_mul_inner_self (c := ((1 / (2 : ℝ)) * S.m)) v) + have h_lag : + (fun y : ConfigurationSpace => lagrangian S t x y) = + fun y : ConfigurationSpace => ((1 / (2 : ℝ)) * S.m) * ⟪y, y⟫_ℝ := by + funext y + simp [lagrangian_eq] + simpa [h_lag, smul_smul, mul_comm, mul_left_comm, mul_assoc] using h_grad /-! @@ -433,8 +456,8 @@ equation of motion. -/ /-- The Euler-Lagrange operator for the classical harmonic oscillator. -/ -noncomputable def gradLagrangian (xₜ : Time → EuclideanSpace ℝ (Fin 1)) : - Time → EuclideanSpace ℝ (Fin 1) := +noncomputable def gradLagrangian (xₜ : Time → ConfigurationSpace) : + Time → ConfigurationSpace := (δ (q':=xₜ), ∫ t, lagrangian S t (q' t) (fderiv ℝ q' t 1)) /-! @@ -445,7 +468,7 @@ Basic equalities for the variational derivative of the action. -/ -lemma gradLagrangian_eq_eulerLagrangeOp (xₜ : Time → EuclideanSpace ℝ (Fin 1)) +lemma gradLagrangian_eq_eulerLagrangeOp (xₜ : Time → ConfigurationSpace) (hq : ContDiff ℝ ∞ xₜ) : gradLagrangian S xₜ = eulerLagrangeOp S.lagrangian xₜ := by rw [gradLagrangian, @@ -461,7 +484,7 @@ variational derivative of the action equal to zero. -/ /-- The equation of motion for the Harmonic oscillator. -/ -def EquationOfMotion (xₜ : Time → EuclideanSpace ℝ (Fin 1)) : Prop := +def EquationOfMotion (xₜ : Time → ConfigurationSpace) : Prop := S.gradLagrangian xₜ = 0 /-! @@ -472,7 +495,7 @@ We write a simple iff statement for the definition of the equation of motions. -/ -lemma equationOfMotion_iff_gradLagrangian_zero (xₜ : Time → EuclideanSpace ℝ (Fin 1)) : +lemma equationOfMotion_iff_gradLagrangian_zero (xₜ : Time → ConfigurationSpace) : S.EquationOfMotion xₜ ↔ S.gradLagrangian xₜ = 0 := by rfl /-! @@ -495,8 +518,8 @@ and show that this is equal to `- k x`. /-- The force of the classical harmonic oscillator defined as `- dU(x)/dx` where `U(x)` is the potential energy. -/ -noncomputable def force (S : HarmonicOscillator) (x : EuclideanSpace ℝ (Fin 1)) : - EuclideanSpace ℝ (Fin 1) := +noncomputable def force (S : HarmonicOscillator) (x : ConfigurationSpace) : + ConfigurationSpace := - gradient (potentialEnergy S) x /-! @@ -508,11 +531,11 @@ We now show that the force is equal to `- k x`. -/ /-- The force on the classical harmonic oscillator is `- k x`. -/ -lemma force_eq_linear (x : EuclideanSpace ℝ (Fin 1)) : force S x = - S.k • x := by +lemma force_eq_linear (x : ConfigurationSpace) : force S x = - S.k • x := by simp [force] refine ext_inner_right (𝕜 := ℝ) fun y => ?_ simp [gradient] - change fderiv ℝ ((1 / (2 : ℝ)) • S.k • (fun (x : EuclideanSpace ℝ (Fin 1)) => ⟪x, x⟫_ℝ)) x y = _ + change fderiv ℝ ((1 / (2 : ℝ)) • S.k • (fun (x : ConfigurationSpace) => ⟪x, x⟫_ℝ)) x y = _ rw [fderiv_const_smul (by fun_prop), fderiv_const_smul (by fun_prop)] simp [inner_smul_left] ring @@ -527,28 +550,13 @@ to Newton's second law. -/ /-- The Euler lagrange operator corresponds to Newton's second law. -/ -lemma gradLagrangian_eq_force (xₜ : Time → EuclideanSpace ℝ (Fin 1)) (hx : ContDiff ℝ ∞ xₜ) : +lemma gradLagrangian_eq_force (xₜ : Time → ConfigurationSpace) (hx : ContDiff ℝ ∞ xₜ) : S.gradLagrangian xₜ = fun t => force S (xₜ t) - S.m • ∂ₜ (∂ₜ xₜ) t := by funext t rw [gradLagrangian_eq_eulerLagrangeOp S xₜ hx, eulerLagrangeOp] simp only congr - · simp [lagrangian_eq, -inner_self_eq_norm_sq_to_K] - rw [Space.euclid_gradient_eq_sum] - simp [-inner_self_eq_norm_sq_to_K] - rw [fderiv_fun_sub (by fun_prop) (by fun_prop)] - simp only [fderiv_fun_const, Pi.zero_apply, zero_sub, Fin.isValue, - ContinuousLinearMap.neg_apply, neg_smul] - rw [fderiv_const_mul (by fun_prop)] - simp [force_eq_linear] - have hx : xₜ t = xₜ t 0 • EuclideanSpace.single 0 1 := by - ext i - fin_cases i - simp - rw [hx] - simp [smul_smul, inner_smul_left] - congr 1 - field_simp + · simp [gradient_lagrangian_position_eq, force_eq_linear] · rw [← Time.deriv_smul _ _ (by fun_prop)] congr funext t @@ -562,7 +570,7 @@ We show that the equation of motion is equivalent to Newton's second law. -/ -lemma equationOfMotion_iff_newtons_2nd_law (xₜ : Time → EuclideanSpace ℝ (Fin 1)) +lemma equationOfMotion_iff_newtons_2nd_law (xₜ : Time → ConfigurationSpace) (hx : ContDiff ℝ ∞ xₜ) : S.EquationOfMotion xₜ ↔ (∀ t, S.m • ∂ₜ (∂ₜ xₜ) t = force S (xₜ t)) := by @@ -592,7 +600,7 @@ the equation of motion. -/ -lemma energy_conservation_of_equationOfMotion (xₜ : Time → EuclideanSpace ℝ (Fin 1)) +lemma energy_conservation_of_equationOfMotion (xₜ : Time → ConfigurationSpace) (hx : ContDiff ℝ ∞ xₜ) (h : S.EquationOfMotion xₜ) : ∂ₜ (S.energy xₜ) = 0 := by rw [energy_deriv _ _ hx] @@ -610,7 +618,7 @@ We prove that the energy is constant for any trajectory satisfying the equation -/ -lemma energy_conservation_of_equationOfMotion' (xₜ : Time → EuclideanSpace ℝ (Fin 1)) +lemma energy_conservation_of_equationOfMotion' (xₜ : Time → ConfigurationSpace) (hx : ContDiff ℝ ∞ xₜ) (h : S.EquationOfMotion xₜ) (t : Time) : S.energy xₜ t = S.energy xₜ 0 := by have h1 := S.energy_conservation_of_equationOfMotion xₜ hx h @@ -647,8 +655,8 @@ the velocity. -/ /-- The equivalence between velocity and canonical momentum. -/ -noncomputable def toCanonicalMomentum (t : Time) (x : EuclideanSpace ℝ (Fin 1)) : - EuclideanSpace ℝ (Fin 1) ≃ₗ[ℝ] EuclideanSpace ℝ (Fin 1) where +noncomputable def toCanonicalMomentum (t : Time) (x : ConfigurationSpace) : + ConfigurationSpace ≃ₗ[ℝ] ConfigurationSpace where toFun v := gradient (S.lagrangian t x ·) v invFun p := (1 / S.m) • p left_inv v := by @@ -669,8 +677,8 @@ An simple equality for the canonical momentum. -/ -lemma toCanonicalMomentum_eq (t : Time) (x : EuclideanSpace ℝ (Fin 1)) - (v : EuclideanSpace ℝ (Fin 1)) : +lemma toCanonicalMomentum_eq (t : Time) (x : ConfigurationSpace) + (v : ConfigurationSpace) : toCanonicalMomentum S t x v = S.m • v := by simp [toCanonicalMomentum, gradient_lagrangian_velocity_eq] @@ -687,8 +695,8 @@ where `v` is a function of `p` and `x` through the canonical momentum. -/ /-- The hamiltonian as a function of time, momentum and position. -/ -noncomputable def hamiltonian (t : Time) (p : EuclideanSpace ℝ (Fin 1)) - (x : EuclideanSpace ℝ (Fin 1)) : ℝ := +noncomputable def hamiltonian (t : Time) (p : ConfigurationSpace) + (x : ConfigurationSpace) : ℝ := ⟪p, (toCanonicalMomentum S t x).symm p⟫_ℝ - S.lagrangian t x ((toCanonicalMomentum S t x).symm p) /-! @@ -730,47 +738,33 @@ We now write down the gradients of the Hamiltonian with respect to the momentum -/ -lemma gradient_hamiltonian_position_eq (t : Time) (x : EuclideanSpace ℝ (Fin 1)) - (p : EuclideanSpace ℝ (Fin 1)) : +lemma gradient_hamiltonian_position_eq (t : Time) (x : ConfigurationSpace) + (p : ConfigurationSpace) : gradient (hamiltonian S t p) x = S.k • x := by - rw [hamiltonian_eq] - simp only [one_div] - rw [Space.euclid_gradient_eq_sum] - simp only [Finset.univ_unique, Fin.default_eq_zero, Fin.isValue, fderiv_const_add, - Finset.sum_singleton] - rw [fderiv_const_mul (by fun_prop)] - simp only [inner_self_eq_norm_sq_to_K, ringHom_apply, fderiv_norm_sq_apply, Fin.isValue, - ContinuousLinearMap.coe_smul', coe_innerSL_apply, nsmul_eq_mul, Nat.cast_ofNat, Pi.smul_apply, - Pi.mul_apply, Pi.ofNat_apply, EuclideanSpace.inner_single_right, smul_eq_mul] - have hx : x = x 0 • EuclideanSpace.single 0 1 := by - ext i - fin_cases i - simp - rw [hx] - simp only [Fin.isValue, PiLp.smul_apply, EuclideanSpace.single_apply, ↓reduceIte, smul_eq_mul, - mul_one, one_mul] - module - -lemma gradient_hamiltonian_momentum_eq (t : Time) (x : EuclideanSpace ℝ (Fin 1)) - (p : EuclideanSpace ℝ (Fin 1)) : + have h_grad : + gradient (fun y : ConfigurationSpace => ((1 / (2 : ℝ)) * S.k) * ⟪y, y⟫_ℝ) x = + (2 * ((1 / (2 : ℝ)) * S.k)) • x := by + simpa using (gradient_const_mul_inner_self (c := ((1 / (2 : ℝ)) * S.k)) x) + have h_ham : + (fun y : ConfigurationSpace => hamiltonian S t p y) = + fun y : ConfigurationSpace => ((1 / (2 : ℝ)) * S.k) * ⟪y, y⟫_ℝ := by + funext y + simp [hamiltonian_eq] + simpa [h_ham, smul_smul, mul_comm, mul_left_comm, mul_assoc] using h_grad + +lemma gradient_hamiltonian_momentum_eq (t : Time) (x : ConfigurationSpace) + (p : ConfigurationSpace) : gradient (hamiltonian S t · x) p = (1 / S.m) • p := by - rw [hamiltonian_eq] - simp only [one_div] - rw [Space.euclid_gradient_eq_sum] - simp only [Finset.univ_unique, Fin.default_eq_zero, Fin.isValue, fderiv_add_const, - Finset.sum_singleton] - rw [fderiv_const_mul (by fun_prop)] - simp only [inner_self_eq_norm_sq_to_K, ringHom_apply, fderiv_norm_sq_apply, Fin.isValue, - ContinuousLinearMap.coe_smul', coe_innerSL_apply, nsmul_eq_mul, Nat.cast_ofNat, Pi.smul_apply, - Pi.mul_apply, Pi.ofNat_apply, EuclideanSpace.inner_single_right, smul_eq_mul] - have hx : p = p 0 • EuclideanSpace.single 0 1 := by - ext i - fin_cases i - simp - rw [hx] - simp only [Fin.isValue, PiLp.smul_apply, EuclideanSpace.single_apply, ↓reduceIte, smul_eq_mul, - mul_one, one_mul] - module + have h_grad : + gradient (fun y : ConfigurationSpace => ((1 / (2 : ℝ)) * (1 / S.m)) * ⟪y, y⟫_ℝ) p = + (2 * ((1 / (2 : ℝ)) * (1 / S.m))) • p := by + simpa using (gradient_const_mul_inner_self (c := ((1 / (2 : ℝ)) * (1 / S.m))) p) + have h_ham : + (fun y : ConfigurationSpace => hamiltonian S t y x) = + fun y : ConfigurationSpace => ((1 / (2 : ℝ)) * (1 / S.m)) * ⟪y, y⟫_ℝ := by + funext y + simp [hamiltonian_eq] + simpa [h_ham, smul_smul, mul_comm, mul_left_comm, mul_assoc] using h_grad /-! @@ -781,7 +775,7 @@ This is independent of whether the trajectory satisfies the equations of motion -/ -lemma hamiltonian_eq_energy (xₜ : Time → EuclideanSpace ℝ (Fin 1)) : +lemma hamiltonian_eq_energy (xₜ : Time → ConfigurationSpace) : (fun t => hamiltonian S t (toCanonicalMomentum S t (xₜ t) (∂ₜ xₜ t)) (xₜ t)) = energy S xₜ := by funext t rw [hamiltonian] @@ -800,8 +794,8 @@ to Hamilton's equations. /-- The operator on the momentum-position phase-space whose vanishing is equivalent to the hamilton's equations between the momentum and position. -/ -noncomputable def hamiltonEqOp (p : Time → EuclideanSpace ℝ (Fin 1)) - (q : Time → EuclideanSpace ℝ (Fin 1)) := +noncomputable def hamiltonEqOp (p : Time → ConfigurationSpace) + (q : Time → ConfigurationSpace) := ClassicalMechanics.hamiltonEqOp (hamiltonian S) p q /-! @@ -813,7 +807,7 @@ to the vanishing of the Hamilton equation operator. -/ -lemma equationOfMotion_iff_hamiltonEqOp_eq_zero (xₜ : Time → EuclideanSpace ℝ (Fin 1)) +lemma equationOfMotion_iff_hamiltonEqOp_eq_zero (xₜ : Time → ConfigurationSpace) (hx : ContDiff ℝ ∞ xₜ) : S.EquationOfMotion xₜ ↔ hamiltonEqOp S (fun t => S.toCanonicalMomentum t (xₜ t) (∂ₜ xₜ t)) xₜ = 0 := by rw [hamiltonEqOp, hamiltonEqOp_eq_zero_iff_hamiltons_equations] @@ -835,7 +829,7 @@ We show that the following are equivalent statements for a smooth trajectory `x -/ -lemma equationOfMotion_tfae (xₜ : Time → EuclideanSpace ℝ (Fin 1)) (hx : ContDiff ℝ ∞ xₜ) : +lemma equationOfMotion_tfae (xₜ : Time → ConfigurationSpace) (hx : ContDiff ℝ ∞ xₜ) : List.TFAE [S.EquationOfMotion xₜ, (∀ t, S.m • ∂ₜ (∂ₜ xₜ) t = force S (xₜ t)), hamiltonEqOp S (fun t => S.toCanonicalMomentum t (xₜ t) (∂ₜ xₜ t)) xₜ = 0, diff --git a/PhysLean/ClassicalMechanics/HarmonicOscillator/ConfigurationSpace.lean b/PhysLean/ClassicalMechanics/HarmonicOscillator/ConfigurationSpace.lean new file mode 100644 index 00000000..9dc9d7b1 --- /dev/null +++ b/PhysLean/ClassicalMechanics/HarmonicOscillator/ConfigurationSpace.lean @@ -0,0 +1,260 @@ +/- +Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joseph Tooby-Smith, Lode Vermeulen +-/ +import Mathlib.Analysis.InnerProductSpace.Basic +import Mathlib.Geometry.Manifold.Diffeomorph +import Mathlib.LinearAlgebra.FiniteDimensional.Basic +import PhysLean.SpaceAndTime.Space.Basic +import PhysLean.SpaceAndTime.Time.Basic +/-! +# Configuration space of the harmonic oscillator + +The configuration space is defined as a one-dimensional smooth manifold, +modeled on `ℝ`, with a chosen coordinate. +-/ + +namespace ClassicalMechanics + +namespace HarmonicOscillator + +/-- The configuration space of the harmonic oscillator. -/ +structure ConfigurationSpace where + /-- The underlying real coordinate. -/ + val : ℝ + +namespace ConfigurationSpace + +@[ext] +lemma ext {x y : ConfigurationSpace} (h : x.val = y.val) : x = y := by + cases x + cases y + simp at h + simp [h] + +/-! +## Algebraic and analytical structure +-/ + +instance : Zero ConfigurationSpace := { zero := ⟨0⟩ } + +instance : OfNat ConfigurationSpace 0 := { ofNat := ⟨0⟩ } + +@[simp] +lemma zero_val : (0 : ConfigurationSpace).val = 0 := rfl + +instance : Add ConfigurationSpace where + add x y := ⟨x.val + y.val⟩ + +@[simp] +lemma add_val (x y : ConfigurationSpace) : (x + y).val = x.val + y.val := rfl + +instance : Neg ConfigurationSpace where + neg x := ⟨-x.val⟩ + +@[simp] +lemma neg_val (x : ConfigurationSpace) : (-x).val = -x.val := rfl + +instance : Sub ConfigurationSpace where + sub x y := ⟨x.val - y.val⟩ + +@[simp] +lemma sub_val (x y : ConfigurationSpace) : (x - y).val = x.val - y.val := rfl + +instance : SMul ℝ ConfigurationSpace where + smul r x := ⟨r * x.val⟩ + +@[simp] +lemma smul_val (r : ℝ) (x : ConfigurationSpace) : (r • x).val = r * x.val := rfl + +instance : CoeFun ConfigurationSpace (fun _ => Fin 1 → ℝ) where + coe x := fun _ => x.val + +@[simp] +lemma apply_zero (x : ConfigurationSpace) : x 0 = x.val := rfl + +@[simp] +lemma apply_eq_val (x : ConfigurationSpace) (i : Fin 1) : x i = x.val := rfl + +instance : AddGroup ConfigurationSpace where + add_assoc x y z := by ext; simp [add_assoc] + zero_add x := by ext; simp [zero_add] + add_zero x := by ext; simp [add_zero] + neg_add_cancel x := by ext; simp [neg_add_cancel] + nsmul := nsmulRec + zsmul := zsmulRec + +instance : AddCommGroup ConfigurationSpace where + add_comm x y := by ext; simp [add_comm] + +instance : Module ℝ ConfigurationSpace where + one_smul x := by ext; simp + smul_add r x y := by ext; simp [mul_add] + smul_zero r := by ext; simp [mul_zero] + add_smul r s x := by ext; simp [add_mul] + mul_smul r s x := by ext; simp [mul_assoc] + zero_smul x := by ext; simp + +instance : Norm ConfigurationSpace where + norm x := ‖x.val‖ + +instance : Dist ConfigurationSpace where + dist x y := ‖x - y‖ + +lemma dist_eq_val (x y : ConfigurationSpace) : + dist x y = ‖x.val - y.val‖ := rfl + +instance : SeminormedAddCommGroup ConfigurationSpace where + dist_self x := by simp [dist_eq_val] + dist_comm x y := by + simpa [dist_eq_val, Real.dist_eq] using (dist_comm x.val y.val) + dist_triangle x y z := by + simpa [dist_eq_val, Real.dist_eq] using (dist_triangle x.val y.val z.val) + +instance : NormedAddCommGroup ConfigurationSpace where + eq_of_dist_eq_zero := by + intro a b h + ext + have h' : dist a.val b.val = 0 := by + simpa [dist_eq_val, Real.dist_eq] using h + exact dist_eq_zero.mp h' + +instance : NormedSpace ℝ ConfigurationSpace where + norm_smul_le r x := by + simp [norm, smul_val, abs_mul] + +open InnerProductSpace + +instance : Inner ℝ ConfigurationSpace where + inner x y := x.val * y.val + +@[simp] +lemma inner_def (x y : ConfigurationSpace) : ⟪x, y⟫_ℝ = x.val * y.val := rfl + +noncomputable instance : InnerProductSpace ℝ ConfigurationSpace where + norm_sq_eq_re_inner := by + intro x + have hx : ‖x‖ ^ 2 = x.val ^ 2 := by + simp [norm, sq_abs] + simpa [inner_def, pow_two] using hx + conj_inner_symm := by + intro x y + simp [inner_def] + ring + add_left := by + intro x y z + simp [inner_def, add_mul] + smul_left := by + intro x y r + simp [inner_def] + ring + +@[fun_prop] +lemma differentiable_inner_self : + Differentiable ℝ (fun x : ConfigurationSpace => ⟪x, x⟫_ℝ) := by + have h_id : Differentiable ℝ (fun x : ConfigurationSpace => x) := differentiable_id + simpa using (Differentiable.inner (𝕜:=ℝ) (f:=fun x : ConfigurationSpace => x) + (g:=fun x : ConfigurationSpace => x) h_id h_id) + +@[fun_prop] +lemma differentiableAt_inner_self (x : ConfigurationSpace) : + DifferentiableAt ℝ (fun y : ConfigurationSpace => ⟪y, y⟫_ℝ) x := by + have h_id : DifferentiableAt ℝ (fun y : ConfigurationSpace => y) x := differentiableAt_id + simpa using (DifferentiableAt.inner (𝕜:=ℝ) (f:=fun y : ConfigurationSpace => y) + (g:=fun y : ConfigurationSpace => y) h_id h_id) + +@[fun_prop] +lemma contDiff_inner_self (n : WithTop ℕ∞) : + ContDiff ℝ n (fun x : ConfigurationSpace => ⟪x, x⟫_ℝ) := by + have h_id : ContDiff ℝ n (fun x : ConfigurationSpace => x) := contDiff_id + simpa using (ContDiff.inner (𝕜:=ℝ) (f:=fun x : ConfigurationSpace => x) + (g:=fun x : ConfigurationSpace => x) h_id h_id) + +noncomputable def toRealLM : ConfigurationSpace →ₗ[ℝ] ℝ := + { toFun := ConfigurationSpace.val + map_add' := by simp + map_smul' := by simp } + +noncomputable def fromRealLM : ℝ →ₗ[ℝ] ConfigurationSpace := + { toFun := fun x => ⟨x⟩ + map_add' := by + intro x y + ext + simp + map_smul' := by + intro r x + ext + simp } + +noncomputable def toRealCLM : ConfigurationSpace →L[ℝ] ℝ := + toRealLM.mkContinuous 1 (by + intro x + simp [toRealLM, norm, mul_comm, mul_left_comm, mul_assoc]) + +noncomputable def fromRealCLM : ℝ →L[ℝ] ConfigurationSpace := + fromRealLM.mkContinuous 1 (by + intro x + simp [fromRealLM, norm, mul_comm, mul_left_comm, mul_assoc]) + +noncomputable def valHomeomorphism : ConfigurationSpace ≃ₜ ℝ where + toFun := ConfigurationSpace.val + invFun := fun t => ⟨t⟩ + left_inv := by + intro t + cases t + rfl + right_inv := by + intro t + rfl + continuous_toFun := by + simpa [toRealCLM, toRealLM] using toRealCLM.continuous + continuous_invFun := by + simpa [fromRealCLM, fromRealLM] using fromRealCLM.continuous + +/-- The structure of a charted space on `ConfigurationSpace`. -/ +noncomputable instance : ChartedSpace ℝ ConfigurationSpace where + atlas := { valHomeomorphism.toOpenPartialHomeomorph } + chartAt _ := valHomeomorphism.toOpenPartialHomeomorph + mem_chart_source := by + simp + chart_mem_atlas := by + intro x + simp + +open Manifold ContDiff + +/-- The structure of a smooth manifold on `ConfigurationSpace`. -/ +noncomputable instance : IsManifold 𝓘(ℝ, ℝ) ω ConfigurationSpace where + compatible := by + intro e1 e2 h1 h2 + simp [atlas, ChartedSpace.atlas] at h1 h2 + subst h1 h2 + exact symm_trans_mem_contDiffGroupoid valHomeomorphism.toOpenPartialHomeomorph + +instance : FiniteDimensional ℝ ConfigurationSpace := by + classical + refine FiniteDimensional.of_injective toRealLM ?_ + intro x y h + ext + simpa using h + +instance : CompleteSpace ConfigurationSpace := by + classical + simpa using (FiniteDimensional.complete ℝ ConfigurationSpace) + +/-! +## Map to space +-/ + +/-- The position in one-dimensional space associated to the configuration. -/ +def toSpace (q : ConfigurationSpace) : Space 1 := ⟨fun _ => q.val⟩ + +@[simp] +lemma toSpace_apply (q : ConfigurationSpace) (i : Fin 1) : q.toSpace i = q.val := rfl + +end ConfigurationSpace + +end HarmonicOscillator + +end ClassicalMechanics diff --git a/PhysLean/ClassicalMechanics/HarmonicOscillator/Solution.lean b/PhysLean/ClassicalMechanics/HarmonicOscillator/Solution.lean index 0c0ec77e..5c488627 100644 --- a/PhysLean/ClassicalMechanics/HarmonicOscillator/Solution.lean +++ b/PhysLean/ClassicalMechanics/HarmonicOscillator/Solution.lean @@ -81,9 +81,9 @@ We start by defining the type of initial conditions for the harmonic oscillator. and an initial velocity. -/ structure InitialConditions where /-- The initial position of the harmonic oscillator. -/ - x₀ : EuclideanSpace ℝ (Fin 1) + x₀ : ConfigurationSpace /-- The initial velocity of the harmonic oscillator. -/ - v₀ : EuclideanSpace ℝ (Fin 1) + v₀ : ConfigurationSpace /-! @@ -173,7 +173,7 @@ namespace InitialConditions -/ /-- Given initial conditions, the solution to the classical harmonic oscillator. -/ -noncomputable def trajectory (IC : InitialConditions) : Time → EuclideanSpace ℝ (Fin 1) := fun t => +noncomputable def trajectory (IC : InitialConditions) : Time → ConfigurationSpace := fun t => cos (S.ω * t) • IC.x₀ + (sin (S.ω * t)/S.ω) • IC.v₀ /-! @@ -311,17 +311,14 @@ lemma trajectory_equationOfMotion (IC : InitialConditions) : funext t simp only [Pi.zero_apply] rw [trajectory_acceleration, force_eq_linear] - simp [trajectory_eq] - ext i - simp only [PiLp.sub_apply, PiLp.add_apply, PiLp.neg_apply, PiLp.smul_apply, smul_eq_mul, - PiLp.zero_apply] - rw [ω_sq] + ext + simp [trajectory_eq, smul_add, add_smul, smul_smul, ω_sq, mul_comm, mul_left_comm, mul_assoc] have h : S.ω ≠ 0 := by exact ω_neq_zero S - field_simp + field_simp [h] ring_nf rw [ω_sq] field_simp - simp only [neg_add_cancel, mul_zero] + simp fun_prop /-! @@ -339,7 +336,7 @@ for the given initial conditions. This is currently a TODO. - One may needed the added condition of smoothness on `x` here. - `EquationOfMotion` needs defining before this can be proved. -/ @[sorryful] -lemma trajectories_unique (IC : InitialConditions) (x : Time → EuclideanSpace ℝ (Fin 1)) : +lemma trajectories_unique (IC : InitialConditions) (x : Time → ConfigurationSpace) : S.EquationOfMotion x ∧ x 0 = IC.x₀ ∧ ∂ₜ x 0 = IC.v₀ → x = IC.trajectory S := by sorry @@ -389,8 +386,7 @@ lemma tan_time_eq_of_trajectory_velocity_eq_zero (IC : InitialConditions) (t : T have h1' : IC.x₀ 0 ≠ 0 := by intro hn apply h1 - ext i - fin_cases i + ext simp [hn] have hcos : cos (S.ω * t.val) ≠ 0 := by by_contra hn @@ -402,7 +398,7 @@ lemma tan_time_eq_of_trajectory_velocity_eq_zero (IC : InitialConditions) (t : T trans (sin (S.ω * t.val) * (S.ω * IC.x₀ 0)) + (-(S.ω • sin (S.ω * t.val) • IC.x₀) + cos (S.ω * t.val) • IC.v₀) 0 · rw [h] - simp only [Fin.isValue, PiLp.zero_apply, add_zero] + simp ring · simp ring @@ -427,25 +423,22 @@ the time `arctan (IC.v₀ 0 / (S.ω * IC.x₀ 0)) / S.ω` the velocity is zero. lemma trajectory_velocity_eq_zero_at_arctan (IC : InitialConditions) (hx : IC.x₀ ≠ 0) : (∂ₜ (IC.trajectory S)) (arctan (IC.v₀ 0 / (S.ω * IC.x₀ 0)) / S.ω) = 0 := by rw [trajectory_velocity] - simp only [Fin.isValue, neg_smul] + simp [neg_smul] have hx' : S.ω ≠ 0 := by exact ω_neq_zero S field_simp rw [Real.sin_arctan, Real.cos_arctan] - ext i - fin_cases i - simp only [Fin.isValue, one_div, Fin.zero_eta, PiLp.add_apply, PiLp.neg_apply, PiLp.smul_apply, - smul_eq_mul, PiLp.zero_apply] + ext + simp [one_div, smul_eq_mul] trans (-(S.ω * (IC.v₀ 0 / (S.ω * IC.x₀ 0) * IC.x₀ 0)) + IC.v₀ 0) * (√(1 + (IC.v₀ 0 / (S.ω * IC.x₀ 0)) ^ 2))⁻¹ · ring - simp only [Fin.isValue, mul_eq_zero, inv_eq_zero] + simp [mul_eq_zero, inv_eq_zero] left field_simp have hx : IC.x₀ 0 ≠ 0 := by intro hn apply hx - ext i - fin_cases i + ext simp [hn] field_simp ring