chore(Analysis/SpecialFunctions/Exp): deal with TODO (#12781)

This deals with the TODO in Mathlib.Analysis.SpecialFuncitons.Exp:L146 by renaming `Continuous{WithinAt|At|On|}.exp` to `...rexp`.

Rationale: These are not in the `Real` namespace, and there are at least three different exponentials in Mathlib (`Real.exp`, `Complex.exp` and `NormedSpace.exp`), so it is better to make clear which one is used in these declarations.

Mathlib/Analysis/SpecialFunctions/Exp.lean

@@ -167,28 +167,32 @@ theorem Filter.Tendsto.rexp {l : Filter α} {f : α → ℝ} {z : ℝ} (hf : Ten
 
 variable [TopologicalSpace α] {f : α → ℝ} {s : Set α} {x : α}
 
--- TODO: the two next theorems should be `rexp` as well
 nonrec
-theorem ContinuousWithinAt.exp (h : ContinuousWithinAt f s x) :
-    ContinuousWithinAt (fun y => exp (f y)) s x :=
+theorem ContinuousWithinAt.rexp (h : ContinuousWithinAt f s x) :
+    ContinuousWithinAt (fun y ↦ exp (f y)) s x :=
   h.rexp
-#align continuous_within_at.exp ContinuousWithinAt.exp
+#align continuous_within_at.exp ContinuousWithinAt.rexp
+@[deprecated (since := "2024-05-09")] alias ContinuousWithinAt.exp := ContinuousWithinAt.rexp
 
 @[fun_prop]
 nonrec
-theorem ContinuousAt.exp (h : ContinuousAt f x) : ContinuousAt (fun y => exp (f y)) x :=
+theorem ContinuousAt.rexp (h : ContinuousAt f x) : ContinuousAt (fun y ↦ exp (f y)) x :=
   h.rexp
-#align continuous_at.exp ContinuousAt.exp
+#align continuous_at.exp ContinuousAt.rexp
+@[deprecated (since := "2024-05-09")] alias ContinuousAt.exp := ContinuousAt.rexp
 
 @[fun_prop]
-theorem ContinuousOn.exp (h : ContinuousOn f s) : ContinuousOn (fun y => exp (f y)) s := fun x hx =>
-  (h x hx).exp
-#align continuous_on.exp ContinuousOn.exp
+theorem ContinuousOn.rexp (h : ContinuousOn f s) :
+    ContinuousOn (fun y ↦ exp (f y)) s :=
+  fun x hx ↦ (h x hx).rexp
+#align continuous_on.exp ContinuousOn.rexp
+@[deprecated (since := "2024-05-09")] alias ContinuousOn.exp := ContinuousOn.rexp
 
 @[fun_prop]
-theorem Continuous.exp (h : Continuous f) : Continuous fun y => exp (f y) :=
-  continuous_iff_continuousAt.2 fun _ => h.continuousAt.exp
-#align continuous.exp Continuous.exp
+theorem Continuous.rexp (h : Continuous f) : Continuous fun y ↦ exp (f y) :=
+  continuous_iff_continuousAt.2 fun _ ↦ h.continuousAt.rexp
+#align continuous.exp Continuous.rexp
+@[deprecated (since := "2024-05-09")] alias Continuous.exp := Continuous.rexp
 
 end RealContinuousExpComp
 

Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean

@@ -73,11 +73,11 @@ theorem GammaIntegral_convergent {s : ℝ} (h : 0 < s) :
   rw [← Ioc_union_Ioi_eq_Ioi (@zero_le_one ℝ _ _ _ _), integrableOn_union]
   constructor
   · rw [← integrableOn_Icc_iff_integrableOn_Ioc]
-    refine' IntegrableOn.continuousOn_mul continuousOn_id.neg.exp _ isCompact_Icc
+    refine' IntegrableOn.continuousOn_mul continuousOn_id.neg.rexp _ isCompact_Icc
     refine' (intervalIntegrable_iff_integrableOn_Icc_of_le zero_le_one).mp _
     exact intervalIntegrable_rpow' (by linarith)
   · refine' integrable_of_isBigO_exp_neg one_half_pos _ (Gamma_integrand_isLittleO _).isBigO
-    refine' continuousOn_id.neg.exp.mul (continuousOn_id.rpow_const _)
+    refine' continuousOn_id.neg.rexp.mul (continuousOn_id.rpow_const _)
     intro x hx
     exact Or.inl ((zero_lt_one : (0 : ℝ) < 1).trans_le hx).ne'
 #align real.Gamma_integral_convergent Real.GammaIntegral_convergent
@@ -96,7 +96,7 @@ theorem GammaIntegral_convergent {s : ℂ} (hs : 0 < s.re) :
     IntegrableOn (fun x => (-x).exp * x ^ (s - 1) : ℝ → ℂ) (Ioi 0) := by
   constructor
   · refine' ContinuousOn.aestronglyMeasurable _ measurableSet_Ioi
-    apply (continuous_ofReal.comp continuous_neg.exp).continuousOn.mul
+    apply (continuous_ofReal.comp continuous_neg.rexp).continuousOn.mul
     apply ContinuousAt.continuousOn
     intro x hx
     have : ContinuousAt (fun x : ℂ => x ^ (s - 1)) ↑x :=
@@ -184,7 +184,7 @@ private theorem Gamma_integrand_deriv_integrable_B {s : ℂ} (hs : 0 < s.re) {Y
   rw [this, intervalIntegrable_iff_integrableOn_Ioc_of_le hY]
   constructor
   · refine' (continuousOn_const.mul _).aestronglyMeasurable measurableSet_Ioc
-    apply (continuous_ofReal.comp continuous_neg.exp).continuousOn.mul
+    apply (continuous_ofReal.comp continuous_neg.rexp).continuousOn.mul
     apply ContinuousAt.continuousOn
     intro x hx
     refine' (_ : ContinuousAt (fun x : ℂ => x ^ (s - 1)) _).comp continuous_ofReal.continuousAt
@@ -213,7 +213,7 @@ theorem partialGamma_add_one {s : ℂ} (hs : 0 < s.re) {X : ℝ} (hX : 0 ≤ X)
       · simpa only [mul_one] using t.comp_ofReal
       · exact ofReal_mem_slitPlane.2 hx.1
     simpa only [ofReal_neg, neg_mul] using d1.ofReal_comp.mul d2
-  have cont := (continuous_ofReal.comp continuous_neg.exp).mul (continuous_ofReal_cpow_const hs)
+  have cont := (continuous_ofReal.comp continuous_neg.rexp).mul (continuous_ofReal_cpow_const hs)
   have der_ible :=
     (Gamma_integrand_deriv_integrable_A hs hX).add (Gamma_integrand_deriv_integrable_B hs hX)
   have int_eval := integral_eq_sub_of_hasDerivAt_of_le hX cont.continuousOn F_der_I der_ible

Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean

@@ -63,7 +63,7 @@ theorem rpow_mul_exp_neg_mul_sq_isLittleO_exp_neg {b : ℝ} (hb : 0 < b) (s : 
 theorem integrableOn_rpow_mul_exp_neg_rpow {p s : ℝ} (hs : -1 < s) (hp : 1 ≤ p) :
     IntegrableOn (fun x : ℝ => x ^ s * exp (- x ^ p)) (Ioi 0) := by
   obtain hp | hp := le_iff_lt_or_eq.mp hp
-  · have h_exp : ∀ x, ContinuousAt (fun x => exp (- x)) x := fun x => continuousAt_neg.exp
+  · have h_exp : ∀ x, ContinuousAt (fun x => exp (- x)) x := fun x => continuousAt_neg.rexp
     rw [← Ioc_union_Ioi_eq_Ioi zero_le_one, integrableOn_union]
     constructor
     · rw [← integrableOn_Icc_iff_integrableOn_Ioc]

Mathlib/Probability/Distributions/Exponential.lean

@@ -151,7 +151,7 @@ lemma lintegral_exponentialPDF_eq_antiDeriv {r : ℝ} (hr : 0 < r) (x : ℝ) :
       · simp only [intervalIntegrable_iff, uIoc_of_le h]
         exact Integrable.const_mul (exp_neg_integrableOn_Ioc hr) _
       · have : Continuous (fun a ↦ rexp (-(r * a))) := by
-          simp only [← neg_mul]; exact (continuous_mul_left (-r)).exp
+          simp only [← neg_mul]; exact (continuous_mul_left (-r)).rexp
         exact Continuous.continuousOn (Continuous.comp' (continuous_mul_left (-1)) this)
       · simp only [neg_mul, one_mul]
         exact fun _ _ ↦ HasDerivAt.hasDerivWithinAt hasDerivAt_neg_exp_mul_exp