Merge branch 'master' into YK-prod-mk

Mathlib.lean

@@ -3763,6 +3763,7 @@ import Mathlib.LinearAlgebra.RootSystem.Basic
 import Mathlib.LinearAlgebra.RootSystem.CartanMatrix
 import Mathlib.LinearAlgebra.RootSystem.Defs
 import Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
+import Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
 import Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
 import Mathlib.LinearAlgebra.RootSystem.Hom
 import Mathlib.LinearAlgebra.RootSystem.OfBilinear

Mathlib/Algebra/MvPolynomial/Eval.lean

@@ -752,14 +752,16 @@ end EvalMem
 variable {S T : Type*} [CommSemiring S] [Algebra R S] [CommSemiring T] [Algebra R T] [Algebra S T]
   [IsScalarTower R S T]
 
-lemma aeval_sum_elim {σ τ : Type*} (p : MvPolynomial (σ ⊕ τ) R) (f : τ → S) (g : σ → T) :
+lemma aeval_sumElim {σ τ : Type*} (p : MvPolynomial (σ ⊕ τ) R) (f : τ → S) (g : σ → T) :
     (aeval (Sum.elim g (algebraMap S T ∘ f))) p =
       (aeval g) ((aeval (Sum.elim X (C ∘ f))) p) := by
   induction' p using MvPolynomial.induction_on with r p q hp hq p i h
   · simp [← IsScalarTower.algebraMap_apply]
   · simp [hp, hq]
   · cases i <;> simp [h]
 
+@[deprecated (since := "2025-02-21")] alias aeval_sum_elim := aeval_sumElim
+
 end CommSemiring
 
 end MvPolynomial

Mathlib/Algebra/MvPolynomial/PDeriv.lean

@@ -132,7 +132,7 @@ lemma pderiv_rename {τ : Type*} {f : σ → τ} (hf : Function.Injective f)
       Pi.single_apply, hf.eq_iff, smul_eq_mul, mul_ite, mul_one, mul_zero, h, map_add, add_left_inj]
     split_ifs <;> simp
 
-lemma aeval_sum_elim_pderiv_inl {S τ : Type*} [CommRing S] [Algebra R S]
+lemma aeval_sumElim_pderiv_inl {S τ : Type*} [CommRing S] [Algebra R S]
     (p : MvPolynomial (σ ⊕ τ) R) (f : τ → S) (j : σ) :
     aeval (Sum.elim X (C ∘ f)) ((pderiv (Sum.inl j)) p) =
       (pderiv j) ((aeval (Sum.elim X (C ∘ f))) p) := by
@@ -143,6 +143,8 @@ lemma aeval_sum_elim_pderiv_inl {S τ : Type*} [CommRing S] [Algebra R S]
   · simp only [Derivation.leibniz, pderiv_X, smul_eq_mul, map_add, map_mul, aeval_X, h]
     cases q <;> simp [Pi.single_apply]
 
+@[deprecated (since := "2025-02-21")] alias aeval_sum_elim_pderiv_inl := aeval_sumElim_pderiv_inl
+
 end PDeriv
 
 end MvPolynomial

Mathlib/Algebra/Order/AddGroupWithTop.lean

@@ -7,7 +7,6 @@ import Mathlib.Algebra.Order.Group.Defs
 import Mathlib.Algebra.Order.Monoid.WithTop
 import Mathlib.Algebra.Group.Hom.Defs
 import Mathlib.Algebra.CharZero.Defs
-import Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual
 import Mathlib.Algebra.Order.Monoid.Canonical.Defs
 
 /-!

Mathlib/Algebra/Star/Pi.lean

