awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Fernique (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
inst_4 : IsGaussian μ
inst_5 : CompleteSpace E
inst_6 : SecondCountableTopology E
hμ : Eq (α := E) (∫ (x : E), id x ∂μ) 0
θ : ℝ
⊢ Measure.map (⇑(ContinuousLinearMap.rotation θ) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
have refine : ∀ (L : StrongDual ℝ E), Eq (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) 0
Tactic: refine map_rotation_eq_self_of_forall_strongDual_eq_zero (fun L ↦ ?_) θ
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic (goal)
Goal:
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : TopologicalSpace E
inst_1 : AddCommMonoid E
inst_2 : Module ℝ E
mE : MeasurableSpace E
X Y : Ω → E
hX : HasGaussianLaw X P
h : X =ᶠ[ae P] Y
⊢ IsGaussian (mE := mE) (Measure.map Y P)
have rw : IsGaussian (mE := mE) (Measure.map X P)
Tactic: rw [← Measure.map_congr h]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic (hypothesis)
Goal:
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : TopologicalSpace E
inst_1 : AddCommMonoid E
inst_2 : Module ℝ E
mE : MeasurableSpace E
X : Ω → E
F : Type u_5
inst_3 : TopologicalSpace F
inst_4 : AddCommMonoid F
inst_5 : Module ℝ F
inst_6 : MeasurableSpace F
inst_7 : OpensMeasurableSpace F
L : E →L[ℝ] F
hX : HasGaussianLaw X P
hL : Measurable.{u_2, u_5} (α := E) (β := F) (⇑L : (a : E) → F)
⊢ IsGaussian.{u_5} (E := F) (mE := inst_6) (Measure.map ((⇑L : (a : E) → F) ∘ X) P)
have this : IsGaussian (mE := mE) (Measure.map X P)
Tactic: have := hX.isGaussian_map
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic (goal)
Goal:
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : TopologicalSpace E
inst_1 : AddCommMonoid E
inst_2 : Module ℝ E
mE : MeasurableSpace E
X : Ω → E
F : Type u_5
inst_3 : TopologicalSpace F
inst_4 : AddCommMonoid F
inst_5 : Module ℝ F
inst_6 : MeasurableSpace F
inst_7 : OpensMeasurableSpace F
L : E →L[ℝ] F
hX : HasGaussianLaw X P
hL : Measurable.{u_2, u_5} (α := E) (β := F) (⇑L : (a : E) → F)
this : IsGaussian (mE := mE) (Measure.map X P)
⊢ IsGaussian.{u_5} (E := F) (mE := inst_6) (Measure.map ((⇑L : (a : E) → F) ∘ X) P)
have rw : IsGaussian.{u_5} (E := F) (mE := inst_6) (Measure.map (⇑L : (a : E) → F) (Measure.map X P))
Tactic: rw [← AEMeasurable.map_map_of_aemeasurable]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic (goal)
Goal:
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : TopologicalSpace E
inst_1 : AddCommMonoid E
inst_2 : Module ℝ E
mE : MeasurableSpace E
X : Ω → E
F : Type u_5
inst_3 : TopologicalSpace F
inst_4 : AddCommMonoid F
inst_5 : Module ℝ F
inst_6 : MeasurableSpace F
inst_7 : OpensMeasurableSpace F
L : E →L[ℝ] F
hX : HasGaussianLaw X P
hL : Measurable.{u_2, u_5} (α := E) (β := F) (⇑L : (a : E) → F)
this : IsGaussian (mE := mE) (Measure.map X P)
rw : IsGaussian.{u_5} (E := F) (mE := inst_6) (Measure.map (⇑L : (a : E) → F) (Measure.map X P))
⊢ IsGaussian.{u_5} (E := F) (mE := inst_6) (Measure.map ((⇑L : (a : E) → F) ∘ X) P)
have hg : AEMeasurable.{u_2, u_5} (β := F) (_m := mE) (⇑L : (a : E) → F) (Measure.map X P)
Tactic: rw [← AEMeasurable.map_map_of_aemeasurable]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic (goal)
Goal:
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : TopologicalSpace E
inst_1 : AddCommMonoid E
inst_2 : Module ℝ E
mE : MeasurableSpace E
X : Ω → E
F : Type u_5
inst_3 : TopologicalSpace F
inst_4 : AddCommMonoid F
inst_5 : Module ℝ F
inst_6 : MeasurableSpace F
inst_7 : OpensMeasurableSpace F
L : E →L[ℝ] F
hX : HasGaussianLaw X P
hL : Measurable.{u_2, u_5} (α := E) (β := F) (⇑L : (a : E) → F)
this : IsGaussian (mE := mE) (Measure.map X P)
rw : IsGaussian.{u_5} (E := F) (mE := inst_6) (Measure.map (⇑L : (a : E) → F) (Measure.map X P))
hg : AEMeasurable.{u_2, u_5} (β := F) (_m := mE) (⇑L : (a : E) → F) (Measure.map X P)
⊢ IsGaussian.{u_5} (E := F) (mE := inst_6) (Measure.map ((⇑L : (a : E) → F) ∘ X) P)
have hf : AEMeasurable X P
Tactic: rw [← AEMeasurable.map_map_of_aemeasurable]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic (hypothesis)
Goal:
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
X : Ω → E
inst_3 : NormedSpace ℝ E
inst_4 : Subsingleton E
inst_5 : IsProbabilityMeasure P
⊢ IsGaussian (mE := inst_1) (Measure.map X P)
have this : IsProbabilityMeasure (m0 := inst_1) (Measure.map X P)
Tactic: have : IsProbabilityMeasure (P.map X) := P.isProbabilityMeasure_map (by fun_prop)
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic (goal)
Goal:
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
X : Ω → E
inst_3 : InnerProductSpace ℝ E
t : E
hX : HasGaussianLaw X P
⊢ charFun (mE := inst_1) (Measure.map X P) t =
    cexp ((↑(∫ (x : Ω), (fun (ω : Ω) ↦ ⟪t, X ω⟫) x ∂P) : ℂ) * I - (↑Var[fun (ω : Ω) ↦ ⟪t, X ω⟫; P] : ℂ) / 2)
have rw : cexp
    ((@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ (↑((fun (x : E) ↦ ⟪t, x⟫) x) : ℂ)) * I -
      (↑(variance (mΩ := inst_1) (fun (x : E) ↦ ⟪t, x⟫) (Measure.map X P)) : ℂ) / 2) =
  cexp ((↑(∫ (x : Ω), (fun (ω : Ω) ↦ ⟪t, X ω⟫) x ∂P) : ℂ) * I - (↑Var[fun (ω : Ω) ↦ ⟪t, X ω⟫; P] : ℂ) / 2)
Tactic: rw [hX.isGaussian_map.charFun_eq, integral_map hX.aemeasurable (by fun_prop),
    variance_map (by fun_prop) hX.aemeasurable, integral_complex_ofReal, Function.comp_def]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic (goal)
Goal:
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
X : Ω → E
inst_3 : InnerProductSpace ℝ E
t : E
hX : HasGaussianLaw X P
rw :
  cexp
      ((@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ (↑((fun (x : E) ↦ ⟪t, x⟫) x) : ℂ)) * I -
        (↑(variance (mΩ := inst_1) (fun (x : E) ↦ ⟪t, x⟫) (Measure.map X P)) : ℂ) / 2) =
    cexp ((↑(∫ (x : Ω), (fun (ω : Ω) ↦ ⟪t, X ω⟫) x ∂P) : ℂ) * I - (↑Var[fun (ω : Ω) ↦ ⟪t, X ω⟫; P] : ℂ) / 2)
⊢ charFun (mE := inst_1) (Measure.map X P) t =
    cexp ((↑(∫ (x : Ω), (fun (ω : Ω) ↦ ⟪t, X ω⟫) x ∂P) : ℂ) * I - (↑Var[fun (ω : Ω) ↦ ⟪t, X ω⟫; P] : ℂ) / 2)
have rw₁ : cexp
    ((∫ (x : Ω), (↑((fun (x : E) ↦ ⟪t, x⟫) (X x)) : ℂ) ∂P) * I -
      (↑(variance (mΩ := inst_1) (fun (x : E) ↦ ⟪t, x⟫) (Measure.map X P)) : ℂ) / 2) =
  cexp ((↑(∫ (x : Ω), (fun (ω : Ω) ↦ ⟪t, X ω⟫) x ∂P) : ℂ) * I - (↑Var[fun (ω : Ω) ↦ ⟪t, X ω⟫; P] : ℂ) / 2)
Tactic: rw [hX.isGaussian_map.charFun_eq, integral_map hX.aemeasurable (by fun_prop),
    variance_map (by fun_prop) hX.aemeasurable, integral_complex_ofReal, Function.comp_def]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic (goal)
Goal:
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
X : Ω → E
inst_3 : InnerProductSpace ℝ E
t : E
hX : HasGaussianLaw X P
rw :
  cexp
      ((@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ (↑((fun (x : E) ↦ ⟪t, x⟫) x) : ℂ)) * I -
        (↑(variance (mΩ := inst_1) (fun (x : E) ↦ ⟪t, x⟫) (Measure.map X P)) : ℂ) / 2) =
    cexp ((↑(∫ (x : Ω), (fun (ω : Ω) ↦ ⟪t, X ω⟫) x ∂P) : ℂ) * I - (↑Var[fun (ω : Ω) ↦ ⟪t, X ω⟫; P] : ℂ) / 2)
rw₁ :
  cexp
      ((∫ (x : Ω), (↑((fun (x : E) ↦ ⟪t, x⟫) (X x)) : ℂ) ∂P) * I -
        (↑(variance (mΩ := inst_1) (fun (x : E) ↦ ⟪t, x⟫) (Measure.map X P)) : ℂ) / 2) =
    cexp ((↑(∫ (x : Ω), (fun (ω : Ω) ↦ ⟪t, X ω⟫) x ∂P) : ℂ) * I - (↑Var[fun (ω : Ω) ↦ ⟪t, X ω⟫; P] : ℂ) / 2)
⊢ charFun (mE := inst_1) (Measure.map X P) t =
    cexp ((↑(∫ (x : Ω), (fun (ω : Ω) ↦ ⟪t, X ω⟫) x ∂P) : ℂ) * I - (↑Var[fun (ω : Ω) ↦ ⟪t, X ω⟫; P] : ℂ) / 2)
have rw₂ : cexp ((∫ (x : Ω), (↑((fun (x : E) ↦ ⟪t, x⟫) (X x)) : ℂ) ∂P) * I - (↑Var[(fun (x : E) ↦ ⟪t, x⟫) ∘ X; P] : ℂ) / 2) =
  cexp ((↑(∫ (x : Ω), (fun (ω : Ω) ↦ ⟪t, X ω⟫) x ∂P) : ℂ) * I - (↑Var[fun (ω : Ω) ↦ ⟪t, X ω⟫; P] : ℂ) / 2)
Tactic: rw [hX.isGaussian_map.charFun_eq, integral_map hX.aemeasurable (by fun_prop),
    variance_map (by fun_prop) hX.aemeasurable, integral_complex_ofReal, Function.comp_def]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic (goal)
Goal:
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
X : Ω → E
inst_3 : InnerProductSpace ℝ E
t : E
hX : HasGaussianLaw X P
rw :
  cexp
      ((@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ (↑((fun (x : E) ↦ ⟪t, x⟫) x) : ℂ)) * I -
        (↑(variance (mΩ := inst_1) (fun (x : E) ↦ ⟪t, x⟫) (Measure.map X P)) : ℂ) / 2) =
    cexp ((↑(∫ (x : Ω), (fun (ω : Ω) ↦ ⟪t, X ω⟫) x ∂P) : ℂ) * I - (↑Var[fun (ω : Ω) ↦ ⟪t, X ω⟫; P] : ℂ) / 2)
rw₁ :
  cexp
      ((∫ (x : Ω), (↑((fun (x : E) ↦ ⟪t, x⟫) (X x)) : ℂ) ∂P) * I -
        (↑(variance (mΩ := inst_1) (fun (x : E) ↦ ⟪t, x⟫) (Measure.map X P)) : ℂ) / 2) =
    cexp ((↑(∫ (x : Ω), (fun (ω : Ω) ↦ ⟪t, X ω⟫) x ∂P) : ℂ) * I - (↑Var[fun (ω : Ω) ↦ ⟪t, X ω⟫; P] : ℂ) / 2)
rw₂ :
  cexp ((∫ (x : Ω), (↑((fun (x : E) ↦ ⟪t, x⟫) (X x)) : ℂ) ∂P) * I - (↑Var[(fun (x : E) ↦ ⟪t, x⟫) ∘ X; P] : ℂ) / 2) =
    cexp ((↑(∫ (x : Ω), (fun (ω : Ω) ↦ ⟪t, X ω⟫) x ∂P) : ℂ) * I - (↑Var[fun (ω : Ω) ↦ ⟪t, X ω⟫; P] : ℂ) / 2)
⊢ charFun (mE := inst_1) (Measure.map X P) t =
    cexp ((↑(∫ (x : Ω), (fun (ω : Ω) ↦ ⟪t, X ω⟫) x ∂P) : ℂ) * I - (↑Var[fun (ω : Ω) ↦ ⟪t, X ω⟫; P] : ℂ) / 2)
have rw₃ : cexp ((↑(∫ (x : Ω), (fun (x : E) ↦ ⟪t, x⟫) (X x) ∂P) : ℂ) * I - (↑Var[(fun (x : E) ↦ ⟪t, x⟫) ∘ X; P] : ℂ) / 2) =
  cexp ((↑(∫ (x : Ω), (fun (ω : Ω) ↦ ⟪t, X ω⟫) x ∂P) : ℂ) * I - (↑Var[fun (ω : Ω) ↦ ⟪t, X ω⟫; P] : ℂ) / 2)
Tactic: rw [hX.isGaussian_map.charFun_eq, integral_map hX.aemeasurable (by fun_prop),
    variance_map (by fun_prop) hX.aemeasurable, integral_complex_ofReal, Function.comp_def]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic (goal)
Goal:
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
X : Ω → E
inst_3 : InnerProductSpace ℝ E
t : E
hX : HasGaussianLaw X P
rw :
  cexp
      ((@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ (↑((fun (x : E) ↦ ⟪t, x⟫) x) : ℂ)) * I -
        (↑(variance (mΩ := inst_1) (fun (x : E) ↦ ⟪t, x⟫) (Measure.map X P)) : ℂ) / 2) =
    cexp ((↑(∫ (x : Ω), (fun (ω : Ω) ↦ ⟪t, X ω⟫) x ∂P) : ℂ) * I - (↑Var[fun (ω : Ω) ↦ ⟪t, X ω⟫; P] : ℂ) / 2)
rw₁ :
  cexp
      ((∫ (x : Ω), (↑((fun (x : E) ↦ ⟪t, x⟫) (X x)) : ℂ) ∂P) * I -
        (↑(variance (mΩ := inst_1) (fun (x : E) ↦ ⟪t, x⟫) (Measure.map X P)) : ℂ) / 2) =
    cexp ((↑(∫ (x : Ω), (fun (ω : Ω) ↦ ⟪t, X ω⟫) x ∂P) : ℂ) * I - (↑Var[fun (ω : Ω) ↦ ⟪t, X ω⟫; P] : ℂ) / 2)
rw₂ :
  cexp ((∫ (x : Ω), (↑((fun (x : E) ↦ ⟪t, x⟫) (X x)) : ℂ) ∂P) * I - (↑Var[(fun (x : E) ↦ ⟪t, x⟫) ∘ X; P] : ℂ) / 2) =
    cexp ((↑(∫ (x : Ω), (fun (ω : Ω) ↦ ⟪t, X ω⟫) x ∂P) : ℂ) * I - (↑Var[fun (ω : Ω) ↦ ⟪t, X ω⟫; P] : ℂ) / 2)
rw₃ :
  cexp ((↑(∫ (x : Ω), (fun (x : E) ↦ ⟪t, x⟫) (X x) ∂P) : ℂ) * I - (↑Var[(fun (x : E) ↦ ⟪t, x⟫) ∘ X; P] : ℂ) / 2) =
    cexp ((↑(∫ (x : Ω), (fun (ω : Ω) ↦ ⟪t, X ω⟫) x ∂P) : ℂ) * I - (↑Var[fun (ω : Ω) ↦ ⟪t, X ω⟫; P] : ℂ) / 2)
⊢ charFun (mE := inst_1) (Measure.map X P) t =
    cexp ((↑(∫ (x : Ω), (fun (ω : Ω) ↦ ⟪t, X ω⟫) x ∂P) : ℂ) * I - (↑Var[fun (ω : Ω) ↦ ⟪t, X ω⟫; P] : ℂ) / 2)
have rw₄ : cexp ((↑(∫ (x : Ω), (fun (x : E) ↦ ⟪t, x⟫) (X x) ∂P) : ℂ) * I - (↑Var[fun (x : Ω) ↦ ⟪t, X x⟫; P] : ℂ) / 2) =
  cexp ((↑(∫ (x : Ω), (fun (ω : Ω) ↦ ⟪t, X ω⟫) x ∂P) : ℂ) * I - (↑Var[fun (ω : Ω) ↦ ⟪t, X ω⟫; P] : ℂ) / 2)
Tactic: rw [hX.isGaussian_map.charFun_eq, integral_map hX.aemeasurable (by fun_prop),
    variance_map (by fun_prop) hX.aemeasurable, integral_complex_ofReal, Function.comp_def]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic (goal)
Goal:
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
X : Ω → E
inst_3 : CompleteSpace E
inst_4 : InnerProductSpace ℝ E
inst_5 : IsFiniteMeasure P
hX : AEMeasurable X P
h :
  ∀ (t : E),
    charFun (mE := inst_1) (Measure.map X P) t =
      cexp ((↑(∫ (x : Ω), (fun (ω : Ω) ↦ ⟪t, X ω⟫) x ∂P) : ℂ) * I - (↑Var[fun (ω : Ω) ↦ ⟪t, X ω⟫; P] : ℂ) / 2)
⊢ HasGaussianLaw X P
have refine : ∀ (t : E),
  charFun (mE := inst_1) (Measure.map X P) t =
    cexp
      ((@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ (↑((fun (x : E) ↦ ⟪t, x⟫) x) : ℂ)) * I -
        (↑(variance (mΩ := inst_1) (fun (x : E) ↦ ⟪t, x⟫) (Measure.map X P)) : ℂ) / 2)
Tactic: refine ⟨isGaussian_iff_charFun_eq.2 fun t ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic (goal)
Goal:
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
X : Ω → E
inst_3 : CompleteSpace E
inst_4 : InnerProductSpace ℝ E
inst_5 : IsFiniteMeasure P
hX : AEMeasurable X P
h :
  ∀ (t : E),
    charFun (mE := inst_1) (Measure.map X P) t =
      cexp ((↑(∫ (x : Ω), (fun (ω : Ω) ↦ ⟪t, X ω⟫) x ∂P) : ℂ) * I - (↑Var[fun (ω : Ω) ↦ ⟪t, X ω⟫; P] : ℂ) / 2)
t : E
⊢ charFun (mE := inst_1) (Measure.map X P) t =
    cexp
      ((@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ (↑((fun (x : E) ↦ ⟪t, x⟫) x) : ℂ)) * I -
        (↑(variance (mΩ := inst_1) (fun (x : E) ↦ ⟪t, x⟫) (Measure.map X P)) : ℂ) / 2)
have hX₁ : AEMeasurable (β := ℝ) (_m := inst_1) (fun (x : E) ↦ ⟪t, x⟫) (Measure.map X P)
Tactic: rw [h, integral_map, variance_map, integral_complex_ofReal, Function.comp_def]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic (goal)
Goal:
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
X : Ω → E
inst_3 : CompleteSpace E
inst_4 : InnerProductSpace ℝ E
inst_5 : IsFiniteMeasure P
hX : AEMeasurable X P
h :
  ∀ (t : E),
    charFun (mE := inst_1) (Measure.map X P) t =
      cexp ((↑(∫ (x : Ω), (fun (ω : Ω) ↦ ⟪t, X ω⟫) x ∂P) : ℂ) * I - (↑Var[fun (ω : Ω) ↦ ⟪t, X ω⟫; P] : ℂ) / 2)
t : E
hX₁ : AEMeasurable (β := ℝ) (_m := inst_1) (fun (x : E) ↦ ⟪t, x⟫) (Measure.map X P)
hY hφ : AEMeasurable X P
⊢ charFun (mE := inst_1) (Measure.map X P) t =
    cexp
      ((@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ (↑((fun (x : E) ↦ ⟪t, x⟫) x) : ℂ)) * I -
        (↑(variance (mΩ := inst_1) (fun (x : E) ↦ ⟪t, x⟫) (Measure.map X P)) : ℂ) / 2)
have hfm : AEStronglyMeasurable (β := ℂ) (m₀ := inst_1) (fun (x : E) ↦ (↑((fun (x : E) ↦ ⟪t, x⟫) x) : ℂ)) (Measure.map X P)
Tactic: rw [h, integral_map, variance_map, integral_complex_ofReal, Function.comp_def]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic (goal)
Goal:
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
X : Ω → E
inst_3 : NormedSpace ℝ E
L : StrongDual ℝ E
hX : HasGaussianLaw X P
⊢ charFunDual (mE := inst_1) (Measure.map X P) L =
    cexp ((↑(∫ (x : Ω), ((⇑L : (a : E) → ℝ) ∘ X) x ∂P) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ) ∘ X; P] : ℂ) / 2)
