awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
X Y : Ω → E
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
h : X ⟂ᵢ[P] Y - X
this : IsProbabilityMeasure P
L : StrongDual ℝ E
ha : charFunDual (mE := inst_2) (Measure.map X P) L ≠ 0
h₁ :
  charFunDual (mE := inst_2) (Measure.map X P) L * charFunDual (mE := inst_2) (Measure.map (Y - X) P) L =
    charFunDual (mE := inst_2) (Measure.map X P) L *
      cexp
        ((↑(∫ (x : Ω), ((⇑L : (a : E) → ℝ) ∘ (Y - X)) x ∂P) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ) ∘ (Y - X); P] : ℂ) / 2)
⊢ charFunDual (mE := inst_2) (Measure.map (Y - X) P) L =
    cexp ((↑(∫ (x : Ω), ((⇑L : (a : E) → ℝ) ∘ (Y - X)) x ∂P) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ) ∘ (Y - X); P] : ℂ) / 2)

Tactic:
apply mul_left_cancel₀ (a := charFunDual (P.map X) L)

Premises used: mul_left_cancel₀
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
X Y : Ω → E
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
h : X ⟂ᵢ[P] Y - X
this : IsProbabilityMeasure P
L : StrongDual ℝ E
⊢ charFunDual (mE := inst_2) (Measure.map X P) L ≠ 0

Tactic:
simp [hX.charFunDual_map_eq]

Premises used: ProbabilityTheory.HasGaussianLaw.charFunDual_map_eq
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
X Y : Ω → E
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
h : X ⟂ᵢ[P] Y - X
this : IsProbabilityMeasure P
L : StrongDual ℝ E
h₁ :
  cexp ((↑(∫ (x : Ω), ((⇑L : (a : E) → ℝ) ∘ Y) x ∂P) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ) ∘ Y; P] : ℂ) / 2) =
    cexp
      ((↑(∫ (a : Ω), HAdd.hAdd (α := ℝ) (((⇑L : (a : E) → ℝ) ∘ X) a) (((⇑L : (a : E) → ℝ) ∘ (Y - X)) a) ∂P) : ℂ) * I -
        (↑Var[HAdd.hAdd (α := Ω → ℝ) ((⇑L : (a : E) → ℝ) ∘ X) ((⇑L : (a : E) → ℝ) ∘ (Y - X)); P] : ℂ) / 2)
h₂ : MemLp (ε := ℝ) ((⇑L : (a : E) → ℝ) ∘ X) 2 P
h₃ : MemLp (ε := ℝ) ((⇑L : (a : E) → ℝ) ∘ (Y - X)) 2 P
h₄ : ((⇑L : (a : E) → ℝ) ∘ X) ⟂ᵢ[P] (⇑L : (a : E) → ℝ) ∘ (Y - X)
h₅ : Integrable (ε := ℝ) ((⇑L : (a : E) → ℝ) ∘ X) P
h₆ : Integrable (ε := ℝ) ((⇑L : (a : E) → ℝ) ∘ (Y - X)) P
h₇ : AEMeasurable X P
h₈ : AEMeasurable (Y - X) P
⊢ charFunDual (mE := inst_2) (Measure.map X P) L * charFunDual (mE := inst_2) (Measure.map (Y - X) P) L =
    charFunDual (mE := inst_2) (Measure.map X P) L *
      cexp
        ((↑(∫ (x : Ω), ((⇑L : (a : E) → ℝ) ∘ (Y - X)) x ∂P) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ) ∘ (Y - X); P] : ℂ) / 2)

Tactic:
rw [← Pi.mul_apply, ← h.charFunDual_map_add_eq_mul, add_sub_cancel, hX.charFunDual_map_eq,
    ← exp_add, sub_add_sub_comm, ← add_mul, ← ofReal_add, ← integral_add, ← add_div, ← ofReal_add,
    ← IndepFun.variance_add, hY.charFunDual_map_eq]

Premises used: add_mul, Pi.mul_apply, Complex.exp_add, Complex.ofReal_add, sub_add_sub_comm, ProbabilityTheory.IndepFun.charFunDual_map_add_eq_mul, add_sub_cancel, ProbabilityTheory.IndepFun.variance_add, ProbabilityTheory.HasGaussianLaw.charFunDual_map_eq, MeasureTheory.integral_add, add_div
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
X Y : Ω → E
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
h : X ⟂ᵢ[P] Y - X
this : IsProbabilityMeasure P
L : StrongDual ℝ E
h₁ :
  ∀ (ω : Ω),
    ((⇑L : (a : E) → ℝ) ∘ Y) ω = HAdd.hAdd (α := ℝ) (((⇑L : (a : E) → ℝ) ∘ X) ω) (((⇑L : (a : E) → ℝ) ∘ (Y - X)) ω)
