awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
inst_4 : CompleteSpace E
S : Type u_4
X : S → Ω → E
Y : T → Ω → E
inst_5 : NormedSpace ℝ E
hXY : IsGaussianProcess (Sum.elim X Y) P
mX : ∀ (s : S), AEMeasurable (X s) P
mY : ∀ (t : T), AEMeasurable (Y t) P
h : ∀ (s : S) (t : T) (L₁ L₂ : StrongDual ℝ E), cov[(⇑L₁ : (a : E) → ℝ) ∘ X s, (⇑L₂ : (a : E) → ℝ) ∘ Y t; P] = 0
this : IsProbabilityMeasure P
I : Finset S
J : Finset T
L₁ : StrongDual ℝ ((i : ↥I) → E)
L₂ : StrongDual ℝ ((j : ↥J) → E)
h1 :
  Eq.{u_2 + 1} (α := Ω → ℝ)
    (Function.comp (β := (i : ↥I) → E) (⇑L₁ : (a : (i : ↥I) → E) → ℝ) fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω)
    (∑ i : ↥I,
      (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₁
              (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (i : ↥I) ↦ E) i)) :
          (a : E) → ℝ) ∘
        X (↑i : S))
h2 :
  Eq.{u_2 + 1} (α := Ω → ℝ)
    (Function.comp (β := (j : ↥J) → E) (⇑L₂ : (a : (j : ↥J) → E) → ℝ) fun (ω : Ω) (j : ↥J) ↦ Y (↑j : T) ω)
    (∑ j : ↥J,
      (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₂
              (ContinuousLinearMap.single.{0, u_1, u_3} ℝ (fun (j : ↥J) ↦ E) j)) :
          (a : E) → ℝ) ∘
        Y (↑j : T))
refine_2 :
  Eq (α := ℝ)
    (∑ i : ↥I,
      ∑ j : ↥J,
        cov[(⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₁
                  (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (i : ↥I) ↦ E) i)) :
              (a : E) → ℝ) ∘
            X (↑i : S),
          (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₂
                  (ContinuousLinearMap.single.{0, u_1, u_3} ℝ (fun (j : ↥J) ↦ E) j)) :
              (a : E) → ℝ) ∘
            Y (↑j : T);
          P])
    0
refine_2₁ :
  ∀ (i : ↥I),
    MemLp (ε := ℝ)
      ((⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₁
              (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (i : ↥I) ↦ E) i)) :
          (a : E) → ℝ) ∘
        X (↑i : S))
      2 P
refine_2₂ :
  ∀ (i : ↥J),
    MemLp (ε := ℝ)
      ((⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₂
              (ContinuousLinearMap.single.{0, u_1, u_3} ℝ (fun (j : ↥J) ↦ E) i)) :
          (a : E) → ℝ) ∘
        Y (↑i : T))
      2 P
⊢ cov[Function.comp (β := (i : ↥I) → E) (⇑L₁ : (a : (i : ↥I) → E) → ℝ) fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω,
      Function.comp (β := (j : ↥J) → E) (⇑L₂ : (a : (j : ↥J) → E) → ℝ) fun (ω : Ω) (j : ↥J) ↦ Y (↑j : T) ω; P] =
    0

Tactic:
rw [h1, h2, covariance_sum_sum]

Premises used: ProbabilityTheory.covariance_sum_sum
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
inst_4 : CompleteSpace E
S : Type u_4
X : S → Ω → E
Y : T → Ω → E
inst_5 : NormedSpace ℝ E
hXY : IsGaussianProcess (Sum.elim X Y) P
mX : ∀ (s : S), AEMeasurable (X s) P
mY : ∀ (t : T), AEMeasurable (Y t) P
h : ∀ (s : S) (t : T) (L₁ L₂ : StrongDual ℝ E), cov[(⇑L₁ : (a : E) → ℝ) ∘ X s, (⇑L₂ : (a : E) → ℝ) ∘ Y t; P] = 0
this : IsProbabilityMeasure P
I : Finset S
J : Finset T
L₁ : StrongDual ℝ ((i : ↥I) → E)
L₂ : StrongDual ℝ ((j : ↥J) → E)
h1 :
  Eq.{u_2 + 1} (α := Ω → ℝ)
    (Function.comp (β := (i : ↥I) → E) (⇑L₁ : (a : (i : ↥I) → E) → ℝ) fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω)
    (∑ i : ↥I,
      (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₁
              (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (i : ↥I) ↦ E) i)) :
          (a : E) → ℝ) ∘
        X (↑i : S))