have rw : cexp
    ((@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ (↑((L : (a : E) → ℝ) x) : ℂ)) * I -
      (↑(variance (mΩ := inst_1) (⇑L : (a : E) → ℝ) (Measure.map X P)) : ℂ) / 2) =
  cexp ((↑(∫ (x : Ω), ((⇑L : (a : E) → ℝ) ∘ X) x ∂P) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ) ∘ X; P] : ℂ) / 2)
Tactic: rw [hX.isGaussian_map.charFunDual_eq, integral_map hX.aemeasurable (by fun_prop),
    variance_map (by fun_prop) hX.aemeasurable, integral_complex_ofReal, Function.comp_def]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic (goal)
Goal:
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
X : Ω → E
inst_3 : NormedSpace ℝ E
L : StrongDual ℝ E
hX : HasGaussianLaw X P
rw :
  cexp
      ((@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ (↑((L : (a : E) → ℝ) x) : ℂ)) * I -
        (↑(variance (mΩ := inst_1) (⇑L : (a : E) → ℝ) (Measure.map X P)) : ℂ) / 2) =
    cexp ((↑(∫ (x : Ω), ((⇑L : (a : E) → ℝ) ∘ X) x ∂P) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ) ∘ X; P] : ℂ) / 2)
⊢ charFunDual (mE := inst_1) (Measure.map X P) L =
    cexp ((↑(∫ (x : Ω), ((⇑L : (a : E) → ℝ) ∘ X) x ∂P) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ) ∘ X; P] : ℂ) / 2)