h₂ :
  ∀ (ω : Ω),
    ((⇑L : (a : E) → ℝ) ∘ Y) ω =
      HAdd.hAdd (α := Ω → ℝ) (β := Ω → ℝ) ((⇑L : (a : E) → ℝ) ∘ X) ((⇑L : (a : E) → ℝ) ∘ (Y - X)) ω
⊢ cexp ((↑(∫ (x : Ω), ((⇑L : (a : E) → ℝ) ∘ Y) x ∂P) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ) ∘ Y; P] : ℂ) / 2) =
    cexp
      ((↑(∫ (a : Ω), HAdd.hAdd (α := ℝ) (((⇑L : (a : E) → ℝ) ∘ X) a) (((⇑L : (a : E) → ℝ) ∘ (Y - X)) a) ∂P) : ℂ) * I -
        (↑Var[HAdd.hAdd (α := Ω → ℝ) ((⇑L : (a : E) → ℝ) ∘ X) ((⇑L : (a : E) → ℝ) ∘ (Y - X)); P] : ℂ) / 2)

Tactic:
congr with ω
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
X Y : Ω → E
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
h : X ⟂ᵢ[P] Y - X
this : IsProbabilityMeasure P
L : StrongDual ℝ E
ω : Ω
⊢ ((⇑L : (a : E) → ℝ) ∘ Y) ω = HAdd.hAdd (α := ℝ) (((⇑L : (a : E) → ℝ) ∘ X) ω) (((⇑L : (a : E) → ℝ) ∘ (Y - X)) ω)

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
X Y : Ω → E
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
h : X ⟂ᵢ[P] Y - X
this : IsProbabilityMeasure P
L : StrongDual ℝ E
ω : Ω
⊢ ((⇑L : (a : E) → ℝ) ∘ Y) ω =
    HAdd.hAdd (α := Ω → ℝ) (β := Ω → ℝ) ((⇑L : (a : E) → ℝ) ∘ X) ((⇑L : (a : E) → ℝ) ∘ (Y - X)) ω

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
X Y : Ω → E
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
h : X ⟂ᵢ[P] Y - X
this : IsProbabilityMeasure P
L : StrongDual ℝ E
funProp : AEFinStronglyMeasurable.{u_1, u_2} (β := E) (fun (a : Ω) ↦ X a) P
⊢ AEMeasurable X P

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
X Y : Ω → E
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
h : X ⟂ᵢ[P] Y - X
this : IsProbabilityMeasure P
L : StrongDual ℝ E
funProp : AEFinStronglyMeasurable.{u_1, u_2} (β := E) (fun (a : Ω) ↦ Y a) P
funProp₁ : AEFinStronglyMeasurable.{u_1, u_2} (β := E) (fun (a : Ω) ↦ X a) P
⊢ AEMeasurable (Y - X) P

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
X Y : Ω → E
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
h : X ⟂ᵢ[P] Y - X
this : IsProbabilityMeasure P
L : StrongDual ℝ E
⊢ MemLp (ε := ℝ) ((⇑L : (a : E) → ℝ) ∘ X) 2 P

Tactic:
(hX.map L).memLp_two

Premises used: ProbabilityTheory.HasGaussianLaw.map, ProbabilityTheory.HasGaussianLaw.memLp_two
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
X Y : Ω → E
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
h : X ⟂ᵢ[P] Y - X
this : IsProbabilityMeasure P
L : StrongDual ℝ E
⊢ MemLp (ε := ℝ) ((⇑L : (a : E) → ℝ) ∘ X) 2 P

Tactic:
exact (hX.map L).memLp_two

Premises used: ProbabilityTheory.HasGaussianLaw.map, ProbabilityTheory.HasGaussianLaw.memLp_two
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
X Y : Ω → E
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
h : X ⟂ᵢ[P] Y - X
this : IsProbabilityMeasure P
L : StrongDual ℝ E
h₁ : MemLp (HSub.hSub (α := Ω → ℝ) ((⇑L : (a : E) → ℝ) ∘ Y) ((⇑L : (a : E) → ℝ) ∘ X)) 2 P
⊢ MemLp (ε := ℝ) ((⇑L : (a : E) → ℝ) ∘ (Y - X)) 2 P

Tactic:
rw [map_comp_sub]