h2 :
  Eq.{u_2 + 1} (α := Ω → ℝ)
    (Function.comp (β := (j : ↥J) → E) (⇑L₂ : (a : (j : ↥J) → E) → ℝ) fun (ω : Ω) (j : ↥J) ↦ Y (↑j : T) ω)
    (∑ j : ↥J,
      (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₂
              (ContinuousLinearMap.single.{0, u_1, u_3} ℝ (fun (j : ↥J) ↦ E) j)) :
          (a : E) → ℝ) ∘
        Y (↑j : T))
⊢ Eq (α := ℝ)
    (∑ i : ↥I,
      ∑ j : ↥J,
        cov[(⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₁
                  (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (i : ↥I) ↦ E) i)) :
              (a : E) → ℝ) ∘
            X (↑i : S),
          (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₂
                  (ContinuousLinearMap.single.{0, u_1, u_3} ℝ (fun (j : ↥J) ↦ E) j)) :
              (a : E) → ℝ) ∘
            Y (↑j : T);
          P])
    0

Tactic:
sum_eq_zero fun i _ ↦ sum_eq_zero fun j _ ↦ h ..

Premises used: ContinuousLinearMap.comp, ContinuousLinearMap.single, Real, Finset.sum_eq_zero, Subtype.val
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
inst_4 : CompleteSpace E
S : Type u_4
X : S → Ω → E
Y : T → Ω → E
inst_5 : NormedSpace ℝ E
hXY : IsGaussianProcess (Sum.elim X Y) P
mX : ∀ (s : S), AEMeasurable (X s) P
mY : ∀ (t : T), AEMeasurable (Y t) P
h : ∀ (s : S) (t : T) (L₁ L₂ : StrongDual ℝ E), cov[(⇑L₁ : (a : E) → ℝ) ∘ X s, (⇑L₂ : (a : E) → ℝ) ∘ Y t; P] = 0
this : IsProbabilityMeasure P
I : Finset S
J : Finset T
L₁ : StrongDual ℝ ((i : ↥I) → E)
L₂ : StrongDual ℝ ((j : ↥J) → E)
h1 :
  Eq.{u_2 + 1} (α := Ω → ℝ)
    (Function.comp (β := (i : ↥I) → E) (⇑L₁ : (a : (i : ↥I) → E) → ℝ) fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω)
    (∑ i : ↥I,
      (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₁
              (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (i : ↥I) ↦ E) i)) :
          (a : E) → ℝ) ∘
        X (↑i : S))
h2 :
  Eq.{u_2 + 1} (α := Ω → ℝ)
    (Function.comp (β := (j : ↥J) → E) (⇑L₂ : (a : (j : ↥J) → E) → ℝ) fun (ω : Ω) (j : ↥J) ↦ Y (↑j : T) ω)
    (∑ j : ↥J,
      (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₂
              (ContinuousLinearMap.single.{0, u_1, u_3} ℝ (fun (j : ↥J) ↦ E) j)) :
          (a : E) → ℝ) ∘
        Y (↑j : T))
⊢ Eq (α := ℝ)
    (∑ i : ↥I,
      ∑ j : ↥J,
        cov[(⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₁
                  (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (i : ↥I) ↦ E) i)) :
              (a : E) → ℝ) ∘
            X (↑i : S),
          (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₂
                  (ContinuousLinearMap.single.{0, u_1, u_3} ℝ (fun (j : ↥J) ↦ E) j)) :
              (a : E) → ℝ) ∘
            Y (↑j : T);
          P])
    0

Tactic:
exact sum_eq_zero fun i _ ↦ sum_eq_zero fun j _ ↦ h ..

