feat(Probability): translations of gaussians are gaussian (#25532)

If `μ` is gaussian, then `μ.map (fun x ↦ x + c)` is gaussian as well.
The same is true for `c + x`, `x - c`, `-x` and `c - x` instead of `x + c`.

Author: RemyDegenne

Mathlib/MeasureTheory/Group/Convolution.lean

@@ -44,23 +44,31 @@ theorem lintegral_mconv [MeasurableMul₂ M] {μ ν : Measure M} [SFinite ν]
   rw [mconv, lintegral_map hf measurable_mul, lintegral_prod]
   fun_prop
 
+@[to_additive]
+lemma dirac_mconv [MeasurableMul₂ M] (x : M) (μ : Measure M) [SFinite μ] :
+    (Measure.dirac x) ∗ₘ μ = μ.map (fun y ↦ x * y) := by
+  unfold mconv
+  rw [Measure.dirac_prod, map_map (by fun_prop) (by fun_prop)]
+  simp [Function.comp_def]
+
+@[to_additive]
+lemma mconv_dirac [MeasurableMul₂ M] (μ : Measure M) [SFinite μ] (x : M) :
+    μ ∗ₘ (Measure.dirac x) = μ.map (fun y ↦ y * x) := by
+  unfold mconv
+  rw [Measure.prod_dirac, map_map (by fun_prop) (by fun_prop)]
+  simp [Function.comp_def]
+
 /-- Convolution of the dirac measure at 1 with a measure μ returns μ. -/
 @[to_additive (attr := simp) "Convolution of the dirac measure at 0 with a measure μ returns μ."]
 theorem dirac_one_mconv [MeasurableMul₂ M] (μ : Measure M) [SFinite μ] :
     (Measure.dirac 1) ∗ₘ μ = μ := by
-  unfold mconv
-  rw [MeasureTheory.Measure.dirac_prod, map_map (by fun_prop)]
-  · simp only [Function.comp_def, one_mul, map_id']
-  fun_prop
+  simp [dirac_mconv]
 
 /-- Convolution of a measure μ with the dirac measure at 1 returns μ. -/
 @[to_additive (attr := simp) "Convolution of a measure μ with the dirac measure at 0 returns μ."]
 theorem mconv_dirac_one [MeasurableMul₂ M]
     (μ : Measure M) [SFinite μ] : μ ∗ₘ (Measure.dirac 1) = μ := by
-  unfold mconv
-  rw [MeasureTheory.Measure.prod_dirac, map_map (by fun_prop)]
-  · simp only [Function.comp_def, mul_one, map_id']
-  fun_prop
+  simp [mconv_dirac]
 
 /-- Convolution of the zero measure with a measure μ returns the zero measure. -/
 @[to_additive (attr := simp) "Convolution of the zero measure with a measure μ returns

Mathlib/MeasureTheory/Measure/CharacteristicFunction.lean

@@ -196,7 +196,30 @@ lemma charFun_map_mul {μ : Measure ℝ} (r t : ℝ) :
     charFun (μ.map (r * ·)) t = charFun μ (r * t) := charFun_map_smul r t
 
 variable {E : Type*} [MeasurableSpace E] {μ ν : Measure E} {t : E}
-  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [BorelSpace E] [SecondCountableTopology E]
+  [NormedAddCommGroup E] [InnerProductSpace ℝ E]
+
+@[simp]
+lemma charFun_dirac [OpensMeasurableSpace E] {x : E} (t : E) :
+    charFun (Measure.dirac x) t = cexp (⟪x, t⟫ * I) := by
+  rw [charFun_apply, integral_dirac]
+
+lemma charFun_map_add_const [BorelSpace E] (r t : E) :
+    charFun (μ.map (· + r)) t = charFun μ t * cexp (⟪r, t⟫ * I) := by
+  rw [charFun_apply, charFun_apply, integral_map (by fun_prop) (by fun_prop),
+    ← integral_mul_const]
+  congr with a
+  rw [← Complex.exp_add]
+  congr
+  rw [inner_add_left]
+  simp only [ofReal_add]
+  ring
+
+lemma charFun_map_const_add [BorelSpace E] (r t : E) :
+    charFun (μ.map (r + ·)) t = charFun μ t * cexp (⟪r, t⟫ * I) := by
+  simp_rw [add_comm r]
+  exact charFun_map_add_const _ _
+
+variable [BorelSpace E] [SecondCountableTopology E]
 
 /-- If the characteristic functions `charFun` of two finite measures `μ` and `ν` on
 a complete second-countable inner product space coincide, then `μ = ν`. -/
@@ -270,6 +293,21 @@ lemma charFunDual_dirac [OpensMeasurableSpace E] {x : E} (L : Dual ℝ E) :
     charFunDual (Measure.dirac x) L = cexp (L x * I) := by
   rw [charFunDual_apply, integral_dirac]
 
+lemma charFunDual_map_add_const [BorelSpace E] (r : E) (L : Dual ℝ E) :
+    charFunDual (μ.map (· + r)) L = charFunDual μ L * cexp (L r * I) := by
+  rw [charFunDual_apply, charFunDual_apply, integral_map (by fun_prop) (by fun_prop),
+    ← integral_mul_const]
+  congr with a
+  rw [← Complex.exp_add]
+  congr
+  simp only [map_add, ofReal_add]
+  ring
+
+lemma charFunDual_map_const_add [BorelSpace E] (r : E) (L : Dual ℝ E) :
+    charFunDual (μ.map (r + ·)) L = charFunDual μ L * cexp (L r * I) := by
+  simp_rw [add_comm r]
+  exact charFunDual_map_add_const _ _
+
 /-- The characteristic function of a product of measures is a product of
 characteristic functions. -/
 lemma charFunDual_prod [SFinite μ] [SFinite ν] (L : Dual ℝ (E × F)) :

Mathlib/Probability/Distributions/Gaussian/Basic.lean

@@ -153,4 +153,31 @@ instance isGaussian_conv [SecondCountableTopology E]
       IsGaussian.map_eq_gaussianReal L, gaussianReal_conv_gaussianReal]
     congr <;> simp [variance_nonneg]
 
+instance (c : E) : IsGaussian (μ.map (fun x ↦ x + c)) := by
+  refine isGaussian_of_charFunDual_eq fun L ↦ ?_
+  rw [charFunDual_map_add_const, IsGaussian.charFunDual_eq, ← exp_add]
+  have hL_comp : L ∘ (fun x ↦ x + c) = fun x ↦ L x + L c := by ext; simp
+  rw [variance_map (by fun_prop) (by fun_prop), integral_map (by fun_prop) (by fun_prop),
+    hL_comp, variance_add_const (by fun_prop), integral_complex_ofReal, integral_complex_ofReal]
+  simp only [map_add, ofReal_add]
+  rw [integral_add (by fun_prop) (by fun_prop)]
+  congr
+  simp only [integral_const, measureReal_univ_eq_one, smul_eq_mul, one_mul, ofReal_add]
+  ring
+
+instance (c : E) : IsGaussian (μ.map (fun x ↦ c + x)) := by simp_rw [add_comm c]; infer_instance
+
+instance (c : E) : IsGaussian (μ.map (fun x ↦ x - c)) := by simp_rw [sub_eq_add_neg]; infer_instance
+
+instance : IsGaussian (μ.map (fun x ↦ -x)) := by
+  change IsGaussian (μ.map (ContinuousLinearEquiv.neg ℝ))
+  infer_instance
+
+instance (c : E) : IsGaussian (μ.map (fun x ↦ c - x)) := by
+  simp_rw [sub_eq_add_neg]
+  suffices IsGaussian ((μ.map (fun x ↦ -x)).map (fun x ↦ c + x)) by
+    rw [Measure.map_map (by fun_prop) (by fun_prop)] at this
+    convert this using 1
+  infer_instance
+
 end ProbabilityTheory