Premises used: map_comp_sub
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
X Y : Ω → E
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
h : X ⟂ᵢ[P] Y - X
this : IsProbabilityMeasure P
L : StrongDual ℝ E
⊢ MemLp (HSub.hSub (α := Ω → ℝ) ((⇑L : (a : E) → ℝ) ∘ Y) ((⇑L : (a : E) → ℝ) ∘ X)) 2 P

Tactic:
(hY.map L).memLp_two.sub (hX.map L).memLp_two

Premises used: ProbabilityTheory.HasGaussianLaw.map, MeasureTheory.MemLp.sub, ProbabilityTheory.HasGaussianLaw.memLp_two
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
X Y : Ω → E
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
h : X ⟂ᵢ[P] Y - X
this : IsProbabilityMeasure P
L : StrongDual ℝ E
⊢ MemLp (HSub.hSub (α := Ω → ℝ) ((⇑L : (a : E) → ℝ) ∘ Y) ((⇑L : (a : E) → ℝ) ∘ X)) 2 P

Tactic:
exact (hY.map L).memLp_two.sub (hX.map L).memLp_two

Premises used: ProbabilityTheory.HasGaussianLaw.map, MeasureTheory.MemLp.sub, ProbabilityTheory.HasGaussianLaw.memLp_two
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
X Y : Ω → E
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
h : X ⟂ᵢ[P] Y - X
this : IsProbabilityMeasure P
L : StrongDual ℝ E
⊢ Measurable (α := E) (β := ℝ) (⇑L : (a : E) → ℝ)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
X Y : Ω → E
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
h : X ⟂ᵢ[P] Y - X
this : IsProbabilityMeasure P
L : StrongDual ℝ E
⊢ ((⇑L : (a : E) → ℝ) ∘ X) ⟂ᵢ[P] (⇑L : (a : E) → ℝ) ∘ (Y - X)

Tactic:
exact h.comp (by fun_prop) (by fun_prop)

Premises used: ProbabilityTheory.IndepFun.comp
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
X Y : Ω → E
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
h : X ⟂ᵢ[P] Y - X
this : IsProbabilityMeasure P
L : StrongDual ℝ E
⊢ Integrable (ε := ℝ) ((⇑L : (a : E) → ℝ) ∘ X) P

Tactic:
(hX.map L).integrable

Premises used: ProbabilityTheory.HasGaussianLaw.map, ProbabilityTheory.HasGaussianLaw.integrable
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
X Y : Ω → E
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
h : X ⟂ᵢ[P] Y - X
this : IsProbabilityMeasure P
L : StrongDual ℝ E
⊢ Integrable (ε := ℝ) ((⇑L : (a : E) → ℝ) ∘ X) P

Tactic:
exact (hX.map L).integrable

Premises used: ProbabilityTheory.HasGaussianLaw.map, ProbabilityTheory.HasGaussianLaw.integrable
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
X Y : Ω → E
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
h : X ⟂ᵢ[P] Y - X
this : IsProbabilityMeasure P
L : StrongDual ℝ E
h₁ : Integrable (HSub.hSub (α := Ω → ℝ) ((⇑L : (a : E) → ℝ) ∘ Y) ((⇑L : (a : E) → ℝ) ∘ X)) P
⊢ Integrable (ε := ℝ) ((⇑L : (a : E) → ℝ) ∘ (Y - X)) P

Tactic:
rw [map_comp_sub]

Premises used: map_comp_sub
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
X Y : Ω → E
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
h : X ⟂ᵢ[P] Y - X
this : IsProbabilityMeasure P
L : StrongDual ℝ E
⊢ Integrable (HSub.hSub (α := Ω → ℝ) ((⇑L : (a : E) → ℝ) ∘ Y) ((⇑L : (a : E) → ℝ) ∘ X)) P

Tactic:
(hY.map L).integrable.sub (hX.map L).integrable

Premises used: MeasureTheory.Integrable.sub, ProbabilityTheory.HasGaussianLaw.map, ProbabilityTheory.HasGaussianLaw.integrable
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
X Y : Ω → E
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
h : X ⟂ᵢ[P] Y - X
this : IsProbabilityMeasure P
L : StrongDual ℝ E
⊢ Integrable (HSub.hSub (α := Ω → ℝ) ((⇑L : (a : E) → ℝ) ∘ Y) ((⇑L : (a : E) → ℝ) ∘ X)) P

Tactic:
exact (hY.map L).integrable.sub (hX.map L).integrable

Premises used: MeasureTheory.Integrable.sub, ProbabilityTheory.HasGaussianLaw.map, ProbabilityTheory.HasGaussianLaw.integrable
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
Goal:
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : AddCommMonoid E
inst_3 : Module ℝ E
hX : IsGaussianProcess X P
⊢ IsProbabilityMeasure P