Premises used: Finset.sum_eq_zero
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
inst_4 : CompleteSpace E
S : Type u_4
X : S → Ω → E
Y : T → Ω → E
inst_5 : NormedSpace ℝ E
hXY : IsGaussianProcess (Sum.elim X Y) P
mX : ∀ (s : S), AEMeasurable (X s) P
mY : ∀ (t : T), AEMeasurable (Y t) P
h : ∀ (s : S) (t : T) (L₁ L₂ : StrongDual ℝ E), cov[(⇑L₁ : (a : E) → ℝ) ∘ X s, (⇑L₂ : (a : E) → ℝ) ∘ Y t; P] = 0
this : IsProbabilityMeasure P
I : Finset S
J : Finset T
L₁ : StrongDual ℝ ((i : ↥I) → E)
L₂ : StrongDual ℝ ((j : ↥J) → E)
h1 :
  Eq.{u_2 + 1} (α := Ω → ℝ)
    (Function.comp (β := (i : ↥I) → E) (⇑L₁ : (a : (i : ↥I) → E) → ℝ) fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω)
    (∑ i : ↥I,
      (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₁
              (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (i : ↥I) ↦ E) i)) :
          (a : E) → ℝ) ∘
        X (↑i : S))
h2 :
  Eq.{u_2 + 1} (α := Ω → ℝ)
    (Function.comp (β := (j : ↥J) → E) (⇑L₂ : (a : (j : ↥J) → E) → ℝ) fun (ω : Ω) (j : ↥J) ↦ Y (↑j : T) ω)
    (∑ j : ↥J,
      (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₂
              (ContinuousLinearMap.single.{0, u_1, u_3} ℝ (fun (j : ↥J) ↦ E) j)) :
          (a : E) → ℝ) ∘
        Y (↑j : T))
⊢ ∀ (i : ↥I),
    MemLp (ε := ℝ)
      ((⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₁
              (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (i : ↥I) ↦ E) i)) :
          (a : E) → ℝ) ∘
        X (↑i : S))
      2 P

Tactic:
fun s ↦ ((hXY.hasGaussianLaw_eval (.inl s)).map _).memLp_two

Premises used: ContinuousLinearMap.comp, ContinuousLinearMap.single, Real, Sum.inl, ProbabilityTheory.HasGaussianLaw.map, ProbabilityTheory.IsGaussianProcess.hasGaussianLaw_eval, Subtype.val, ProbabilityTheory.HasGaussianLaw.memLp_two, Sum.elim
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
inst_4 : CompleteSpace E
S : Type u_4
X : S → Ω → E
Y : T → Ω → E
inst_5 : NormedSpace ℝ E
hXY : IsGaussianProcess (Sum.elim X Y) P
mX : ∀ (s : S), AEMeasurable (X s) P
mY : ∀ (t : T), AEMeasurable (Y t) P
h : ∀ (s : S) (t : T) (L₁ L₂ : StrongDual ℝ E), cov[(⇑L₁ : (a : E) → ℝ) ∘ X s, (⇑L₂ : (a : E) → ℝ) ∘ Y t; P] = 0
this : IsProbabilityMeasure P
I : Finset S
J : Finset T
L₁ : StrongDual ℝ ((i : ↥I) → E)
L₂ : StrongDual ℝ ((j : ↥J) → E)
h1 :
  Eq.{u_2 + 1} (α := Ω → ℝ)
    (Function.comp (β := (i : ↥I) → E) (⇑L₁ : (a : (i : ↥I) → E) → ℝ) fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω)
    (∑ i : ↥I,
      (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₁
              (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (i : ↥I) ↦ E) i)) :
          (a : E) → ℝ) ∘
        X (↑i : S))
h2 :
  Eq.{u_2 + 1} (α := Ω → ℝ)
    (Function.comp (β := (j : ↥J) → E) (⇑L₂ : (a : (j : ↥J) → E) → ℝ) fun (ω : Ω) (j : ↥J) ↦ Y (↑j : T) ω)
    (∑ j : ↥J,
      (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₂
              (ContinuousLinearMap.single.{0, u_1, u_3} ℝ (fun (j : ↥J) ↦ E) j)) :
          (a : E) → ℝ) ∘
        Y (↑j : T))