have rw₁ : cexp
    ((∫ (x : Ω), (↑((L : (a : E) → ℝ) (X x)) : ℂ) ∂P) * I -
      (↑(variance (mΩ := inst_1) (⇑L : (a : E) → ℝ) (Measure.map X P)) : ℂ) / 2) =
  cexp ((↑(∫ (x : Ω), ((⇑L : (a : E) → ℝ) ∘ X) x ∂P) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ) ∘ X; P] : ℂ) / 2)
Tactic: rw [hX.isGaussian_map.charFunDual_eq, integral_map hX.aemeasurable (by fun_prop),
    variance_map (by fun_prop) hX.aemeasurable, integral_complex_ofReal, Function.comp_def]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic (goal)
Goal:
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
X : Ω → E
inst_3 : NormedSpace ℝ E
L : StrongDual ℝ E
hX : HasGaussianLaw X P
rw :
  cexp
      ((@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ (↑((L : (a : E) → ℝ) x) : ℂ)) * I -
        (↑(variance (mΩ := inst_1) (⇑L : (a : E) → ℝ) (Measure.map X P)) : ℂ) / 2) =
    cexp ((↑(∫ (x : Ω), ((⇑L : (a : E) → ℝ) ∘ X) x ∂P) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ) ∘ X; P] : ℂ) / 2)
