chore: rename five lemmas involving mathlib3 names (#11934)

Mathlib/Algebra/Lie/Weights/Linear.lean

@@ -95,7 +95,7 @@ open FiniteDimensional
 variable [IsDomain R] [IsPrincipalIdealRing R] [Module.Free R M] [Module.Finite R M]
   [LieAlgebra.IsNilpotent R L]
 
-lemma trace_comp_toEndomorphism_weight_space_eq (χ : L → R) :
+lemma trace_comp_toEndomorphism_weightSpace_eq (χ : L → R) :
     LinearMap.trace R _ ∘ₗ (toEndomorphism R L (weightSpace M χ)).toLinearMap =
     finrank R (weightSpace M χ) • χ := by
   ext x
@@ -106,6 +106,9 @@ lemma trace_comp_toEndomorphism_weight_space_eq (χ : L → R) :
   rw [LinearMap.comp_apply, LieHom.coe_toLinearMap, h₁, map_add, h₂]
   simp [mul_comm (χ x)]
 
+@[deprecated] alias trace_comp_toEndomorphism_weight_space_eq :=
+  trace_comp_toEndomorphism_weightSpace_eq -- 2024-04-06
+
 variable {R L M} in
 lemma zero_lt_finrank_weightSpace {χ : L → R} (hχ : weightSpace M χ ≠ ⊥) :
     0 < finrank R (weightSpace M χ) := by
@@ -118,13 +121,13 @@ instance instLinearWeightsOfCharZero [CharZero R] :
     LinearWeights R L M where
   map_add χ hχ x y := by
     rw [← smul_right_inj (zero_lt_finrank_weightSpace hχ).ne', smul_add, ← Pi.smul_apply,
-      ← Pi.smul_apply, ← Pi.smul_apply, ← trace_comp_toEndomorphism_weight_space_eq, map_add]
+      ← Pi.smul_apply, ← Pi.smul_apply, ← trace_comp_toEndomorphism_weightSpace_eq, map_add]
   map_smul χ hχ t x := by
     rw [← smul_right_inj (zero_lt_finrank_weightSpace hχ).ne', smul_comm, ← Pi.smul_apply,
-      ← Pi.smul_apply (finrank R _), ← trace_comp_toEndomorphism_weight_space_eq, map_smul]
+      ← Pi.smul_apply (finrank R _), ← trace_comp_toEndomorphism_weightSpace_eq, map_smul]
   map_lie χ hχ x y := by
     rw [← smul_right_inj (zero_lt_finrank_weightSpace hχ).ne', nsmul_zero, ← Pi.smul_apply,
-      ← trace_comp_toEndomorphism_weight_space_eq, LinearMap.comp_apply, LieHom.coe_toLinearMap,
+      ← trace_comp_toEndomorphism_weightSpace_eq, LinearMap.comp_apply, LieHom.coe_toLinearMap,
       LieHom.map_lie, Ring.lie_def, map_sub, LinearMap.trace_mul_comm, sub_self]
 
 end FiniteDimensional

Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean

@@ -615,7 +615,7 @@ theorem integrableOn_Ioi_of_intervalIntegral_norm_tendsto (I a : ℝ)
   integrableOn_Ioi_of_intervalIntegral_norm_bounded I' a hfi hb hI'
 #align measure_theory.integrable_on_Ioi_of_interval_integral_norm_tendsto MeasureTheory.integrableOn_Ioi_of_intervalIntegral_norm_tendsto
 
-theorem integrableOn_Ioc_of_interval_integral_norm_bounded {I a₀ b₀ : ℝ}
+theorem integrableOn_Ioc_of_intervalIntegral_norm_bounded {I a₀ b₀ : ℝ}
     (hfi : ∀ i, IntegrableOn f <| Ioc (a i) (b i)) (ha : Tendsto a l <| 𝓝 a₀)
     (hb : Tendsto b l <| 𝓝 b₀) (h : ∀ᶠ i in l, (∫ x in Ioc (a i) (b i), ‖f x‖) ≤ I) :
     IntegrableOn f (Ioc a₀ b₀) := by
@@ -625,19 +625,26 @@ theorem integrableOn_Ioc_of_interval_integral_norm_bounded {I a₀ b₀ : ℝ}
   refine' le_trans (set_integral_mono_set (hfi i).norm _ _) hi <;> apply ae_of_all
   · simp only [Pi.zero_apply, norm_nonneg, forall_const]
   · intro c hc; exact hc.1