⊢ ∀ (i : ↥I),
    MemLp (ε := ℝ)
      ((⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₁
              (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (i : ↥I) ↦ E) i)) :
          (a : E) → ℝ) ∘
        X (↑i : S))
      2 P

Tactic:
exact fun s ↦ ((hXY.hasGaussianLaw_eval (.inl s)).map _).memLp_two

Premises used: Sum.inl, ProbabilityTheory.HasGaussianLaw.map, ProbabilityTheory.IsGaussianProcess.hasGaussianLaw_eval, ProbabilityTheory.HasGaussianLaw.memLp_two
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
inst_4 : CompleteSpace E
S : Type u_4
X : S → Ω → E
Y : T → Ω → E
inst_5 : NormedSpace ℝ E
hXY : IsGaussianProcess (Sum.elim X Y) P
mX : ∀ (s : S), AEMeasurable (X s) P
mY : ∀ (t : T), AEMeasurable (Y t) P
h : ∀ (s : S) (t : T) (L₁ L₂ : StrongDual ℝ E), cov[(⇑L₁ : (a : E) → ℝ) ∘ X s, (⇑L₂ : (a : E) → ℝ) ∘ Y t; P] = 0
this : IsProbabilityMeasure P
I : Finset S
J : Finset T
L₁ : StrongDual ℝ ((i : ↥I) → E)
L₂ : StrongDual ℝ ((j : ↥J) → E)
h1 :
  Eq.{u_2 + 1} (α := Ω → ℝ)
    (Function.comp (β := (i : ↥I) → E) (⇑L₁ : (a : (i : ↥I) → E) → ℝ) fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω)
    (∑ i : ↥I,
      (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₁
              (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (i : ↥I) ↦ E) i)) :
          (a : E) → ℝ) ∘
        X (↑i : S))
h2 :
  Eq.{u_2 + 1} (α := Ω → ℝ)
    (Function.comp (β := (j : ↥J) → E) (⇑L₂ : (a : (j : ↥J) → E) → ℝ) fun (ω : Ω) (j : ↥J) ↦ Y (↑j : T) ω)
    (∑ j : ↥J,
      (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₂
              (ContinuousLinearMap.single.{0, u_1, u_3} ℝ (fun (j : ↥J) ↦ E) j)) :
          (a : E) → ℝ) ∘
        Y (↑j : T))
⊢ ∀ (i : ↥J),
    MemLp (ε := ℝ)
      ((⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₂
              (ContinuousLinearMap.single.{0, u_1, u_3} ℝ (fun (j : ↥J) ↦ E) i)) :
          (a : E) → ℝ) ∘
        Y (↑i : T))
      2 P

Tactic:
fun t ↦ ((hXY.hasGaussianLaw_eval (.inr t)).map _).memLp_two

Premises used: ContinuousLinearMap.comp, ContinuousLinearMap.single, Real, ProbabilityTheory.HasGaussianLaw.map, ProbabilityTheory.IsGaussianProcess.hasGaussianLaw_eval, Sum.inr, Subtype.val, ProbabilityTheory.HasGaussianLaw.memLp_two, Sum.elim
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
inst_4 : CompleteSpace E
S : Type u_4
X : S → Ω → E
Y : T → Ω → E
inst_5 : NormedSpace ℝ E
hXY : IsGaussianProcess (Sum.elim X Y) P
mX : ∀ (s : S), AEMeasurable (X s) P
mY : ∀ (t : T), AEMeasurable (Y t) P
h : ∀ (s : S) (t : T) (L₁ L₂ : StrongDual ℝ E), cov[(⇑L₁ : (a : E) → ℝ) ∘ X s, (⇑L₂ : (a : E) → ℝ) ∘ Y t; P] = 0
this : IsProbabilityMeasure P
I : Finset S
J : Finset T
L₁ : StrongDual ℝ ((i : ↥I) → E)
L₂ : StrongDual ℝ ((j : ↥J) → E)
h1 :
  Eq.{u_2 + 1} (α := Ω → ℝ)
    (Function.comp (β := (i : ↥I) → E) (⇑L₁ : (a : (i : ↥I) → E) → ℝ) fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω)
    (∑ i : ↥I,
      (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₁
              (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (i : ↥I) ↦ E) i)) :
          (a : E) → ℝ) ∘
        X (↑i : S))