rw₁ :
  cexp
      ((∫ (x : Ω), (↑((L : (a : E) → ℝ) (X x)) : ℂ) ∂P) * I -
        (↑(variance (mΩ := inst_1) (⇑L : (a : E) → ℝ) (Measure.map X P)) : ℂ) / 2) =
    cexp ((↑(∫ (x : Ω), ((⇑L : (a : E) → ℝ) ∘ X) x ∂P) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ) ∘ X; P] : ℂ) / 2)
⊢ charFunDual (mE := inst_1) (Measure.map X P) L =
    cexp ((↑(∫ (x : Ω), ((⇑L : (a : E) → ℝ) ∘ X) x ∂P) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ) ∘ X; P] : ℂ) / 2)
have rw₂ : cexp ((∫ (x : Ω), (↑((L : (a : E) → ℝ) (X x)) : ℂ) ∂P) * I - (↑Var[(⇑L : (a : E) → ℝ) ∘ X; P] : ℂ) / 2) =
  cexp ((↑(∫ (x : Ω), ((⇑L : (a : E) → ℝ) ∘ X) x ∂P) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ) ∘ X; P] : ℂ) / 2)
Tactic: rw [hX.isGaussian_map.charFunDual_eq, integral_map hX.aemeasurable (by fun_prop),
    variance_map (by fun_prop) hX.aemeasurable, integral_complex_ofReal, Function.comp_def]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic (goal)