-#align measure_theory.integrable_on_Ioc_of_interval_integral_norm_bounded MeasureTheory.integrableOn_Ioc_of_interval_integral_norm_bounded
+#align measure_theory.integrable_on_Ioc_of_interval_integral_norm_bounded MeasureTheory.integrableOn_Ioc_of_intervalIntegral_norm_bounded
 
-theorem integrableOn_Ioc_of_interval_integral_norm_bounded_left {I a₀ b : ℝ}
+theorem integrableOn_Ioc_of_intervalIntegral_norm_bounded_left {I a₀ b : ℝ}
     (hfi : ∀ i, IntegrableOn f <| Ioc (a i) b) (ha : Tendsto a l <| 𝓝 a₀)
     (h : ∀ᶠ i in l, (∫ x in Ioc (a i) b, ‖f x‖) ≤ I) : IntegrableOn f (Ioc a₀ b) :=
-  integrableOn_Ioc_of_interval_integral_norm_bounded hfi ha tendsto_const_nhds h
-#align measure_theory.integrable_on_Ioc_of_interval_integral_norm_bounded_left MeasureTheory.integrableOn_Ioc_of_interval_integral_norm_bounded_left
+  integrableOn_Ioc_of_intervalIntegral_norm_bounded hfi ha tendsto_const_nhds h
+#align measure_theory.integrable_on_Ioc_of_interval_integral_norm_bounded_left MeasureTheory.integrableOn_Ioc_of_intervalIntegral_norm_bounded_left
 
-theorem integrableOn_Ioc_of_interval_integral_norm_bounded_right {I a b₀ : ℝ}
+theorem integrableOn_Ioc_of_intervalIntegral_norm_bounded_right {I a b₀ : ℝ}
     (hfi : ∀ i, IntegrableOn f <| Ioc a (b i)) (hb : Tendsto b l <| 𝓝 b₀)
     (h : ∀ᶠ i in l, (∫ x in Ioc a (b i), ‖f x‖) ≤ I) : IntegrableOn f (Ioc a b₀) :=
-  integrableOn_Ioc_of_interval_integral_norm_bounded hfi tendsto_const_nhds hb h
-#align measure_theory.integrable_on_Ioc_of_interval_integral_norm_bounded_right MeasureTheory.integrableOn_Ioc_of_interval_integral_norm_bounded_right
+  integrableOn_Ioc_of_intervalIntegral_norm_bounded hfi tendsto_const_nhds hb h
+#align measure_theory.integrable_on_Ioc_of_interval_integral_norm_bounded_right MeasureTheory.integrableOn_Ioc_of_intervalIntegral_norm_bounded_right
+
+@[deprecated] alias integrableOn_Ioc_of_interval_integral_norm_bounded :=
+  integrableOn_Ioc_of_intervalIntegral_norm_bounded -- 2024-04-06
+@[deprecated] alias integrableOn_Ioc_of_interval_integral_norm_bounded_left :=
+  integrableOn_Ioc_of_intervalIntegral_norm_bounded_left -- 2024-04-06
+@[deprecated] alias integrableOn_Ioc_of_interval_integral_norm_bounded_right :=
+  integrableOn_Ioc_of_intervalIntegral_norm_bounded_right -- 2024-04-06
 
 end IntegrableOfIntervalIntegral
 

Mathlib/MeasureTheory/Integral/IntervalIntegral.lean