h2 :
  Eq.{u_2 + 1} (α := Ω → ℝ)
    (Function.comp (β := (j : ↥J) → E) (⇑L₂ : (a : (j : ↥J) → E) → ℝ) fun (ω : Ω) (j : ↥J) ↦ Y (↑j : T) ω)
    (∑ j : ↥J,
      (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₂
              (ContinuousLinearMap.single.{0, u_1, u_3} ℝ (fun (j : ↥J) ↦ E) j)) :
          (a : E) → ℝ) ∘
        Y (↑j : T))
⊢ ∀ (i : ↥J),
    MemLp (ε := ℝ)
      ((⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₂
              (ContinuousLinearMap.single.{0, u_1, u_3} ℝ (fun (j : ↥J) ↦ E) i)) :
          (a : E) → ℝ) ∘
        Y (↑i : T))
      2 P

Tactic:
exact fun t ↦ ((hXY.hasGaussianLaw_eval (.inr t)).map _).memLp_two

Premises used: ProbabilityTheory.HasGaussianLaw.map, ProbabilityTheory.IsGaussianProcess.hasGaussianLaw_eval, Sum.inr, ProbabilityTheory.HasGaussianLaw.memLp_two
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence
Goal:
T : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
S : Type u_4
X : S → Ω → ℝ
Y : T → Ω → ℝ
hXY : IsGaussianProcess (Sum.elim X Y) P
mX : ∀ (s : S), AEMeasurable (X s) P
mY : ∀ (t : T), AEMeasurable (Y t) P
h : ∀ (s : S) (t : T), cov[X s, Y t; P] = 0
x : S
x_1 : T
x_2 x_3 : ℝ
⊢ cov[fun (ω : Ω) ↦ ⟪x_2, X x ω⟫, fun (ω : Ω) ↦ ⟪x_3, Y x_1 ω⟫; P] = 0

Tactic:
simp [covariance_mul_const_left, covariance_mul_const_right, h]

Premises used: ProbabilityTheory.covariance_mul_const_left, ProbabilityTheory.covariance_mul_const_right
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
ι : Type u_1
inst : Fintype ι
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
⊢ Measurable.{0, u_2} (β := E) fun (x : (i : Fin (finrank ℝ E)) → ℝ) ↦
    ∑ i : Fin (finrank ℝ E), HSMul.hSMul (β := E) (x i) ((stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) i : E)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
⊢ AEStronglyMeasurable (β := E) (m₀ := inst_3) (fun (x : E) ↦ x)
    (Measure.map
      (fun (x : (i : Fin (finrank ℝ E)) → ℝ) ↦
        ∑ i : Fin (finrank ℝ E),
          HSMul.hSMul (β := E) (x i) ((stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) i : E))
      (Measure.pi (α := fun (x : Fin (finrank ℝ E)) ↦ ℝ) fun (x : Fin (finrank ℝ E)) ↦ gaussianReal 0 1))

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
rw :
  Eq.{u_2 + 1} (α := E)
    (∑ i : Fin (finrank ℝ E),
      @integral _ _ _ _ (MeasurableSpace.pi (X := fun (x : Fin (finrank ℝ E)) ↦ ℝ))
        (Measure.pi (α := fun (x : Fin (finrank ℝ E)) ↦ ℝ) fun (x : Fin (finrank ℝ E)) ↦ gaussianReal 0 1)
        fun (a : (i : Fin (finrank ℝ E)) → ℝ) ↦
        HSMul.hSMul (β := E) (a i) ((stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) i : E))
    0