Tactic:
hX.hasGaussianLaw Classical.ofNonempty |>.isProbabilityMeasure

Premises used: Classical.ofNonempty, ProbabilityTheory.HasGaussianLaw.isProbabilityMeasure, ProbabilityTheory.IsGaussianProcess.hasGaussianLaw
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
Goal:
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : AddCommMonoid E
inst_3 : Module ℝ E
hX : IsGaussianProcess X P
t : T
⊢ Membership.mem (γ := Finset T) {t} t

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
Goal:
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : T → Ω → E
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : AddCommMonoid E
inst_3 : Module ℝ E
hX : IsGaussianProcess X P
hXY : ∀ (t : T), X t =ᶠ[ae P] Y t
I : Finset T
isGaussian_map :
  IsGaussian (E := (i : ↥I) → E) (mE := MeasurableSpace.pi (X := fun (i : ↥I) ↦ E))
    (Measure.map (fun (ω : Ω) ↦ I.restrict (π := fun (x : T) ↦ E) fun (x : T) ↦ Y x ω) P)
⊢ HasGaussianLaw (E := (i : ↥I) → E) (fun (ω : Ω) ↦ I.restrict (π := fun (x : T) ↦ E) fun (x : T) ↦ Y x ω) P

Tactic:
constructor
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
Goal:
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : T → Ω → E
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : AddCommMonoid E
inst_3 : Module ℝ E
hX : IsGaussianProcess X P
hXY : ∀ (t : T), X t =ᶠ[ae P] Y t
I : Finset T
isGaussian_map :
  IsGaussian (E := (i : ↥I) → E) (mE := MeasurableSpace.pi (X := fun (i : ↥I) ↦ E))
    (Measure.map (fun (ω : Ω) ↦ I.restrict (π := fun (t : T) ↦ E) fun (x : T) ↦ X x ω) P)
⊢ IsGaussian (E := (i : ↥I) → E) (mE := MeasurableSpace.pi (X := fun (i : ↥I) ↦ E))
    (Measure.map (fun (ω : Ω) ↦ I.restrict (π := fun (x : T) ↦ E) fun (x : T) ↦ Y x ω) P)

Tactic:
rw [map_restrict_eq_of_forall_ae_eq fun t ↦ (hXY t).symm]

Premises used: ProbabilityTheory.map_restrict_eq_of_forall_ae_eq, Filter.EventuallyEq.symm
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
Goal:
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : T → Ω → E
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : AddCommMonoid E
inst_3 : Module ℝ E
hX : IsGaussianProcess X P
hXY : ∀ (t : T), X t =ᶠ[ae P] Y t
I : Finset T
⊢ IsGaussian (E := (i : ↥I) → E) (mE := MeasurableSpace.pi (X := fun (i : ↥I) ↦ E))
    (Measure.map (fun (ω : Ω) ↦ I.restrict (π := fun (t : T) ↦ E) fun (x : T) ↦ X x ω) P)

Tactic:
(hX.hasGaussianLaw I).isGaussian_map

Premises used: ProbabilityTheory.IsGaussianProcess.hasGaussianLaw, ProbabilityTheory.HasGaussianLaw.isGaussian_map
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
Goal:
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : T → Ω → E
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : AddCommMonoid E
inst_3 : Module ℝ E
hX : IsGaussianProcess X P
hXY : ∀ (t : T), X t =ᶠ[ae P] Y t
I : Finset T
⊢ IsGaussian (E := (i : ↥I) → E) (mE := MeasurableSpace.pi (X := fun (i : ↥I) ↦ E))
    (Measure.map (fun (ω : Ω) ↦ I.restrict (π := fun (t : T) ↦ E) fun (x : T) ↦ X x ω) P)

Tactic:
exact (hX.hasGaussianLaw I).isGaussian_map

Premises used: ProbabilityTheory.IsGaussianProcess.hasGaussianLaw, ProbabilityTheory.HasGaussianLaw.isGaussian_map
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
Goal:
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedSpace ℝ E
hX : IsGaussianProcess X P
t : T
⊢ Membership.mem (γ := Finset T) {t} t

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
Goal:
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedSpace ℝ E
hX : IsGaussianProcess X P
t : T
⊢ HasGaussianLaw (X t) P

Tactic:
exact (hX.hasGaussianLaw {t}).map (.proj ⟨t, by simp⟩)

