Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic

Goal state before:
pp: Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : NormedAddCommGroup E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
X : Ω → E
inst✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure P
hX : AEMeasurable X P
h :
  ∀ (L : StrongDual ℝ E), charFunDual (Measure.map X P) L = cexp (↑(∫ (x : Ω), (⇑L ∘ X) x ∂P) * I - ↑Var[⇑L ∘ X; P] / 2)
t : StrongDual ℝ E
⊢ cexp (↑(∫ (x : Ω), (⇑t ∘ X) x ∂P) * I - ↑Var[⇑t ∘ X; P] / 2) =
    cexp ((∫ (x : Ω), ↑(t (X x)) ∂P) * I - ↑Var[⇑t ∘ X; P] / 2)

pp: case hX
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : NormedAddCommGroup E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
X : Ω → E
inst✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure P
hX : AEMeasurable X P
h :
  ∀ (L : StrongDual ℝ E), charFunDual (Measure.map X P) L = cexp (↑(∫ (x : Ω), (⇑L ∘ X) x ∂P) * I - ↑Var[⇑L ∘ X; P] / 2)
t : StrongDual ℝ E
⊢ AEMeasurable (⇑t) (Measure.map X P)

pp: case hY
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : NormedAddCommGroup E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
X : Ω → E
inst✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure P
hX : AEMeasurable X P
h :
  ∀ (L : StrongDual ℝ E), charFunDual (Measure.map X P) L = cexp (↑(∫ (x : Ω), (⇑L ∘ X) x ∂P) * I - ↑Var[⇑L ∘ X; P] / 2)
t : StrongDual ℝ E
⊢ AEMeasurable X P

pp: case hφ
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : NormedAddCommGroup E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
X : Ω → E
inst✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure P
hX : AEMeasurable X P
h :
  ∀ (L : StrongDual ℝ E), charFunDual (Measure.map X P) L = cexp (↑(∫ (x : Ω), (⇑L ∘ X) x ∂P) * I - ↑Var[⇑L ∘ X; P] / 2)
t : StrongDual ℝ E
⊢ AEMeasurable X P

pp: case hfm
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : NormedAddCommGroup E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
X : Ω → E
inst✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure P
hX : AEMeasurable X P
h :
  ∀ (L : StrongDual ℝ E), charFunDual (Measure.map X P) L = cexp (↑(∫ (x : Ω), (⇑L ∘ X) x ∂P) * I - ↑Var[⇑L ∘ X; P] / 2)
t : StrongDual ℝ E
⊢ AEStronglyMeasurable (fun x ↦ ↑(t x)) (Measure.map X P)

Tactic:
integral_complex_ofReal,

Goal state after:
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : NormedAddCommGroup E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
X : Ω → E
inst✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure P
hX : AEMeasurable X P
h :
  ∀ (L : StrongDual ℝ E), charFunDual (Measure.map X P) L = cexp (↑(∫ (x : Ω), (⇑L ∘ X) x ∂P) * I - ↑Var[⇑L ∘ X; P] / 2)
t : StrongDual ℝ E
⊢ cexp (↑(∫ (x : Ω), (⇑t ∘ X) x ∂P) * I - ↑Var[⇑t ∘ X; P] / 2) =
    cexp (↑(∫ (x : Ω), t (X x) ∂P) * I - ↑Var[⇑t ∘ X; P] / 2)

case hX
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : NormedAddCommGroup E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
X : Ω → E
inst✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure P
hX : AEMeasurable X P
h :
  ∀ (L : StrongDual ℝ E), charFunDual (Measure.map X P) L = cexp (↑(∫ (x : Ω), (⇑L ∘ X) x ∂P) * I - ↑Var[⇑L ∘ X; P] / 2)
t : StrongDual ℝ E
⊢ AEMeasurable (⇑t) (Measure.map X P)

case hY
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : NormedAddCommGroup E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
X : Ω → E
inst✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure P
hX : AEMeasurable X P
h :
  ∀ (L : StrongDual ℝ E), charFunDual (Measure.map X P) L = cexp (↑(∫ (x : Ω), (⇑L ∘ X) x ∂P) * I - ↑Var[⇑L ∘ X; P] / 2)
t : StrongDual ℝ E
⊢ AEMeasurable X P

case hφ
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : NormedAddCommGroup E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
X : Ω → E
inst✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure P
hX : AEMeasurable X P
h :
  ∀ (L : StrongDual ℝ E), charFunDual (Measure.map X P) L = cexp (↑(∫ (x : Ω), (⇑L ∘ X) x ∂P) * I - ↑Var[⇑L ∘ X; P] / 2)
t : StrongDual ℝ E
⊢ AEMeasurable X P

case hfm
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : NormedAddCommGroup E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
X : Ω → E
inst✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure P
hX : AEMeasurable X P
h :
  ∀ (L : StrongDual ℝ E), charFunDual (Measure.map X P) L = cexp (↑(∫ (x : Ω), (⇑L ∘ X) x ∂P) * I - ↑Var[⇑L ∘ X; P] / 2)
t : StrongDual ℝ E
⊢ AEStronglyMeasurable (fun x ↦ ↑(t x)) (Measure.map X P)