Skip to content

chore: fix build warnings from the v4.34.0 bump #1685

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
zhikaip merged 3 commits into from
Sep 24, 2026
Merged

chore: fix build warnings from the v4.34.0 bump #1685

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
e647e69
chore(ClassicalMechanics): replace deprecated tfae_cons_self in equat…
zhikaip Sep 24, 2026
704d645
chore(Space): drop unused simp arguments in eq_neg_curl_of_div_zero
zhikaip Sep 24, 2026
adf8b08
chore(QuantumInfo): replace deprecated peel in tendsto_toReal_iff_of_…
zhikaip Sep 24, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions Physlib/ClassicalMechanics/HarmonicOscillator/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
6 changes: 3 additions & 3 deletions Physlib/ClassicalMechanics/Pendulum/SimplePendulum/Hamiltonian.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
6 changes: 2 additions & 4 deletions Physlib/SpaceAndTime/Space/Derivatives/Curl.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
2 changes: 1 addition & 1 deletion QuantumInfo/ForMathlib/Filter.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion QuantumInfo/ForMathlib/LimSupInf.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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) →
Expand Down
3 changes: 2 additions & 1 deletion QuantumInfo/ForMathlib/Matrix.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
Loading