Goal:
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
X : Ω → E
inst_3 : NormedSpace ℝ E
L : StrongDual ℝ E
hX : HasGaussianLaw X P
rw :
  cexp
      ((@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ (↑((L : (a : E) → ℝ) x) : ℂ)) * I -
        (↑(variance (mΩ := inst_1) (⇑L : (a : E) → ℝ) (Measure.map X P)) : ℂ) / 2) =
    cexp ((↑(∫ (x : Ω), ((⇑L : (a : E) → ℝ) ∘ X) x ∂P) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ) ∘ X; P] : ℂ) / 2)
rw₁ :
  cexp
      ((∫ (x : Ω), (↑((L : (a : E) → ℝ) (X x)) : ℂ) ∂P) * I -
        (↑(variance (mΩ := inst_1) (⇑L : (a : E) → ℝ) (Measure.map X P)) : ℂ) / 2) =
    cexp ((↑(∫ (x : Ω), ((⇑L : (a : E) → ℝ) ∘ X) x ∂P) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ) ∘ X; P] : ℂ) / 2)
rw₂ :
  cexp ((∫ (x : Ω), (↑((L : (a : E) → ℝ) (X x)) : ℂ) ∂P) * I - (↑Var[(⇑L : (a : E) → ℝ) ∘ X; P] : ℂ) / 2) =
    cexp ((↑(∫ (x : Ω), ((⇑L : (a : E) → ℝ) ∘ X) x ∂P) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ) ∘ X; P] : ℂ) / 2)