Premises used: ProbabilityTheory.IsGaussianProcess.hasGaussianLaw, ProbabilityTheory.HasGaussianLaw.map, ContinuousLinearMap.proj, Singleton.singleton
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
Goal:
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedSpace ℝ E
inst_4 : SecondCountableTopology E
hX : IsGaussianProcess X P
s t : T
⊢ Membership.mem (γ := Finset T) {s, t} s

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
Goal:
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedSpace ℝ E
inst_4 : SecondCountableTopology E
hX : IsGaussianProcess X P
s t : T
⊢ Membership.mem (γ := Finset T) {s, t} t

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
Goal:
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedSpace ℝ E
inst_4 : SecondCountableTopology E
hX : IsGaussianProcess X P
s t : T
⊢ HasGaussianLaw.{u_3, u_4} (E := E × E) (fun (ω : Ω) ↦ (X s ω, X t ω)) P

Tactic:
exact (hX.hasGaussianLaw {s, t}).prodMk ⟨s, by simp⟩ ⟨t, by simp⟩

Premises used: ProbabilityTheory.IsGaussianProcess.hasGaussianLaw, Insert.insert, Subtype.mk, ProbabilityTheory.HasGaussianLaw.prodMk, Singleton.singleton
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
Goal:
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedSpace ℝ E
inst_4 : SecondCountableTopology E
hX : IsGaussianProcess X P
s t : T
⊢ HasGaussianLaw.{u_3, u_4} (E := E × E) (fun (ω : Ω) ↦ (X s ω, X t ω)) P

Tactic:
classical
  exact (hX.hasGaussianLaw {s, t}).prodMk ⟨s, by simp⟩ ⟨t, by simp⟩
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
Goal:
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedSpace ℝ E
inst_4 : SecondCountableTopology E
hX : IsGaussianProcess X P
s t : T
⊢ HasGaussianLaw (X s + X t) P

Tactic:
hX.hasGaussianLaw_prodMk.add

Premises used: ProbabilityTheory.HasGaussianLaw.add, ProbabilityTheory.IsGaussianProcess.hasGaussianLaw_prodMk
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
Goal:
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedSpace ℝ E
inst_4 : SecondCountableTopology E
hX : IsGaussianProcess X P
s t : T
⊢ HasGaussianLaw.{u_3, u_4} (E := E) (fun (ω : Ω) ↦ X s ω + X t ω) P

Tactic:
hX.hasGaussianLaw_add

Premises used: ProbabilityTheory.IsGaussianProcess.hasGaussianLaw_add
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
Goal:
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedSpace ℝ E
inst_4 : SecondCountableTopology E
hX : IsGaussianProcess X P
s t : T
⊢ HasGaussianLaw (X s - X t) P

Tactic:
hX.hasGaussianLaw_prodMk.sub

Premises used: ProbabilityTheory.HasGaussianLaw.sub, ProbabilityTheory.IsGaussianProcess.hasGaussianLaw_prodMk
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
Goal:
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedSpace ℝ E
inst_4 : SecondCountableTopology E
hX : IsGaussianProcess X P
s t : T
⊢ HasGaussianLaw.{u_3, u_4} (E := E) (fun (ω : Ω) ↦ X s ω - X t ω) P

Tactic:
hX.hasGaussianLaw_sub

Premises used: ProbabilityTheory.IsGaussianProcess.hasGaussianLaw_sub
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
Goal:
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedSpace ℝ E
inst_4 : SecondCountableTopology E
hX : IsGaussianProcess X P
I : Finset T
⊢ HasGaussianLaw.{u_3, u_4} (E := E) (∑ i : ↥I, fun (ω : Ω) ↦ I.restrict (π := fun (x : T) ↦ E) (fun (x : T) ↦ X x ω) i)
    P

Tactic:
(hX.hasGaussianLaw I).sum

Premises used: ProbabilityTheory.IsGaussianProcess.hasGaussianLaw, ProbabilityTheory.HasGaussianLaw.sum
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
Goal:
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedSpace ℝ E
inst_4 : SecondCountableTopology E
hX : IsGaussianProcess X P
I : Finset T
h : Eq (α := Ω → E) (∑ i ∈ I, X i) (∑ i : ↥I, fun (ω : Ω) ↦ I.restrict (π := fun (x : T) ↦ E) (fun (x : T) ↦ X x ω) i)
⊢ HasGaussianLaw.{u_3, u_4} (E := E) (∑ i ∈ I, X i) P

Tactic:
convert! (hX.hasGaussianLaw I).sum

Premises used: ProbabilityTheory.IsGaussianProcess.hasGaussianLaw, ProbabilityTheory.HasGaussianLaw.sum