refactor: golf proofs in HarmonicOscillator, IsExtrema, TotalDerivativeEquivalence, KineticTerm

Physlib/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean

@@ -227,7 +227,7 @@ lemma equationOfMotion_iff_newtons_2nd_law (xₜ : Time → EuclideanSpace ℝ (
     have ha :
         S.m • ∂ₜ (∂ₜ xₜ) t = -(S.γ • ∂ₜ xₜ t + S.k • xₜ t) :=
       eq_neg_of_add_eq_zero_left h'
-    simpa [sub_eq_add_neg, neg_add, add_comm] using ha
+    simpa [force, sub_eq_add_neg, neg_add, add_comm] using ha
   · intro h t
     rw [h t]
     module

Physlib/ClassicalMechanics/DampedHarmonicOscillator/Solution.lean

@@ -178,15 +178,13 @@ private lemma exp_decay_smul_velocity
     ∂ₜ (fun t : Time => exp (-a * t.val) • y t) =
       fun t : Time => exp (-a * t.val) • (∂ₜ y t - a • y t) := by
   funext t
-  rw [Time.deriv]
-  rw [fderiv_fun_smul (by fun_prop) (hy t)]
-  rw [fderiv_exp (by fun_prop), fderiv_fun_mul (by fun_prop) (by fun_prop)]
+  rw [Time.deriv, fderiv_fun_smul (by fun_prop) (hy t), fderiv_exp (by fun_prop),
+    fderiv_fun_mul (by fun_prop) (by fun_prop)]
   simp only [add_apply, ContinuousLinearMap.smulRight_apply,
     fderiv_fun_neg, fderiv_fun_const, Pi.zero_apply, Time.fderiv_val,
     _root_.neg_apply, FunLike.coe_smul, Pi.smul_apply, smul_eq_mul]
   rw [← Time.deriv_eq]
-  simp [smul_sub, smul_smul]
-  module
+  simp [smul_smul, sub_eq_add_neg]
 
 private lemma exp_decay_smul_acceleration
     (a μ : ℝ) (y : Time → EuclideanSpace ℝ (Fin 1))
@@ -197,11 +195,9 @@ private lemma exp_decay_smul_acceleration
         (μ • y t - (2 * a) • ∂ₜ y t + a^2 • y t) := by
   rw [exp_decay_smul_velocity a y hy]
   funext t
-  rw [Time.deriv]
-  rw [fderiv_fun_smul (by fun_prop) (by fun_prop)]
-  rw [fderiv_exp (by fun_prop), fderiv_fun_mul (by fun_prop) (by fun_prop)]
-  rw [fderiv_fun_sub (hdy t) (by fun_prop)]
-  rw [fderiv_fun_const_smul (hy t)]
+  rw [Time.deriv, fderiv_fun_smul (by fun_prop) (by fun_prop),
+    fderiv_exp (by fun_prop), fderiv_fun_mul (by fun_prop) (by fun_prop),
+    fderiv_fun_sub (hdy t) (by fun_prop), fderiv_fun_const_smul (hy t)]
   have hy''_t := congrFun hy'' t
   rw [Time.deriv] at hy''_t
   simp only [add_apply, _root_.sub_apply,
@@ -210,7 +206,7 @@ private lemma exp_decay_smul_acceleration
     FunLike.coe_smul, Pi.smul_apply, smul_eq_mul]
   rw [hy''_t, ← Time.deriv_eq]
   simp [smul_add, smul_sub, smul_smul]
-  module
+  ext i; simp; ring
 
 private lemma exp_decay_smul_equationOfMotion
     (a μ : ℝ) (y : Time → EuclideanSpace ℝ (Fin 1))
@@ -219,11 +215,10 @@ private lemma exp_decay_smul_equationOfMotion
     (hγ : S.γ = 2 * S.m * a) (hk : S.k = S.m * (a^2 - μ)) :
     S.EquationOfMotion (fun t : Time => exp (-a * t.val) • y t) := by
   intro t
-  rw [exp_decay_smul_acceleration a μ y hy hdy hy'']
-  rw [exp_decay_smul_velocity a y hy]
-  rw [hγ, hk]
+  rw [exp_decay_smul_acceleration a μ y hy hdy hy'', exp_decay_smul_velocity a y hy,
+    hγ, hk]
   simp [smul_add, smul_sub, smul_smul]
-  module
+  ext i; simp; ring
 
 /-!
 
@@ -234,12 +229,17 @@ polynomial, and hyperbolic base trajectories before the exponential decay factor
 
 -/
 
+private lemma fderiv_comp_val_eq_deriv {t : Time} (g : ℝ → ℝ)
+    (hg : DifferentiableAt ℝ g t.val) :
+    (fderiv ℝ (fun s : Time => g s.val) t) 1 = _root_.deriv g t.val := by
+  rw [fderiv_fun_comp t hg (by fun_prop), ContinuousLinearMap.comp_apply, Time.fderiv_val]
+  simp
+
 private lemma criticallyDampedBase_velocity (IC : InitialConditions) :
     ∂ₜ (S.criticallyDampedBase IC) =
       fun _ : Time => IC.v₀ + S.decayRate • IC.x₀ := by
   funext t
-  change ∂ₜ (fun t : Time =>
-    IC.x₀ + t.val • (IC.v₀ + S.decayRate • IC.x₀)) t = _
+  unfold criticallyDampedBase
   rw [Time.deriv_eq, fderiv_fun_add (by fun_prop) (by fun_prop),
     fderiv_fun_const, fderiv_smul_const (by fun_prop)]
   simp
@@ -262,11 +262,6 @@ private lemma underdampedBase_velocity (IC : InitialConditions) (hS : S.IsUnderd
           (IC.v₀ + S.decayRate • IC.x₀) := by
   have hΩ : S.angularFrequency ≠ 0 := S.angularFrequency_ne_zero_of_underdamped hS
   funext t
-  have fderiv_comp_val_eq_deriv : ∀ g : ℝ → ℝ, DifferentiableAt ℝ g t.val →
-      (fderiv ℝ (fun s : Time => g s.val) t) 1 = _root_.deriv g t.val := by
-    intro g hg
-    rw [fderiv_fun_comp t hg (by fun_prop), ContinuousLinearMap.comp_apply, Time.fderiv_val]
-    simp
   rw [Time.deriv_eq, fderiv_fun_add (by fun_prop) (by fun_prop),
     fderiv_smul_const (by fun_prop), fderiv_smul_const (by fun_prop)]
   simp only [add_apply, ContinuousLinearMap.smulRight_apply]
@@ -287,11 +282,6 @@ private lemma underdampedBase_acceleration (IC : InitialConditions) (hS : S.IsUn
   have hΩ : S.angularFrequency ≠ 0 := S.angularFrequency_ne_zero_of_underdamped hS
   rw [S.underdampedBase_velocity IC hS]
   funext t
-  have fderiv_comp_val_eq_deriv : ∀ g : ℝ → ℝ, DifferentiableAt ℝ g t.val →
-      (fderiv ℝ (fun s : Time => g s.val) t) 1 = _root_.deriv g t.val := by
-    intro g hg
-    rw [fderiv_fun_comp t hg (by fun_prop), ContinuousLinearMap.comp_apply, Time.fderiv_val]
-    simp
   rw [Time.deriv_eq, fderiv_fun_add (by fun_prop) (by fun_prop),
     fderiv_smul_const (by fun_prop), fderiv_smul_const (by fun_prop)]
   simp only [add_apply, ContinuousLinearMap.smulRight_apply]
@@ -312,11 +302,6 @@ private lemma overdampedBase_velocity (IC : InitialConditions) (hS : S.IsOverdam
           (IC.v₀ + S.decayRate • IC.x₀) := by
   have hΩ : S.angularFrequency ≠ 0 := S.angularFrequency_ne_zero_of_overdamped hS
   funext t
-  have fderiv_comp_val_eq_deriv : ∀ g : ℝ → ℝ, DifferentiableAt ℝ g t.val →
-      (fderiv ℝ (fun s : Time => g s.val) t) 1 = _root_.deriv g t.val := by
-    intro g hg
-    rw [fderiv_fun_comp t hg (by fun_prop), ContinuousLinearMap.comp_apply, Time.fderiv_val]
-    simp
   rw [Time.deriv_eq, fderiv_fun_add (by fun_prop) (by fun_prop),
     fderiv_smul_const (by fun_prop), fderiv_smul_const (by fun_prop)]
   simp only [add_apply, ContinuousLinearMap.smulRight_apply]
@@ -337,11 +322,6 @@ private lemma overdampedBase_acceleration (IC : InitialConditions) (hS : S.IsOve
   have hΩ : S.angularFrequency ≠ 0 := S.angularFrequency_ne_zero_of_overdamped hS
   rw [S.overdampedBase_velocity IC hS]
   funext t
-  have fderiv_comp_val_eq_deriv : ∀ g : ℝ → ℝ, DifferentiableAt ℝ g t.val →
-      (fderiv ℝ (fun s : Time => g s.val) t) 1 = _root_.deriv g t.val := by
-    intro g hg
-    rw [fderiv_fun_comp t hg (by fun_prop), ContinuousLinearMap.comp_apply, Time.fderiv_val]
-    simp
   rw [Time.deriv_eq, fderiv_fun_add (by fun_prop) (by fun_prop),
     fderiv_smul_const (by fun_prop), fderiv_smul_const (by fun_prop)]
   simp only [add_apply, ContinuousLinearMap.smulRight_apply]
@@ -375,8 +355,9 @@ lemma trajectory_equationOfMotion_of_criticallyDamped (IC : InitialConditions)
       fun_prop)
     (by
       rw [S.criticallyDampedBase_velocity IC]
-      fun_prop) ?_ hγ hk
-  simpa using S.criticallyDampedBase_acceleration IC
+      fun_prop)
+    (by
+      simpa using S.criticallyDampedBase_acceleration IC) hγ hk
 
 /-- In the underdamped regime, the selected trajectory satisfies the damped equation of
 motion. -/
@@ -388,13 +369,14 @@ lemma trajectory_equationOfMotion_of_underdamped (IC : InitialConditions)
   have hk : S.k = S.m * (S.decayRate^2 - (-S.angularFrequency^2)) := by
     rw [S.k_eq_m_mul_ω_sq, S.angularFrequency_sq_of_underdamped hS]
     ring
-  refine S.exp_decay_smul_equationOfMotion S.decayRate
-    (-S.angularFrequency^2) (S.underdampedBase IC)
+  refine S.exp_decay_smul_equationOfMotion S.decayRate (-S.angularFrequency^2)
+    (S.underdampedBase IC)
     (by
       unfold underdampedBase
       fun_prop) ?_
     (S.underdampedBase_acceleration IC hS) hγ hk
-  rw [show ∂ₜ (S.underdampedBase IC) = _ from S.underdampedBase_velocity IC hS]
+  unfold underdampedBase
+  rw [S.underdampedBase_velocity IC hS]
   fun_prop
 
 /-- In the overdamped regime, the selected trajectory satisfies the damped equation of
@@ -413,7 +395,8 @@ lemma trajectory_equationOfMotion_of_overdamped (IC : InitialConditions)
       unfold overdampedBase
       fun_prop) ?_
     (S.overdampedBase_acceleration IC hS) hγ hk
-  rw [show ∂ₜ (S.overdampedBase IC) = _ from S.overdampedBase_velocity IC hS]
+  unfold overdampedBase
+  rw [S.overdampedBase_velocity IC hS]
   fun_prop
 
 /-- The selected trajectory satisfies the damped equation of motion. -/
@@ -424,8 +407,9 @@ lemma trajectory_equationOfMotion (IC : InitialConditions) :
   · by_cases hCritical : S.IsCriticallyDamped
     · exact S.trajectory_equationOfMotion_of_criticallyDamped IC hCritical
     · have hOver : S.IsOverdamped := by
-        rw [IsOverdamped, IsUnderdamped] at *
-        exact lt_of_le_of_ne (not_lt.mp hUnder) (Ne.symm hCritical)
+        dsimp [IsOverdamped, IsUnderdamped, IsCriticallyDamped] at hUnder hCritical ⊢
+        have hle : 0 ≤ S.discriminant := not_lt.mp hUnder
+        exact lt_of_le_of_ne hle (Ne.symm hCritical)
       exact S.trajectory_equationOfMotion_of_overdamped IC hOver
 
 /-!

Physlib/ClassicalMechanics/HarmonicOscillator/Basic.lean

@@ -273,7 +273,7 @@ lemma kineticEnergy_deriv (xₜ : Time → EuclideanSpace ℝ (Fin 1)) (hx : Con
   congr 1
   simp only [smul_add]
   module
-  repeat fun_prop
+  all_goals fun_prop
 
 lemma potentialEnergy_deriv (xₜ : Time → EuclideanSpace ℝ (Fin 1)) (hx : ContDiff ℝ ∞ xₜ) :
     ∂ₜ (fun t => potentialEnergy S (xₜ t)) = fun t => ⟪∂ₜ xₜ t, S.k • xₜ t⟫_ℝ := by
@@ -293,10 +293,7 @@ lemma potentialEnergy_deriv (xₜ : Time → EuclideanSpace ℝ (Fin 1)) (hx : C
     congr 1
     module
   rw [real_inner_comm, ← inner_smul_right]
-  repeat fun_prop
-  apply Differentiable.differentiableAt
-  rw [contDiff_infty_iff_fderiv] at hx
-  exact hx.1
+  all_goals (first | fun_prop | exact ((contDiff_infty_iff_fderiv.mp hx).1 t))
 
 lemma energy_deriv (xₜ : Time → EuclideanSpace ℝ (Fin 1)) (hx : ContDiff ℝ ∞ xₜ) :
     ∂ₜ (energy S xₜ) = fun t => ⟪∂ₜ xₜ t, S.m • ∂ₜ (∂ₜ xₜ) t + S.k • xₜ t⟫_ℝ := by
@@ -309,8 +306,7 @@ lemma energy_deriv (xₜ : Time → EuclideanSpace ℝ (Fin 1)) (hx : ContDiff 
   rw [potentialEnergy_deriv, kineticEnergy_deriv]
   simp only
   rw [← inner_add_right]
-  fun_prop
-  fun_prop
+  all_goals fun_prop
 
 /-!
 
@@ -374,19 +370,7 @@ The lagrangian is smooth in all its arguments.
 @[fun_prop]
 lemma contDiff_lagrangian (n : WithTop ℕ∞) : ContDiff ℝ n ↿S.lagrangian := by
   rw [lagrangian_eq]
-  apply ContDiff.sub
-  · apply ContDiff.mul
-    · apply ContDiff.mul
-      · exact contDiff_const
-      · exact contDiff_const
-    · exact ContDiff.inner (𝕜 := ℝ) (contDiff_snd.comp contDiff_snd)
-        (contDiff_snd.comp contDiff_snd)
-  · apply ContDiff.mul
-    · apply ContDiff.mul
-      · exact contDiff_const
-      · exact contDiff_const
-    · exact ContDiff.inner (𝕜 := ℝ) (contDiff_fst.comp contDiff_snd)
-        (contDiff_fst.comp contDiff_snd)
+  fun_prop
 
 lemma toDual_symm_innerSL (x : EuclideanSpace ℝ (Fin 1)) :
     (InnerProductSpace.toDual ℝ (EuclideanSpace ℝ (Fin 1))).symm (innerSL ℝ x) = x := by
@@ -400,8 +384,6 @@ lemma gradient_inner_self (x : EuclideanSpace ℝ (Fin 1)) :
   unfold gradient
   rw [InnerProductSpace.toDual_symm_apply]
   have hid : DifferentiableAt ℝ (fun y : EuclideanSpace ℝ (Fin 1) => y) x := differentiableAt_id
-  rw [show (fun y : EuclideanSpace ℝ (Fin 1) => ⟪y, y⟫_ℝ) =
-      fun y => ⟪(fun y => y) y, (fun y => y) y⟫_ℝ from rfl]
   rw [fderiv_inner_apply (𝕜 := ℝ) hid hid]
   simp only [fderiv_fun_id, ContinuousLinearMap.coe_id', id_eq, real_inner_comm, inner_smul_left',
     ringHom_apply]
@@ -418,10 +400,8 @@ lemma gradient_const_mul_inner_self (c : ℝ) (x : EuclideanSpace ℝ (Fin 1)) :
           rw [fderiv_const_mul]; fun_prop
     _ = c • gradient (fun y : EuclideanSpace ℝ (Fin 1) => ⟪y, y⟫_ℝ) x := by
           simp only [gradient, map_smul]
-    _ = c • ((2 : ℝ) • x) := by
-          rw [gradient_inner_self]
-    _ = (2 * c) • x := by
-          rw [smul_smul, mul_comm]
+    _ = c • ((2 : ℝ) • x) := by rw [gradient_inner_self]
+    _ = (2 * c) • x := by rw [smul_smul, mul_comm]
 
 /-!
 
@@ -550,17 +530,9 @@ 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
   unfold force potentialEnergy
-  have hpot : (fun y : EuclideanSpace ℝ (Fin 1) => (1 / (2 : ℝ)) • S.k • ⟪y, y⟫_ℝ) =
-      fun y => ((1 / (2 : ℝ)) * S.k) * ⟪y, y⟫_ℝ := by
-    funext y
-    simp [smul_eq_mul, mul_assoc]
-  rw [hpot]
-  have hgrad : gradient (fun y : EuclideanSpace ℝ (Fin 1) => ((1 / (2 : ℝ)) * S.k) * ⟪y, y⟫_ℝ) x
-      = S.k • x := by
-    simpa [smul_eq_mul, mul_assoc] using
-      (gradient_const_mul_inner_self (c := (1 / (2 : ℝ)) * S.k) x)
-  rw [hgrad]
-  simp [neg_smul]
+  simp only [smul_eq_mul]
+  simpa [mul_assoc] using congrArg Neg.neg
+    (gradient_const_mul_inner_self (c := (1/2) * S.k) x)
 
 /-!
 
@@ -578,19 +550,8 @@ lemma gradLagrangian_eq_force (xₜ : Time → EuclideanSpace ℝ (Fin 1)) (hx :
   rw [gradLagrangian_eq_eulerLagrangeOp S xₜ hx, eulerLagrangeOp]
   congr
   · simp [gradient_lagrangian_position_eq, force_eq_linear]
-  · conv_lhs =>
-      arg 1
-      ext t'
-      rw [gradient_lagrangian_velocity_eq]
-    show ∂ₜ (fun t' => S.m • ∂ₜ xₜ t') t = S.m • ∂ₜ (∂ₜ xₜ) t
-    have hd : DifferentiableAt ℝ (∂ₜ xₜ) t :=
-      (deriv_differentiable_of_contDiff xₜ hx).differentiableAt
-    calc
-      ∂ₜ (fun t' => S.m • ∂ₜ xₜ t') t
-          = fderiv ℝ (fun t' => S.m • ∂ₜ xₜ t') t 1 := rfl
-      _ = S.m • (fderiv ℝ (∂ₜ xₜ) t 1) := by
-          exact congrArg (fun L => L 1) (fderiv_const_smul (c := S.m) (f := ∂ₜ xₜ) hd)
-      _ = S.m • ∂ₜ (∂ₜ xₜ) t := rfl
+  · simp [gradient_lagrangian_velocity_eq, Time.deriv_smul (∂ₜ xₜ) S.m
+      (deriv_differentiable_of_contDiff xₜ hx)]
 
 /-!
 
@@ -636,9 +597,7 @@ lemma energy_conservation_of_equationOfMotion (xₜ : Time → EuclideanSpace 
   rw [energy_deriv _ _ hx]
   rw [equationOfMotion_iff_newtons_2nd_law _ _ hx] at h
   funext x
-  simp only [Pi.zero_apply]
-  rw [h]
-  simp [force_eq_linear]
+  simp [h x, force_eq_linear]
 
 /-!
 
@@ -783,17 +742,15 @@ 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)) :
     gradient (hamiltonian S t p) x = S.k • x := by
-  have h_eq : (fun y : EuclideanSpace ℝ (Fin 1) => hamiltonian S t p y) =
-      fun y => ((1 / (2 : ℝ)) * S.k) * ⟪y, y⟫_ℝ +
+  have h_eq : hamiltonian S t p = fun y : EuclideanSpace ℝ (Fin 1) =>
+      ((1 / (2 : ℝ)) * S.k) * ⟪y, y⟫_ℝ +
         ((1 / (2 : ℝ)) * (1 / S.m) * ⟪p, p⟫_ℝ) := by
-    funext y; unfold hamiltonian; simp only [toCanonicalMomentum, lagrangian, one_div,
+    ext y; unfold hamiltonian; simp only [toCanonicalMomentum, lagrangian, one_div,
       inner_self_eq_norm_sq_to_K, ringHom_apply, potentialEnergy, smul_eq_mul,
       LinearEquiv.coe_symm_mk', inner_smul_right, norm_smul, norm_inv, norm_eq_abs]
-    have hm : S.m ≠ 0 := m_ne_zero S
     field_simp
-    ring_nf
-    simp [mul_two]
-  change gradient (fun y : EuclideanSpace ℝ (Fin 1) => hamiltonian S t p y) x = S.k • x
+    simp [sq_abs]
+    ring
   rw [h_eq, gradient_add_const', gradient_const_mul_inner_self]
   ext; simp
 
@@ -806,11 +763,9 @@ lemma gradient_hamiltonian_momentum_eq (t : Time) (x : EuclideanSpace ℝ (Fin 1
     funext y; unfold hamiltonian; simp only [toCanonicalMomentum, lagrangian, one_div,
       inner_self_eq_norm_sq_to_K, ringHom_apply, potentialEnergy, smul_eq_mul,
       LinearEquiv.coe_symm_mk', inner_smul_right, norm_smul, norm_inv, norm_eq_abs]
-    have hm : S.m ≠ 0 := m_ne_zero S
     field_simp
-    ring_nf
-    simp [mul_two]
-  change gradient (fun y : EuclideanSpace ℝ (Fin 1) => hamiltonian S t y x) p = (1 / S.m) • p
+    simp [sq_abs]
+    ring
   rw [h_eq, gradient_add_const', gradient_const_mul_inner_self]
   ext; simp
 
@@ -831,11 +786,7 @@ lemma hamiltonian_eq_energy (xₜ : Time → EuclideanSpace ℝ (Fin 1)) :
     rw [← toCanonicalMomentum_eq (S := S) (t := t) (x := xₜ t) (v := ∂ₜ xₜ t)]
     exact LinearEquiv.symm_apply_apply (toCanonicalMomentum S t (xₜ t)) (∂ₜ xₜ t)
   unfold hamiltonian lagrangian energy kineticEnergy potentialEnergy
-  simp only [toCanonicalMomentum_eq, inner_smul_left, one_div, smul_eq_mul]
-  rw [hsymm]
-  ring_nf
-  simp only [ringHom_apply, inner_self_eq_norm_sq_to_K, one_div, add_left_inj]
-  field_simp
+  simp [toCanonicalMomentum_eq, inner_smul_left, one_div, smul_eq_mul, hsymm]
   ring
 
 /-!