@@ -671,13 +671,15 @@ nonrec theorem integral_smul_measure (c : ℝ≥0∞) :
 end Basic
 
 -- Porting note (#11215): TODO: add `Complex.ofReal` version of `_root_.integral_ofReal`
-nonrec theorem _root_.RCLike.interval_integral_ofReal {𝕜 : Type*} [RCLike 𝕜] {a b : ℝ}
+nonrec theorem _root_.RCLike.intervalIntegral_ofReal {𝕜 : Type*} [RCLike 𝕜] {a b : ℝ}
     {μ : Measure ℝ} {f : ℝ → ℝ} : (∫ x in a..b, (f x : 𝕜) ∂μ) = ↑(∫ x in a..b, f x ∂μ) := by
   simp only [intervalIntegral, integral_ofReal, RCLike.ofReal_sub]
 
+@[deprecated] alias RCLike.interval_integral_ofReal := RCLike.intervalIntegral_ofReal -- 2024-04-06
+
 nonrec theorem integral_ofReal {a b : ℝ} {μ : Measure ℝ} {f : ℝ → ℝ} :
     (∫ x in a..b, (f x : ℂ) ∂μ) = ↑(∫ x in a..b, f x ∂μ) :=
-  RCLike.interval_integral_ofReal
+  RCLike.intervalIntegral_ofReal
 #align interval_integral.integral_of_real intervalIntegral.integral_ofReal
 
 section ContinuousLinearMap

Mathlib/MeasureTheory/Measure/Lebesgue/VolumeOfBalls.lean

@@ -29,7 +29,7 @@ Using these formulas, we compute the volume of the unit balls in several cases.
 * `Complex.volume_sum_rpow_lt_one` / `Complex.volume_sum_rpow_lt`: same as above but for complex
   finite dimensional vector space.
 
-* `Euclidean_space.volume_ball` / `Euclidean_space.volume_closedBall` : volume of open and closed
+* `EuclideanSpace.volume_ball` / `EuclideanSpace.volume_closedBall` : volume of open and closed
   balls in a finite dimensional Euclidean space.
 
 * `InnerProductSpace.volume_ball` / `InnerProductSpace.volume_closedBall`: volume of open and closed
@@ -157,7 +157,7 @@ theorem MeasureTheory.measure_le_eq_lt [Nontrivial E] (r : ℝ) :
 
 end general_case
 
-section Lp_space
+section LpSpace
 
 open BigOperators Real Fintype ENNReal FiniteDimensional MeasureTheory MeasureTheory.Measure
 
@@ -313,15 +313,15 @@ theorem Complex.volume_sum_rpow_le [Nonempty ι] {p : ℝ} (hp : 1 ≤ p) (r : 
   rw [measure_le_eq_lt _ nm_zero (fun x ↦ nm_neg x) (fun x y ↦ nm_add x y) (eq_zero _).mp
     (fun r x => nm_smul r x), Complex.volume_sum_rpow_lt _ hp]
 
-end Lp_space
+end LpSpace
 
-section Euclidean_space
+section EuclideanSpace
 
 variable (ι : Type*) [Nonempty ι] [Fintype ι]
 
 open Fintype Real MeasureTheory MeasureTheory.Measure ENNReal
 
-theorem Euclidean_space.volume_ball (x : EuclideanSpace ℝ ι) (r : ℝ) :
+theorem EuclideanSpace.volume_ball (x : EuclideanSpace ℝ ι) (r : ℝ) :
     volume (Metric.ball x r) = (.ofReal r) ^ card ι *
       .ofReal (Real.sqrt π  ^ card ι / Gamma (card ι / 2 + 1)) := by
   obtain hr | hr := le_total r 0
@@ -338,12 +338,16 @@ theorem Euclidean_space.volume_ball (x : EuclideanSpace ℝ ι) (r : ℝ) :
     · rw [Gamma_add_one (by norm_num), Gamma_one_half_eq, ← mul_assoc, mul_div_cancel₀ _
         two_ne_zero, one_mul]
 
-theorem Euclidean_space.volume_closedBall (x : EuclideanSpace ℝ ι) (r : ℝ) :
+theorem EuclideanSpace.volume_closedBall (x : EuclideanSpace ℝ ι) (r : ℝ) :
     volume (Metric.closedBall x r) = (.ofReal r) ^ card ι *
       .ofReal (sqrt π  ^ card ι / Gamma (card ι / 2 + 1)) := by
-  rw [addHaar_closedBall_eq_addHaar_ball, Euclidean_space.volume_ball]
+  rw [addHaar_closedBall_eq_addHaar_ball, EuclideanSpace.volume_ball]
 
-end Euclidean_space
+-- 2024-04-06
+@[deprecated] alias Euclidean_space.volume_ball := EuclideanSpace.volume_ball
+@[deprecated] alias Euclidean_space.volume_closedBall := EuclideanSpace.volume_closedBall
+
+end EuclideanSpace
 
 section InnerProductSpace
 
@@ -358,7 +362,7 @@ theorem InnerProductSpace.volume_ball (x : E) (r : ℝ) :
   rw [← ((stdOrthonormalBasis ℝ E).measurePreserving_repr_symm).measure_preimage
       measurableSet_ball]
   have : Nonempty (Fin (finrank ℝ E)) := Fin.pos_iff_nonempty.mp finrank_pos
-  have := Euclidean_space.volume_ball (Fin (finrank ℝ E)) ((stdOrthonormalBasis ℝ E).repr x) r
+  have := EuclideanSpace.volume_ball (Fin (finrank ℝ E)) ((stdOrthonormalBasis ℝ E).repr x) r
   simp_rw [Fintype.card_fin] at this
   convert this
   simp only [LinearIsometryEquiv.preimage_ball, LinearIsometryEquiv.symm_symm, _root_.map_zero]