awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
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
this : IsProbabilityMeasure (m0 := inst_1) (Measure.map X P)
⊢ IsGaussian (mE := inst_1) (Measure.map X P)

Tactic:
.of_subsingleton

Premises used: ProbabilityTheory.IsGaussian.of_subsingleton
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
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
this : IsProbabilityMeasure (m0 := inst_1) (Measure.map X P)
⊢ IsGaussian (mE := inst_1) (Measure.map X P)

Tactic:
exact .of_subsingleton
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
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
⊢ AEStronglyMeasurable (β := ℂ) (m₀ := inst_1) (fun (x : E) ↦ (↑((fun (x : E) ↦ ⟪t, x⟫) x) : ℂ)) (Measure.map X P)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
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
⊢ AEMeasurable (β := ℝ) (_m := inst_1) (fun (x : E) ↦ ⟪t, x⟫) (Measure.map X P)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
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)
rw₄ 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)
⊢ charFun (mE := inst_1) (Measure.map X P) t =
    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]

Premises used: MeasureTheory.integral_map, Function.comp_def, ProbabilityTheory.variance_map, integral_complex_ofReal, ProbabilityTheory.IsGaussian.charFun_eq, ProbabilityTheory.HasGaussianLaw.aemeasurable
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
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

Tactic:
⟨isGaussian_iff_charFun_eq.2 fun t ↦ ?_⟩

Premises used: Iff.mpr, ProbabilityTheory.isGaussian_iff_charFun_eq, ProbabilityTheory.HasGaussianLaw.mk
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
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)
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)
⊢ HasGaussianLaw X P

Tactic:
refine ⟨isGaussian_iff_charFun_eq.2 fun t ↦ ?_⟩
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
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
hfm : AEStronglyMeasurable (β := ℂ) (m₀ := inst_1) (fun (x : E) ↦ (↑((fun (x : E) ↦ ⟪t, x⟫) x) : ℂ)) (Measure.map 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)

Tactic:
rw [h, integral_map, variance_map, integral_complex_ofReal, Function.comp_def]

Premises used: MeasureTheory.integral_map, Function.comp_def, ProbabilityTheory.variance_map, integral_complex_ofReal
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
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
⊢ AEMeasurable (β := ℝ) (_m := inst_1) (fun (x : E) ↦ ⟪t, x⟫) (Measure.map X P)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
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
⊢ AEMeasurable X P

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
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
⊢ AEStronglyMeasurable (β := ℂ) (m₀ := inst_1) (fun (x : E) ↦ (↑((fun (x : E) ↦ ⟪t, x⟫) x) : ℂ)) (Measure.map X P)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
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
⊢ AEStronglyMeasurable (β := ℂ) (m₀ := inst_1) (fun (x : E) ↦ (↑((L : (a : E) → ℝ) x) : ℂ)) (Measure.map X P)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
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
⊢ AEMeasurable (β := ℝ) (_m := inst_1) (⇑L : (a : E) → ℝ) (Measure.map X P)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
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)
rw₄ 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)
⊢ 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)

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]

Premises used: MeasureTheory.integral_map, ProbabilityTheory.IsGaussian.charFunDual_eq, Function.comp_def, ProbabilityTheory.variance_map, integral_complex_ofReal, ProbabilityTheory.HasGaussianLaw.aemeasurable
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
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

Tactic:
⟨isGaussian_iff_charFunDual_eq.2 fun t ↦ ?_⟩

Premises used: Iff.mpr, ProbabilityTheory.isGaussian_iff_charFunDual_eq, ProbabilityTheory.HasGaussianLaw.mk
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
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)
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)
⊢ HasGaussianLaw X P

