From e647e698aaefc465bba705b491f6ef2ebe33c552 Mon Sep 17 00:00:00 2001 From: ZhiKai Pong Date: Thu, 24 Sep 2026 20:45:19 +0100 Subject: [PATCH 1/3] chore(ClassicalMechanics): replace deprecated tfae_cons_self in equationOfMotion_tfae `List.tfae_cons_self` is deprecated in Mathlib; use `List.tfae_cons_of_mem` with `List.mem_cons_self` in the harmonic oscillator and simple pendulum `equationOfMotion_tfae`. Co-authored-by: Claude Opus 5.5 --- Physlib/ClassicalMechanics/HarmonicOscillator/Basic.lean | 6 +++--- .../Pendulum/SimplePendulum/Hamiltonian.lean | 6 +++--- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/Physlib/ClassicalMechanics/HarmonicOscillator/Basic.lean b/Physlib/ClassicalMechanics/HarmonicOscillator/Basic.lean index 8100b914a..74aee8bb7 100644 --- a/Physlib/ClassicalMechanics/HarmonicOscillator/Basic.lean +++ b/Physlib/ClassicalMechanics/HarmonicOscillator/Basic.lean @@ -747,11 +747,11 @@ lemma equationOfMotion_tfae (xₜ : Time → EuclideanSpace ℝ (Fin 1)) (hx : C ∫ t, ⟪(pq' t).1, ∂ₜ (Prod.snd ∘ pq') t⟫_ℝ - S.hamiltonian t (pq' t).1 (pq' t).2) = 0] := by rw [← equationOfMotion_iff_hamiltonEqOp_eq_zero, ← equationOfMotion_iff_newtons_2nd_law] rw [hamiltons_equations_varGradient, euler_lagrange_varGradient] - simp only [List.tfae_cons_self] + simp only [List.tfae_cons_of_mem, List.mem_cons_self] rw [← gradLagrangian_eq_eulerLagrangeOp, ← equationOfMotion_iff_gradLagrangian_zero] - simp only [List.tfae_cons_self] + simp only [List.tfae_cons_of_mem, List.mem_cons_self] erw [← equationOfMotion_iff_hamiltonEqOp_eq_zero] - simp only [List.tfae_cons_self, List.tfae_singleton] + simp only [List.tfae_cons_of_mem, List.mem_cons_self, List.tfae_singleton] repeat fun_prop simp [toCanonicalMomentum_eq] repeat fun_prop diff --git a/Physlib/ClassicalMechanics/Pendulum/SimplePendulum/Hamiltonian.lean b/Physlib/ClassicalMechanics/Pendulum/SimplePendulum/Hamiltonian.lean index cdab3617d..ed83f35c5 100644 --- a/Physlib/ClassicalMechanics/Pendulum/SimplePendulum/Hamiltonian.lean +++ b/Physlib/ClassicalMechanics/Pendulum/SimplePendulum/Hamiltonian.lean @@ -309,14 +309,14 @@ lemma equationOfMotion_tfae (θ : Time → EuclideanSpace ℝ (Fin 1)) (hθ : Co rw [← S.equationOfMotion_iff_hamiltonEqOp_eq_zero θ hθ, ← S.equationOfMotion_iff_scalar θ] rw [hamiltons_equations_varGradient, euler_lagrange_varGradient] - simp only [List.tfae_cons_self] + simp only [List.tfae_cons_of_mem, List.mem_cons_self] rw [← S.gradLagrangian_eq_eulerLagrangeOp θ hθ, ← S.equationOfMotion_iff_gradLagrangian_zero θ hθ] - simp only [List.tfae_cons_self] + simp only [List.tfae_cons_of_mem, List.mem_cons_self] show List.TFAE [S.EquationOfMotion θ, S.hamiltonEqOp (fun t => S.canonicalMomentum t (θ t) (∂ₜ θ t)) θ = 0] rw [← S.equationOfMotion_iff_hamiltonEqOp_eq_zero θ hθ] - simp only [List.tfae_cons_self, List.tfae_singleton] + simp only [List.tfae_cons_of_mem, List.mem_cons_self, List.tfae_singleton] · exact hθ · exact S.contDiff_lagrangian _ · simp only [S.canonicalMomentum_eq]; fun_prop From 704d645629b1b1f06b5537ac495636396d6c872d Mon Sep 17 00:00:00 2001 From: ZhiKai Pong Date: Thu, 24 Sep 2026 20:45:20 +0100 Subject: [PATCH 2/3] chore(Space): drop unused simp arguments in eq_neg_curl_of_div_zero Co-authored-by: Claude Opus 5.5 --- Physlib/SpaceAndTime/Space/Derivatives/Curl.lean | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/Physlib/SpaceAndTime/Space/Derivatives/Curl.lean b/Physlib/SpaceAndTime/Space/Derivatives/Curl.lean index 8afeb162b..427896d81 100644 --- a/Physlib/SpaceAndTime/Space/Derivatives/Curl.lean +++ b/Physlib/SpaceAndTime/Space/Derivatives/Curl.lean @@ -490,10 +490,8 @@ lemma eq_neg_curl_of_div_zero (f : Space → EuclideanSpace ℝ (Fin 3)) (hf : C rw [fderiv_comp _ (by fun_prop) (by fun_prop), fderiv_comp _ (by fun_prop) (by fun_prop), fderiv_fun_smul (by fun_prop) (by fun_prop)] simp only [Function.comp_apply, ContinuousLinearMap.fderiv, fderiv_fun_const, Pi.zero_apply, - fderiv_fun_id, ContinuousLinearMap.coe_comp, _root_.add_apply, - FunLike.coe_smul, Pi.smul_apply, _root_.zero_apply, smul_zero, - ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.coe_id', id_eq, one_smul, zero_add, - PiLp.proj_apply] + fderiv_fun_id, ContinuousLinearMap.coe_comp, smul_zero, ContinuousLinearMap.smulRight_apply, + ContinuousLinearMap.coe_id', id_eq, one_smul, zero_add, PiLp.proj_apply] have hi (x : Space) (i : Fin 3) : ∫ (t : ℝ) in 0..1, (t * f (t • x) i * 2) - t * (- fderiv ℝ f (t • x) (t • x)) i ∂(volume) = f x i := by trans ∫ (t : ℝ) in 0..1, fderiv ℝ (fun t => t ^ 2 * f (t • x) i) t 1 ∂(volume) From adf8b08be4cf3772a0f146c7d94a3c26f883b5b0 Mon Sep 17 00:00:00 2001 From: ZhiKai Pong Date: Thu, 24 Sep 2026 20:45:20 +0100 Subject: [PATCH 3/3] chore(QuantumInfo): replace deprecated peel in tendsto_toReal_iff_of_eventually_ne_top, exists_liminf_zero_of_forall_liminf_le_with_UB, PosSemidef.rsmul `peel` is deprecated in Mathlib; use `filter_upwards` for the eventually-statements and `intro` for `PosSemidef.rsmul`. Co-authored-by: Claude Opus 5.5 --- QuantumInfo/ForMathlib/Filter.lean | 2 +- QuantumInfo/ForMathlib/LimSupInf.lean | 2 +- QuantumInfo/ForMathlib/Matrix.lean | 3 ++- 3 files changed, 4 insertions(+), 3 deletions(-) diff --git a/QuantumInfo/ForMathlib/Filter.lean b/QuantumInfo/ForMathlib/Filter.lean index 503835a25..4dcb0ac46 100644 --- a/QuantumInfo/ForMathlib/Filter.lean +++ b/QuantumInfo/ForMathlib/Filter.lean @@ -51,7 +51,7 @@ theorem ENNReal.tendsto_toReal_iff_of_eventually_ne_top (hx : x ≠ ∞) : Tendsto (fun n => (f n).toReal) fi (𝓝 x.toReal) ↔ Tendsto f fi (𝓝 x) := by have he₁ : f =ᶠ[fi] (fun n ↦ (f n).toNNReal) := by rw [EventuallyEq] - peel hf with h + filter_upwards [hf] with i h simp [h] have he₂ : (fun n ↦ (f n).toReal) = (fun n ↦ ((f n).toNNReal : ℝ≥0∞).toReal) := rfl diff --git a/QuantumInfo/ForMathlib/LimSupInf.lean b/QuantumInfo/ForMathlib/LimSupInf.lean index 7de745f57..94f009578 100644 --- a/QuantumInfo/ForMathlib/LimSupInf.lean +++ b/QuantumInfo/ForMathlib/LimSupInf.lean @@ -186,7 +186,7 @@ lemma exists_liminf_zero_of_forall_liminf_le_with_UB (y : ℝ≥0) (f : ℝ≥0 · beta_reduce rwa [Filter.liminf_congr] have h := hg₁.eventually (gt_mem_nhds <| half_pos hz) - peel h with h + filter_upwards [h] with n h rw [min_eq_left h.le] /- (∀ x, x > 0 → liminf (n ↦ f x n) ≤ y) → diff --git a/QuantumInfo/ForMathlib/Matrix.lean b/QuantumInfo/ForMathlib/Matrix.lean index 7fdb90282..07b3c3b74 100644 --- a/QuantumInfo/ForMathlib/Matrix.lean +++ b/QuantumInfo/ForMathlib/Matrix.lean @@ -722,7 +722,8 @@ theorem PosSemidef.rsmul {n : Type*} [Fintype n] {M : Matrix n n ℂ} (hM : M.Po rw [Matrix.posSemidef_iff_dotProduct_mulVec] at hM ⊢ constructor · exact hM.1.smul_real c - · peel hM.2 + · intro x + have := hM.2 x rw [smul_mulVec, dotProduct_smul] positivity