hf :
  ∀ (i : Fin (finrank ℝ E)),
    Membership.mem (γ := Finset (Fin (finrank ℝ E))) Finset.univ i →
      @Integrable.{u_2, 0} E _ _ _ (MeasurableSpace.pi (X := fun (x : Fin (finrank ℝ E)) ↦ ℝ))
        (fun (x : (i : Fin (finrank ℝ E)) → ℝ) ↦
          HSMul.hSMul (β := E) (x i) ((stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) i : E))
        (Measure.pi (α := fun (x : Fin (finrank ℝ E)) ↦ ℝ) fun (x : Fin (finrank ℝ E)) ↦ gaussianReal 0 1)
rw₁ :
  AEMeasurable.{0, u_2} (β := E) (_m := MeasurableSpace.pi (X := fun (x : Fin (finrank ℝ E)) ↦ ℝ))
    (fun (x : (i : Fin (finrank ℝ E)) → ℝ) ↦
      ∑ i : Fin (finrank ℝ E),
        HSMul.hSMul (β := E) (x i) ((stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) i : E))
    (Measure.pi (α := fun (x : Fin (finrank ℝ E)) ↦ ℝ) fun (x : Fin (finrank ℝ E)) ↦ gaussianReal 0 1)
⊢ Eq (α := E) (@integral _ _ _ _ inst_3 (stdGaussian E) fun (x : E) ↦ x) 0

Tactic:
rw [stdGaussian, integral_map _ (by fun_prop), integral_finsetSum]

Premises used: MeasureTheory.integral_map, MeasureTheory.integral_finsetSum, ProbabilityTheory.stdGaussian
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
⊢ Eq.{u_2 + 1} (α := E)
    (∑ i : Fin (finrank ℝ E),
      @integral _ _ _ _ (MeasurableSpace.pi (X := fun (x : Fin (finrank ℝ E)) ↦ ℝ))
        (Measure.pi (α := fun (x : Fin (finrank ℝ E)) ↦ ℝ) fun (x : Fin (finrank ℝ E)) ↦ gaussianReal 0 1)
        fun (a : (i : Fin (finrank ℝ E)) → ℝ) ↦
        HSMul.hSMul (β := E) (a i) ((stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) i : E))
    0

Tactic:
simp [integral_smul_const, integral_eval]

Premises used: integral_smul_const, MeasureTheory.integral_eval
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
⊢ ∀ (i : Fin (finrank ℝ E)),
    Membership.mem (γ := Finset (Fin (finrank ℝ E))) Finset.univ i →
      @Integrable.{u_2, 0} E _ _ _ (MeasurableSpace.pi (X := fun (x : Fin (finrank ℝ E)) ↦ ℝ))
        (fun (x : (i : Fin (finrank ℝ E)) → ℝ) ↦
          HSMul.hSMul (β := E) (x i) ((stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) i : E))
        (Measure.pi (α := fun (x : Fin (finrank ℝ E)) ↦ ℝ) fun (x : Fin (finrank ℝ E)) ↦ gaussianReal 0 1)

Tactic:
fun i _ ↦ Integrable.smul_const (integrable_eval IsGaussian.integrable_id) _

Premises used: Real, MeasureTheory.Integrable.smul_const, DFunLike.coe, stdOrthonormalBasis
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
⊢ ∀ (i : Fin (finrank ℝ E)),
    Membership.mem (γ := Finset (Fin (finrank ℝ E))) Finset.univ i →
      @Integrable.{u_2, 0} E _ _ _ (MeasurableSpace.pi (X := fun (x : Fin (finrank ℝ E)) ↦ ℝ))
        (fun (x : (i : Fin (finrank ℝ E)) → ℝ) ↦
          HSMul.hSMul (β := E) (x i) ((stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) i : E))
        (Measure.pi (α := fun (x : Fin (finrank ℝ E)) ↦ ℝ) fun (x : Fin (finrank ℝ E)) ↦ gaussianReal 0 1)

Tactic:
exact fun i _ ↦ Integrable.smul_const (integrable_eval IsGaussian.integrable_id) _