Tactic:
refine ⟨isGaussian_iff_charFunDual_eq.2 fun t ↦ ?_⟩
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
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
hX₁ : AEMeasurable (β := ℝ) (_m := inst_1) (⇑t : (a : E) → ℝ) (Measure.map X P)
hY hφ : AEMeasurable X P
hfm : AEStronglyMeasurable (β := ℂ) (m₀ := inst_1) (fun (x : E) ↦ (↑((t : (a : E) → ℝ) x) : ℂ)) (Measure.map X P)
⊢ 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:
rw [h, integral_map, variance_map, integral_complex_ofReal, Function.comp_def]

Premises used: MeasureTheory.integral_map, Function.comp_def, ProbabilityTheory.variance_map, integral_complex_ofReal
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
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
⊢ AEMeasurable (β := ℝ) (_m := inst_1) (⇑t : (a : E) → ℝ) (Measure.map X P)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
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
⊢ AEMeasurable X P

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
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
⊢ AEStronglyMeasurable (β := ℂ) (m₀ := inst_1) (fun (x : E) ↦ (↑((t : (a : E) → ℝ) x) : ℂ)) (Measure.map X P)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
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 ((↑(∫ (x : Ω), ((⇑L : (a : E) → ℝ) ∘ X) x ∂P) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ) ∘ X; P] : ℂ) / 2) =
    cexp ((↑(∫ (ω : Ω), (L : (a : E) → ℝ) (X ω) ∂P) : ℂ) * I - (↑Var[fun (ω : Ω) ↦ (L : (a : E) → ℝ) (X ω); P] : ℂ) / 2)
rw₁ rw₂ :
  cexp
      ((↑(∫ (x : Ω), (fun (x : Ω) ↦ ((L : (a : E) → ℝ) (X x) : ℝ)) x ∂P) : ℂ) * I -
        (↑Var[fun (x : Ω) ↦ (L : (a : E) → ℝ) (X x); P] : ℂ) / 2) =
    cexp ((↑(∫ (ω : Ω), (L : (a : E) → ℝ) (X ω) ∂P) : ℂ) * I - (↑Var[fun (ω : Ω) ↦ (L : (a : E) → ℝ) (X ω); P] : ℂ) / 2)
⊢ charFunDual (mE := inst_1) (Measure.map X P) L =
    cexp ((↑(∫ (ω : Ω), (L : (a : E) → ℝ) (X ω) ∂P) : ℂ) * I - (↑Var[fun (ω : Ω) ↦ (L : (a : E) → ℝ) (X ω); P] : ℂ) / 2)

Tactic:
rw [hX.charFunDual_map_eq, Function.comp_def]

Premises used: Function.comp_def, ProbabilityTheory.HasGaussianLaw.charFunDual_map_eq
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
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 : CompleteSpace E
inst_5 : SecondCountableTopology E
hX : HasGaussianLaw X P
p : ℝ≥0∞
hp : p ≠ ∞
rw : MemLp (m0 := inst_1) id p (Measure.map X P)
hg : AEStronglyMeasurable (m₀ := inst_1) id (Measure.map X P)
hf : AEMeasurable X P
rw₁ : MeasurableSpace E
⊢ MemLp X p P

Tactic:
rw [← Function.id_comp X, ← memLp_map_measure_iff]

Premises used: MeasureTheory.memLp_map_measure_iff, Function.id_comp
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
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 : CompleteSpace E
inst_5 : SecondCountableTopology E
hX : HasGaussianLaw X P
p : ℝ≥0∞
hp : p ≠ ∞
⊢ MemLp (m0 := inst_1) id p (Measure.map X P)

Tactic:
hX.isGaussian_map.memLp_id _ p hp

Premises used: ProbabilityTheory.IsGaussian.memLp_id
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
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 : CompleteSpace E
inst_5 : SecondCountableTopology E
hX : HasGaussianLaw X P
p : ℝ≥0∞
hp : p ≠ ∞
⊢ MemLp (m0 := inst_1) id p (Measure.map X P)

Tactic:
exact hX.isGaussian_map.memLp_id _ p hp