⊢ charFunDual (mE := inst_1) (Measure.map X P) L =
    cexp ((↑(∫ (x : Ω), ((⇑L : (a : E) → ℝ) ∘ X) x ∂P) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ) ∘ X; P] : ℂ) / 2)
have rw₃ : cexp ((↑(∫ (x : Ω), (L : (a : E) → ℝ) (X x) ∂P) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ) ∘ X; P] : ℂ) / 2) =
  cexp ((↑(∫ (x : Ω), ((⇑L : (a : E) → ℝ) ∘ X) x ∂P) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ) ∘ X; P] : ℂ) / 2)
Tactic: rw [hX.isGaussian_map.charFunDual_eq, integral_map hX.aemeasurable (by fun_prop),
    variance_map (by fun_prop) hX.aemeasurable, integral_complex_ofReal, Function.comp_def]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic (goal)
Goal:
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
X : Ω → E
inst_3 : NormedSpace ℝ E
L : StrongDual ℝ E
hX : HasGaussianLaw X P
rw :
  cexp
      ((@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ (↑((L : (a : E) → ℝ) x) : ℂ)) * I -
        (↑(variance (mΩ := inst_1) (⇑L : (a : E) → ℝ) (Measure.map X P)) : ℂ) / 2) =
    cexp ((↑(∫ (x : Ω), ((⇑L : (a : E) → ℝ) ∘ X) x ∂P) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ) ∘ X; P] : ℂ) / 2)