@@ -70,8 +70,10 @@ theorem update_star [∀ i, Star (f i)] [DecidableEq I] (h : ∀ i : I, f i) (i
     Function.update (star h) i (star a) = star (Function.update h i a) :=
   funext fun j => (apply_update (fun _ => star) h i a j).symm
 
-theorem star_sum_elim {I J α : Type*} (x : I → α) (y : J → α) [Star α] :
+theorem star_sumElim {I J α : Type*} (x : I → α) (y : J → α) [Star α] :
     star (Sum.elim x y) = Sum.elim (star x) (star y) := by
   ext x; cases x <;> simp only [Pi.star_apply, Sum.elim_inl, Sum.elim_inr]
 
+@[deprecated (since := "2025-02-21")] alias star_sum_elim := Function.star_sumElim
+
 end Function

Mathlib/Analysis/Calculus/Rademacher.lean

@@ -61,11 +61,14 @@ variation, and is therefore ae differentiable, together with a Fubini argument.
 -/
 
 
-theorem memℒp_lineDeriv (hf : LipschitzWith C f) (v : E) :
-    Memℒp (fun x ↦ lineDeriv ℝ f x v) ∞ μ :=
-  memℒp_top_of_bound (aestronglyMeasurable_lineDeriv hf.continuous μ)
+theorem memLp_lineDeriv (hf : LipschitzWith C f) (v : E) :
+    MemLp (fun x ↦ lineDeriv ℝ f x v) ∞ μ :=
+  memLp_top_of_bound (aestronglyMeasurable_lineDeriv hf.continuous μ)
     (C * ‖v‖) (.of_forall fun _x ↦ norm_lineDeriv_le_of_lipschitz ℝ hf)
 
+@[deprecated (since := "2025-02-21")]
+alias memℒp_lineDeriv := memLp_lineDeriv
+
 variable [FiniteDimensional ℝ E] [IsAddHaarMeasure μ]
 
 theorem ae_lineDifferentiableAt
@@ -87,7 +90,7 @@ theorem ae_lineDifferentiableAt
 
 theorem locallyIntegrable_lineDeriv (hf : LipschitzWith C f) (v : E) :
     LocallyIntegrable (fun x ↦ lineDeriv ℝ f x v) μ :=
-  (hf.memℒp_lineDeriv v).locallyIntegrable le_top
+  (hf.memLp_lineDeriv v).locallyIntegrable le_top
 
 /-!
 ### Step 2: the ae line derivative is linear
@@ -212,7 +215,7 @@ theorem ae_lineDeriv_sum_eq
   simp_rw [Finset.smul_sum]
   have A : ∀ i ∈ s, Integrable (fun x ↦ g x • (a i • fun x ↦ lineDeriv ℝ f x (v i)) x) μ :=
     fun i hi ↦ (g_smooth.continuous.integrable_of_hasCompactSupport g_comp).smul_of_top_left
-      ((hf.memℒp_lineDeriv (v i)).const_smul (a i))
+      ((hf.memLp_lineDeriv (v i)).const_smul (a i))
   rw [integral_finset_sum _ A]
   suffices S1 : ∫ x, lineDeriv ℝ f x (∑ i ∈ s, a i • v i) * g x ∂μ
       = ∑ i ∈ s, a i * ∫ x, lineDeriv ℝ f x (v i) * g x ∂μ by

Mathlib/Analysis/Convolution.lean

@@ -80,7 +80,7 @@ The following notations are localized in the locale `Convolution`:
 # To do
 * Existence and (uniform) continuity of the convolution if
   one of the maps is in `ℒ^p` and the other in `ℒ^q` with `1 / p + 1 / q = 1`.
-  This might require a generalization of `MeasureTheory.Memℒp.smul` where `smul` is generalized
+  This might require a generalization of `MeasureTheory.MemLp.smul` where `smul` is generalized
   to a continuous bilinear map.
   (see e.g. [Fremlin, *Measure Theory* (volume 2)][fremlin_vol2], 255K)
 * The convolution is an `AEStronglyMeasurable` function

Mathlib/Analysis/Distribution/SchwartzSpace.lean

@@ -1298,22 +1298,28 @@ theorem eLpNorm_lt_top (f : 𝓢(E, F)) (p : ℝ≥0∞) (μ : Measure E := by v
 variable [SecondCountableTopologyEither E F]
 
 /-- Schwartz functions are in `L^∞`; does not require `hμ.HasTemperateGrowth`. -/
-theorem memℒp_top (f : 𝓢(E, F)) (μ : Measure E := by volume_tac) : Memℒp f ⊤ μ := by
+theorem memLp_top (f : 𝓢(E, F)) (μ : Measure E := by volume_tac) : MemLp f ⊤ μ := by
   rcases f.decay 0 0 with ⟨C, _, hC⟩
-  refine memℒp_top_of_bound f.continuous.aestronglyMeasurable C (ae_of_all μ fun x ↦ ?_)
+  refine memLp_top_of_bound f.continuous.aestronglyMeasurable C (ae_of_all μ fun x ↦ ?_)
   simpa using hC x
 
+@[deprecated (since := "2025-02-21")]
+alias memℒp_top := memLp_top
+
 /-- Schwartz functions are in `L^p` for any `p`. -/
-theorem memℒp (f : 𝓢(E, F)) (p : ℝ≥0∞) (μ : Measure E := by volume_tac)
-    [hμ : μ.HasTemperateGrowth] : Memℒp f p μ :=
+theorem memLp (f : 𝓢(E, F)) (p : ℝ≥0∞) (μ : Measure E := by volume_tac)
+    [hμ : μ.HasTemperateGrowth] : MemLp f p μ :=
   ⟨f.continuous.aestronglyMeasurable, f.eLpNorm_lt_top p μ⟩
 
+@[deprecated (since := "2025-02-21")]
+alias memℒp := memLp
+
 /-- Map a Schwartz function to an `Lp` function for any `p`. -/
 def toLp (f : 𝓢(E, F)) (p : ℝ≥0∞) (μ : Measure E := by volume_tac) [hμ : μ.HasTemperateGrowth] :
-    Lp F p μ := (f.memℒp p μ).toLp
+    Lp F p μ := (f.memLp p μ).toLp
 
 theorem coeFn_toLp (f : 𝓢(E, F)) (p : ℝ≥0∞) (μ : Measure E := by volume_tac)
-    [hμ : μ.HasTemperateGrowth] : f.toLp p μ =ᵐ[μ] f := (f.memℒp p μ).coeFn_toLp
+    [hμ : μ.HasTemperateGrowth] : f.toLp p μ =ᵐ[μ] f := (f.memLp p μ).coeFn_toLp
 
 theorem norm_toLp {f : 𝓢(E, F)} {p : ℝ≥0∞} {μ : Measure E} [hμ : μ.HasTemperateGrowth] :
     ‖f.toLp p μ‖ = ENNReal.toReal (eLpNorm f p μ) := by

Mathlib/Analysis/FunctionalSpaces/SobolevInequality.lean

@@ -534,7 +534,7 @@ theorem eLpNorm_le_eLpNorm_fderiv_of_eq_inner  {u : E → F'}
     refine lintegral_rpow_enorm_lt_top_of_eLpNorm'_lt_top
       ((NNReal.coe_pos.trans pos_iff_ne_zero).mpr h0p') ?_ |>.ne
     rw [← eLpNorm_nnreal_eq_eLpNorm' h0p']
-    exact hu.continuous.memℒp_of_hasCompactSupport (μ := μ) h2u |>.eLpNorm_lt_top
+    exact hu.continuous.memLp_of_hasCompactSupport (μ := μ) h2u |>.eLpNorm_lt_top
   have h5u : (∫⁻ x, ‖u x‖ₑ ^ (p' : ℝ) ∂μ) ^ (1 / q) ≠ 0 :=
     ENNReal.rpow_pos (pos_iff_ne_zero.mpr h3u) h4u |>.ne'
   have h6u : (∫⁻ x, ‖u x‖ₑ ^ (p' : ℝ) ∂μ) ^ (1 / q) ≠ ∞ :=

Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean

@@ -72,13 +72,13 @@ theorem Gamma_mul_add_mul_le_rpow_Gamma_mul_rpow_Gamma {s t a b : ℝ} (hs : 0 <
   -- show `f c u` is in `ℒp` for `p = 1/c`:
   have f_mem_Lp :
     ∀ {c u : ℝ} (hc : 0 < c) (hu : 0 < u),
-      Memℒp (f c u) (ENNReal.ofReal (1 / c)) (volume.restrict (Ioi 0)) := by
+      MemLp (f c u) (ENNReal.ofReal (1 / c)) (volume.restrict (Ioi 0)) := by
     intro c u hc hu
     have A : ENNReal.ofReal (1 / c) ≠ 0 := by
       rwa [Ne, ENNReal.ofReal_eq_zero, not_le, one_div_pos]
     have B : ENNReal.ofReal (1 / c) ≠ ∞ := ENNReal.ofReal_ne_top
-    rw [← memℒp_norm_rpow_iff _ A B, ENNReal.toReal_ofReal (one_div_nonneg.mpr hc.le),
-      ENNReal.div_self A B, memℒp_one_iff_integrable]
+    rw [← memLp_norm_rpow_iff _ A B, ENNReal.toReal_ofReal (one_div_nonneg.mpr hc.le),
+      ENNReal.div_self A B, memLp_one_iff_integrable]
     · apply Integrable.congr (GammaIntegral_convergent hu)
       refine eventuallyEq_of_mem (self_mem_ae_restrict measurableSet_Ioi) fun x hx => ?_
       dsimp only

Mathlib/Analysis/SumIntegralComparisons.lean

@@ -232,7 +232,7 @@ lemma sum_mul_Ico_le_integral_of_monotone_antitone
   · apply Integrable.mono_measure _ (Measure.restrict_mono_set _ Ico_subset_Icc_self)
     apply Integrable.mul_of_top_left
     · exact hf.integrableOn_isCompact isCompact_Icc
-    · apply AntitoneOn.memℒp_isCompact isCompact_Icc
+    · apply AntitoneOn.memLp_isCompact isCompact_Icc
       intro x hx y hy hxy
       apply hg
       · simpa using hx
@@ -277,7 +277,7 @@ lemma integral_le_sum_mul_Ico_of_antitone_monotone
   · apply Integrable.mono_measure _ (Measure.restrict_mono_set _ Ico_subset_Icc_self)
     apply Integrable.mul_of_top_left
     · exact hf.integrableOn_isCompact isCompact_Icc
-    · apply MonotoneOn.memℒp_isCompact isCompact_Icc
+    · apply MonotoneOn.memLp_isCompact isCompact_Icc
       intro x hx y hy hxy
       apply hg
       · simpa using hx