Premises used: MeasureTheory.Integrable.smul_const
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
⊢ ∀ (i : Fin (finrank ℝ E)),
    Membership.mem (γ := Finset (Fin (finrank ℝ E))) Finset.univ i →
      Measurable.{0, u_2} (β := E) fun (x : (i : Fin (finrank ℝ E)) → ℝ) ↦
        HSMul.hSMul (β := E) (x i) ((stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) i : E)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
⊢ AEMeasurable.{0, u_2} (β := E) (_m := MeasurableSpace.pi (X := fun (x : Fin (finrank ℝ E)) ↦ ℝ))
    (fun (x : (i : Fin (finrank ℝ E)) → ℝ) ↦
      ∑ i : Fin (finrank ℝ E),
        HSMul.hSMul (β := E) (x i) ((stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) i : E))
    (Measure.pi (α := fun (x : Fin (finrank ℝ E)) ↦ ℝ) fun (x : Fin (finrank ℝ E)) ↦ gaussianReal 0 1)

Tactic:
exact (Finset.measurable_sum _ (by fun_prop)).aemeasurable

Premises used: Measurable.aemeasurable, Finset.measurable_sum
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
L : StrongDual ℝ E
⊢ Measurable.{0, u_2} (β := E) fun (x : (i : Fin (finrank ℝ E)) → ℝ) ↦
    ∑ i : Fin (finrank ℝ E), HSMul.hSMul (β := E) (x i) ((stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) i : E)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
L : StrongDual ℝ E
rw :
  variance (Ω := (i : Fin (finrank ℝ E)) → ℝ) (mΩ := MeasurableSpace.pi (X := fun (x : Fin (finrank ℝ E)) ↦ ℝ))
      (Function.comp (β := E) (⇑L : (a : E) → ℝ) fun (x : (i : Fin (finrank ℝ E)) → ℝ) ↦
        ∑ i : Fin (finrank ℝ E),
          HSMul.hSMul (β := E) (x i) ((stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) i : E))
      (Measure.pi (α := fun (x : Fin (finrank ℝ E)) ↦ ℝ) fun (x : Fin (finrank ℝ E)) ↦ gaussianReal 0 1) =
    HPow.hPow (β := ℕ) ‖L‖ 2
⊢ variance (mΩ := inst_3) (⇑L : (a : E) → ℝ) (stdGaussian E) = HPow.hPow (β := ℕ) ‖L‖ 2

Tactic:
rw [stdGaussian, variance_map L.continuous.aemeasurable (Measurable.aemeasurable (by fun_prop))]

Premises used: Measurable.aemeasurable, ContinuousLinearMap.continuous, Continuous.aemeasurable, ProbabilityTheory.variance_map, ProbabilityTheory.stdGaussian
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
L : StrongDual ℝ E
h :
  ∀ (x : Fin (finrank ℝ E) → ℝ),
    Eq (α := ℝ)
      (Function.comp (β := E) (⇑L : (a : E) → ℝ)
        (fun (x : Fin (finrank ℝ E) → ℝ) ↦
          ∑ i : Fin (finrank ℝ E),
            HSMul.hSMul (β := E) (x i) ((stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) i : E))
        x)
      ((∑ i : Fin (finrank ℝ E), fun (x : Fin (finrank ℝ E) → ℝ) ↦
          HMul.hMul (α := ℝ) ((L : (a : E) → ℝ) ((stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) i : E) : ℝ)
            (x i))
        x)
⊢ Eq (α := (Fin (finrank ℝ E) → ℝ) → ℝ)
    (Function.comp (β := E) (⇑L : (a : E) → ℝ) fun (x : Fin (finrank ℝ E) → ℝ) ↦
      ∑ i : Fin (finrank ℝ E),
        HSMul.hSMul (β := E) (x i) ((stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) i : E))
    (∑ i : Fin (finrank ℝ E), fun (x : Fin (finrank ℝ E) → ℝ) ↦
      HMul.hMul (α := ℝ) ((L : (a : E) → ℝ) ((stdOrthonormalBasis ℝ E : (a : Fin (finrank ℝ E)) → E) i : E) : ℝ) (x i))

Tactic:
ext x