rw₁ :
  cexp
      ((∫ (x : Ω), (↑((L : (a : E) → ℝ) (X x)) : ℂ) ∂P) * I -
        (↑(variance (mΩ := inst_1) (⇑L : (a : E) → ℝ) (Measure.map X P)) : ℂ) / 2) =
    cexp ((↑(∫ (x : Ω), ((⇑L : (a : E) → ℝ) ∘ X) x ∂P) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ) ∘ X; P] : ℂ) / 2)
rw₂ :
  cexp ((∫ (x : Ω), (↑((L : (a : E) → ℝ) (X x)) : ℂ) ∂P) * I - (↑Var[(⇑L : (a : E) → ℝ) ∘ X; P] : ℂ) / 2) =
    cexp ((↑(∫ (x : Ω), ((⇑L : (a : E) → ℝ) ∘ X) x ∂P) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ) ∘ X; P] : ℂ) / 2)
rw₃ :
  cexp ((↑(∫ (x : Ω), (L : (a : E) → ℝ) (X x) ∂P) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ) ∘ X; P] : ℂ) / 2) =
    cexp ((↑(∫ (x : Ω), ((⇑L : (a : E) → ℝ) ∘ X) x ∂P) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ) ∘ X; P] : ℂ) / 2)
⊢ charFunDual (mE := inst_1) (Measure.map X P) L =
    cexp ((↑(∫ (x : Ω), ((⇑L : (a : E) → ℝ) ∘ X) x ∂P) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ) ∘ X; P] : ℂ) / 2)