Premises used: ProbabilityTheory.IsGaussian.memLp_id
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
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 : CompleteSpace E
inst_5 : SecondCountableTopology E
hX : HasGaussianLaw X P
p : ℝ≥0∞
hp : p ≠ ∞
⊢ AEStronglyMeasurable (m₀ := inst_1) id (Measure.map X P)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
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 : CompleteSpace E
inst_5 : SecondCountableTopology E
hX : HasGaussianLaw X P
p : ℝ≥0∞
hp : p ≠ ∞
funProp : AEFinStronglyMeasurable.{u_1, u_2} (β := E) (fun (a : Ω) ↦ X a) P
⊢ AEMeasurable X P

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
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 : CompleteSpace E
inst_5 : SecondCountableTopology E
hX : HasGaussianLaw X P
⊢ Ne (α := ℝ≥0∞) 2 ∞

Tactic:
norm_num
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
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 : CompleteSpace E
inst_5 : SecondCountableTopology E
hX : HasGaussianLaw X P
⊢ Ne (α := ℝ≥0∞) 1 ∞

Tactic:
norm_num
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
Goal:
Ω : Type u_1
E : Type u_2
F : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
X : Ω → E
inst_3 : NormedSpace ℝ E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
hX : HasGaussianLaw X P
L : E →L[ℝ] F
⊢ Measurable.{u_2, u_3} (α := E) (β := F) (⇑L : (a : E) → F)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
Goal:
Ω : Type u_1
E : Type u_2
F : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
X : Ω → E
inst_3 : NormedSpace ℝ E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
hX : HasGaussianLaw X P
L : E →L[ℝ] F
⊢ HasGaussianLaw.{u_1, u_3} (E := F) (fun (ω : Ω) ↦ (L : (a : E) → F) (X ω)) P

Tactic:
hX.map L

Premises used: ProbabilityTheory.HasGaussianLaw.map
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
Goal:
Ω : Type u_1
E : Type u_2
F : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
X : Ω → E
inst_3 : NormedSpace ℝ E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
hX : HasGaussianLaw X P
L : E ≃L[ℝ] F
⊢ HasGaussianLaw.{u_1, u_3} (E := F) ((⇑L : (a : E) → F) ∘ X) P

Tactic:
hX.map L.toContinuousLinearMap

Premises used: ProbabilityTheory.HasGaussianLaw.map, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
Goal:
Ω : Type u_1
E : Type u_2
F : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
X : Ω → E
inst_3 : NormedSpace ℝ E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
hX : HasGaussianLaw X P
L : E ≃L[ℝ] F
⊢ HasGaussianLaw.{u_1, u_3} (E := F) (fun (ω : Ω) ↦ (L : (a : E) → F) (X ω)) P

Tactic:
hX.map_equiv L

Premises used: ProbabilityTheory.HasGaussianLaw.map_equiv
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
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
c : ℝ
hX : HasGaussianLaw X P
⊢ HasGaussianLaw (c • X) P

Tactic:
hX.map (.lsmul ℝ ℝ c)

Premises used: Real, ProbabilityTheory.HasGaussianLaw.map, ContinuousLinearMap.lsmul, DFunLike.coe
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
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
c : ℝ
hX : HasGaussianLaw X P
⊢ HasGaussianLaw.{u_1, u_2} (E := E) (fun (ω : Ω) ↦ c • X ω) P

Tactic:
hX.smul c

Premises used: ProbabilityTheory.HasGaussianLaw.smul
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
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
hX : HasGaussianLaw X P
⊢ HasGaussianLaw (-X) P

Tactic:
simpa using hX.smul (-1)

Premises used: ProbabilityTheory.HasGaussianLaw.smul, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
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
hX : HasGaussianLaw X P
⊢ HasGaussianLaw.{u_1, u_2} (E := E) (fun (ω : Ω) ↦ -X ω) P

Tactic:
hX.neg

Premises used: ProbabilityTheory.HasGaussianLaw.neg