have rw₄ : cexp ((↑(∫ (x : Ω), (L : (a : E) → ℝ) (X x) ∂P) : ℂ) * I - (↑Var[fun (x : Ω) ↦ (L : (a : E) → ℝ) (X x); P] : ℂ) / 2) =
  cexp
    ((↑(∫ (x : Ω), (fun (x : Ω) ↦ ((L : (a : E) → ℝ) (X x) : ℝ)) x ∂P) : ℂ) * I -
      (↑Var[fun (x : Ω) ↦ (L : (a : E) → ℝ) (X x); P] : ℂ) / 2)
Tactic: rw [hX.isGaussian_map.charFunDual_eq, integral_map hX.aemeasurable (by fun_prop),
    variance_map (by fun_prop) hX.aemeasurable, integral_complex_ofReal, Function.comp_def]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic (goal)
Goal:
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
X : Ω → E
inst_3 : NormedSpace ℝ E
inst_4 : IsFiniteMeasure P
hX : AEMeasurable X P
h :
  ∀ (L : StrongDual ℝ E),
    charFunDual (mE := inst_1) (Measure.map X P) L =
      cexp ((↑(∫ (x : Ω), ((⇑L : (a : E) → ℝ) ∘ X) x ∂P) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ) ∘ X; P] : ℂ) / 2)
⊢ HasGaussianLaw X P
have refine : ∀ (t : StrongDual ℝ E),
  charFunDual (mE := inst_1) (Measure.map X P) t =
    cexp
      ((@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ (↑((t : (a : E) → ℝ) x) : ℂ)) * I -
        (↑(variance (mΩ := inst_1) (⇑t : (a : E) → ℝ) (Measure.map X P)) : ℂ) / 2)
Tactic: refine ⟨isGaussian_iff_charFunDual_eq.2 fun t ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic (goal)
Goal:
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
X : Ω → E
inst_3 : NormedSpace ℝ E
inst_4 : IsFiniteMeasure P
hX : AEMeasurable X P
h :
  ∀ (L : StrongDual ℝ E),
    charFunDual (mE := inst_1) (Measure.map X P) L =
      cexp ((↑(∫ (x : Ω), ((⇑L : (a : E) → ℝ) ∘ X) x ∂P) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ) ∘ X; P] : ℂ) / 2)
t : StrongDual ℝ E
⊢ charFunDual (mE := inst_1) (Measure.map X P) t =
    cexp
      ((@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ (↑((t : (a : E) → ℝ) x) : ℂ)) * I -
        (↑(variance (mΩ := inst_1) (⇑t : (a : E) → ℝ) (Measure.map X P)) : ℂ) / 2)
have hX₁ : AEMeasurable (β := ℝ) (_m := inst_1) (⇑t : (a : E) → ℝ) (Measure.map X P)
Tactic: rw [h, integral_map, variance_map, integral_complex_ofReal, Function.comp_def]