awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_4
κ : Type u_5
inst : Finite ι
inst_1 : Finite κ
X : ι → Ω → ℝ
Y : κ → Ω → ℝ
hXY :
  HasGaussianLaw (E := Prod.{u_4, u_5} ((i : ι) → ℝ) ((j : κ) → ℝ))
    (fun (ω : Ω) ↦ (fun (i : ι) ↦ X i ω, fun (j : κ) ↦ Y j ω)) P
h : ∀ (i : ι) (j : κ), cov[X i, Y j; P] = 0
this_1 : IsProbabilityMeasure P
hX :
  Eq (α := (ω : Ω) → (i : ι) → ℝ) (fun (ω : Ω) (i : ι) ↦ X i ω)
    (Function.comp (β := WithLp 2 ((i : ι) → ℝ)) ofLp (toLp 2 ∘ fun (ω : Ω) (i : ι) ↦ X i ω))
hY :
  Eq (α := (ω : Ω) → (j : κ) → ℝ) (fun (ω : Ω) (j : κ) ↦ Y j ω)
    (Function.comp (β := WithLp 2 ((j : κ) → ℝ)) ofLp (toLp 2 ∘ fun (ω : Ω) (j : κ) ↦ Y j ω))
this_2 : Fintype ι := Fintype.ofFinite ι
this : Fintype κ := Fintype.ofFinite κ
x : WithLp 2 ((i : ι) → ℝ)
y : WithLp 2 ((j : κ) → ℝ)
refine_2 :
  cov[fun (ω : Ω) ↦
      ∑ x_1 : ι,
        HMul.hMul (α := ℝ)
          ((starRingEnd ℝ : (a : ℝ) → ℝ)
              (ofLp (p := 2)
                ((OrthonormalBasis.repr (EuclideanSpace.basisFun ι ℝ) : (a : EuclideanSpace ℝ ι) → EuclideanSpace ℝ ι)
                  x)
                x_1) :
            ℝ)
          (inner ℝ (E := WithLp 2 ((i : ι) → ℝ))
            ((EuclideanSpace.basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) x_1 : EuclideanSpace ℝ ι)
            ((toLp 2 ∘ fun (ω : Ω) (i : ι) ↦ X i ω) ω : WithLp 2 ((i : ι) → ℝ))),
      fun (ω : Ω) ↦
      ∑ x : κ,
        HMul.hMul (α := ℝ)
          ((starRingEnd ℝ : (a : ℝ) → ℝ)
              (ofLp (p := 2)
                ((OrthonormalBasis.repr (EuclideanSpace.basisFun κ ℝ) : (a : EuclideanSpace ℝ κ) → EuclideanSpace ℝ κ)
                  y)
                x) :
            ℝ)
          (inner ℝ (E := WithLp 2 ((j : κ) → ℝ))
            ((EuclideanSpace.basisFun κ ℝ : (a : κ) → EuclideanSpace ℝ κ) x : EuclideanSpace ℝ κ)
            ((toLp 2 ∘ fun (ω : Ω) (j : κ) ↦ Y j ω) ω : WithLp 2 ((j : κ) → ℝ)));
      P] =
    0
⊢ cov[fun (ω : Ω) ↦
      inner.{0, u_4} ℝ (E := WithLp 2 ((i : ι) → ℝ))
        (∑ i : ι,
          HSMul.hSMul (α := (fun (x : ι) ↦ ℝ) i) (β := EuclideanSpace ℝ ι)
            (ofLp (p := 2)
              ((OrthonormalBasis.repr (EuclideanSpace.basisFun ι ℝ) : (a : EuclideanSpace ℝ ι) → EuclideanSpace ℝ ι) x)
              i)
            ((EuclideanSpace.basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) i : EuclideanSpace ℝ ι))
        ((toLp 2 ∘ fun (ω : Ω) (i : ι) ↦ X i ω) ω),
      fun (ω : Ω) ↦
      inner.{0, u_5} ℝ (E := WithLp 2 ((j : κ) → ℝ))
        (∑ i : κ,
          HSMul.hSMul (α := (fun (x : κ) ↦ ℝ) i) (β := EuclideanSpace ℝ κ)
            (ofLp (p := 2)
              ((OrthonormalBasis.repr (EuclideanSpace.basisFun κ ℝ) : (a : EuclideanSpace ℝ κ) → EuclideanSpace ℝ κ) y)
              i)
            ((EuclideanSpace.basisFun κ ℝ : (a : κ) → EuclideanSpace ℝ κ) i : EuclideanSpace ℝ κ))
        ((toLp 2 ∘ fun (ω : Ω) (j : κ) ↦ Y j ω) ω);
      P] =
    0

Tactic:
simp_rw [sum_inner, inner_smul_left]

Premises used: sum_inner, inner_smul_left
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_4
κ : Type u_5
inst : Finite ι
inst_1 : Finite κ
X : ι → Ω → ℝ
Y : κ → Ω → ℝ
hXY :
  HasGaussianLaw (E := Prod.{u_4, u_5} ((i : ι) → ℝ) ((j : κ) → ℝ))
    (fun (ω : Ω) ↦ (fun (i : ι) ↦ X i ω, fun (j : κ) ↦ Y j ω)) P
h : ∀ (i : ι) (j : κ), cov[X i, Y j; P] = 0
this_1 : IsProbabilityMeasure P
hX :
  Eq (α := (ω : Ω) → (i : ι) → ℝ) (fun (ω : Ω) (i : ι) ↦ X i ω)
    (Function.comp (β := WithLp 2 ((i : ι) → ℝ)) ofLp (toLp 2 ∘ fun (ω : Ω) (i : ι) ↦ X i ω))
hY :
  Eq (α := (ω : Ω) → (j : κ) → ℝ) (fun (ω : Ω) (j : κ) ↦ Y j ω)
    (Function.comp (β := WithLp 2 ((j : κ) → ℝ)) ofLp (toLp 2 ∘ fun (ω : Ω) (j : κ) ↦ Y j ω))
this_2 : Fintype ι := Fintype.ofFinite ι
this : Fintype κ := Fintype.ofFinite κ
x : WithLp 2 ((i : ι) → ℝ)
y : WithLp 2 ((j : κ) → ℝ)
refine_2 :
  Eq (α := ℝ) (∑ x_1 : ι, ∑ x_2 : κ, cov[fun (ω : Ω) ↦ x.ofLp x_1 * X x_1 ω, fun (ω : Ω) ↦ y.ofLp x_2 * Y x_2 ω; P]) 0
⊢ Eq (α := ℝ)
    (∑ i : ι,
      ∑ j : κ,
        cov[fun (ω : Ω) ↦
          HMul.hMul (α := ℝ)
            ((starRingEnd ℝ : (a : ℝ) → ℝ)
                (ofLp (p := 2)
                  ((OrthonormalBasis.repr (EuclideanSpace.basisFun ι ℝ) : (a : EuclideanSpace ℝ ι) → EuclideanSpace ℝ ι)
                    x)
                  i) :
              ℝ)
            (inner ℝ (E := WithLp 2 ((i : ι) → ℝ))
              ((EuclideanSpace.basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) i : EuclideanSpace ℝ ι)
              ((toLp 2 ∘ fun (ω : Ω) (i : ι) ↦ X i ω) ω : WithLp 2 ((i : ι) → ℝ))),
          fun (ω : Ω) ↦
          HMul.hMul (α := ℝ)
            ((starRingEnd ℝ : (a : ℝ) → ℝ)
                (ofLp (p := 2)
                  ((OrthonormalBasis.repr (EuclideanSpace.basisFun κ ℝ) : (a : EuclideanSpace ℝ κ) → EuclideanSpace ℝ κ)
                    y)
                  j) :
              ℝ)
            (inner ℝ (E := WithLp 2 ((j : κ) → ℝ))
              ((EuclideanSpace.basisFun κ ℝ : (a : κ) → EuclideanSpace ℝ κ) j : EuclideanSpace ℝ κ)
              ((toLp 2 ∘ fun (ω : Ω) (j : κ) ↦ Y j ω) ω : WithLp 2 ((j : κ) → ℝ)));
          P])
    0

Tactic:
simp only [EuclideanSpace.basisFun_repr, conj_trivial, Function.comp_apply,
      EuclideanSpace.basisFun_inner]

Premises used: conj_trivial, EuclideanSpace.basisFun_repr, EuclideanSpace.basisFun_inner, Function.comp_apply
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_4
κ : Type u_5
inst : Finite ι
inst_1 : Finite κ
X : ι → Ω → ℝ
Y : κ → Ω → ℝ
hXY :
  HasGaussianLaw (E := Prod.{u_4, u_5} ((i : ι) → ℝ) ((j : κ) → ℝ))
    (fun (ω : Ω) ↦ (fun (i : ι) ↦ X i ω, fun (j : κ) ↦ Y j ω)) P
h : ∀ (i : ι) (j : κ), cov[X i, Y j; P] = 0
this_1 : IsProbabilityMeasure P
hX :
  Eq (α := (ω : Ω) → (i : ι) → ℝ) (fun (ω : Ω) (i : ι) ↦ X i ω)
    (Function.comp (β := WithLp 2 ((i : ι) → ℝ)) ofLp (toLp 2 ∘ fun (ω : Ω) (i : ι) ↦ X i ω))
hY :
  Eq (α := (ω : Ω) → (j : κ) → ℝ) (fun (ω : Ω) (j : κ) ↦ Y j ω)
    (Function.comp (β := WithLp 2 ((j : κ) → ℝ)) ofLp (toLp 2 ∘ fun (ω : Ω) (j : κ) ↦ Y j ω))
this_2 : Fintype ι := Fintype.ofFinite ι
this : Fintype κ := Fintype.ofFinite κ
x : WithLp 2 ((i : ι) → ℝ)
y : WithLp 2 ((j : κ) → ℝ)
⊢ Eq (α := ℝ) (∑ x_1 : ι, ∑ x_2 : κ, cov[fun (ω : Ω) ↦ x.ofLp x_1 * X x_1 ω, fun (ω : Ω) ↦ y.ofLp x_2 * Y x_2 ω; P]) 0

Tactic:
sum_eq_zero fun k _ ↦ sum_eq_zero fun l _ ↦ ?_

Premises used: Finset.sum_eq_zero
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_4
κ : Type u_5
inst : Finite ι
inst_1 : Finite κ
X : ι → Ω → ℝ
Y : κ → Ω → ℝ
hXY :
  HasGaussianLaw (E := Prod.{u_4, u_5} ((i : ι) → ℝ) ((j : κ) → ℝ))
    (fun (ω : Ω) ↦ (fun (i : ι) ↦ X i ω, fun (j : κ) ↦ Y j ω)) P
h : ∀ (i : ι) (j : κ), cov[X i, Y j; P] = 0
this_1 : IsProbabilityMeasure P
hX :
  Eq (α := (ω : Ω) → (i : ι) → ℝ) (fun (ω : Ω) (i : ι) ↦ X i ω)
    (Function.comp (β := WithLp 2 ((i : ι) → ℝ)) ofLp (toLp 2 ∘ fun (ω : Ω) (i : ι) ↦ X i ω))
hY :
  Eq (α := (ω : Ω) → (j : κ) → ℝ) (fun (ω : Ω) (j : κ) ↦ Y j ω)
    (Function.comp (β := WithLp 2 ((j : κ) → ℝ)) ofLp (toLp 2 ∘ fun (ω : Ω) (j : κ) ↦ Y j ω))
this_2 : Fintype ι := Fintype.ofFinite ι
this : Fintype κ := Fintype.ofFinite κ
x : WithLp 2 ((i : ι) → ℝ)
y : WithLp 2 ((j : κ) → ℝ)
refine_2 :
  ∀ (k : ι),
    Membership.mem (γ := Finset ι) univ k →
      ∀ (l : κ),
        Membership.mem (γ := Finset κ) univ l →
          cov[fun (ω : Ω) ↦ x.ofLp k * X k ω, fun (ω : Ω) ↦ y.ofLp l * Y l ω; P] = 0
⊢ Eq (α := ℝ) (∑ x_1 : ι, ∑ x_2 : κ, cov[fun (ω : Ω) ↦ x.ofLp x_1 * X x_1 ω, fun (ω : Ω) ↦ y.ofLp x_2 * Y x_2 ω; P]) 0

Tactic:
refine sum_eq_zero fun k _ ↦ sum_eq_zero fun l _ ↦ ?_

Premises used: Finset.sum_eq_zero
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_4
κ : Type u_5
inst : Finite ι
inst_1 : Finite κ
X : ι → Ω → ℝ
Y : κ → Ω → ℝ
hXY :
  HasGaussianLaw (E := Prod.{u_4, u_5} ((i : ι) → ℝ) ((j : κ) → ℝ))
    (fun (ω : Ω) ↦ (fun (i : ι) ↦ X i ω, fun (j : κ) ↦ Y j ω)) P
h : ∀ (i : ι) (j : κ), cov[X i, Y j; P] = 0
this_1 : IsProbabilityMeasure P
hX :
  Eq (α := (ω : Ω) → (i : ι) → ℝ) (fun (ω : Ω) (i : ι) ↦ X i ω)
    (Function.comp (β := WithLp 2 ((i : ι) → ℝ)) ofLp (toLp 2 ∘ fun (ω : Ω) (i : ι) ↦ X i ω))
hY :
  Eq (α := (ω : Ω) → (j : κ) → ℝ) (fun (ω : Ω) (j : κ) ↦ Y j ω)
    (Function.comp (β := WithLp 2 ((j : κ) → ℝ)) ofLp (toLp 2 ∘ fun (ω : Ω) (j : κ) ↦ Y j ω))
this_2 : Fintype ι := Fintype.ofFinite ι
this : Fintype κ := Fintype.ofFinite κ
x : WithLp 2 ((i : ι) → ℝ)
y : WithLp 2 ((j : κ) → ℝ)
k : ι
h_1 : Membership.mem (γ := Finset ι) univ k
l : κ
h_2 : Membership.mem (γ := Finset κ) univ l
refine_2 : x.ofLp k * cov[X k, fun (ω : Ω) ↦ y.ofLp l * Y l ω; P] = 0
refine_2₁ : x.ofLp k * (y.ofLp l * cov[X k, Y l; P]) = 0
refine_2₂ : x.ofLp k * (y.ofLp l * 0) = 0
refine_2₃ : x.ofLp k * 0 = 0
refine_2₄ refine_2₅ : Eq (α := ℝ) 0 0
⊢ cov[fun (ω : Ω) ↦ x.ofLp k * X k ω, fun (ω : Ω) ↦ y.ofLp l * Y l ω; P] = 0

Tactic:
rw [covariance_const_mul_left, covariance_const_mul_right, h, mul_zero, mul_zero]

Premises used: ProbabilityTheory.covariance_const_mul_right, MulZeroClass.mul_zero, ProbabilityTheory.covariance_const_mul_left
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_4
κ : Type u_5
inst : Finite ι
inst_1 : Finite κ
X : ι → Ω → ℝ
Y : κ → Ω → ℝ
hXY :
  HasGaussianLaw (E := Prod.{u_4, u_5} ((i : ι) → ℝ) ((j : κ) → ℝ))
    (fun (ω : Ω) ↦ (fun (i : ι) ↦ X i ω, fun (j : κ) ↦ Y j ω)) P
h : ∀ (i : ι) (j : κ), cov[X i, Y j; P] = 0
this_1 : IsProbabilityMeasure P
hX :
  Eq (α := (ω : Ω) → (i : ι) → ℝ) (fun (ω : Ω) (i : ι) ↦ X i ω)
    (Function.comp (β := WithLp 2 ((i : ι) → ℝ)) ofLp (toLp 2 ∘ fun (ω : Ω) (i : ι) ↦ X i ω))
hY :
  Eq (α := (ω : Ω) → (j : κ) → ℝ) (fun (ω : Ω) (j : κ) ↦ Y j ω)
    (Function.comp (β := WithLp 2 ((j : κ) → ℝ)) ofLp (toLp 2 ∘ fun (ω : Ω) (j : κ) ↦ Y j ω))
this_2 : Fintype ι := Fintype.ofFinite ι
this : Fintype κ := Fintype.ofFinite κ
x : WithLp 2 ((i : ι) → ℝ)
y : WithLp 2 ((j : κ) → ℝ)
refine_2 : ∀ (i : ι), MemLp (ε := ℝ) (fun (ω : Ω) ↦ x.ofLp i * X i ω) 2 P
⊢ ∀ (i : ι),
    MemLp (ε := ℝ)
      (fun (ω : Ω) ↦
        HMul.hMul (α := ℝ)
          ((starRingEnd ℝ : (a : ℝ) → ℝ)
              (ofLp (p := 2)
                ((OrthonormalBasis.repr (EuclideanSpace.basisFun ι ℝ) : (a : EuclideanSpace ℝ ι) → EuclideanSpace ℝ ι)
                  x)
                i) :
            ℝ)
          (inner ℝ (E := WithLp 2 ((i : ι) → ℝ))
            ((EuclideanSpace.basisFun ι ℝ : (a : ι) → EuclideanSpace ℝ ι) i : EuclideanSpace ℝ ι)
            ((toLp 2 ∘ fun (ω : Ω) (i : ι) ↦ X i ω) ω : WithLp 2 ((i : ι) → ℝ))))
      2 P

Tactic:
simp only [EuclideanSpace.basisFun_repr, conj_trivial, Function.comp_apply,
    EuclideanSpace.basisFun_inner]

Premises used: conj_trivial, EuclideanSpace.basisFun_repr, EuclideanSpace.basisFun_inner, Function.comp_apply
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_4
κ : Type u_5
inst : Finite ι
inst_1 : Finite κ
X : ι → Ω → ℝ
Y : κ → Ω → ℝ
hXY :
  HasGaussianLaw (E := Prod.{u_4, u_5} ((i : ι) → ℝ) ((j : κ) → ℝ))
    (fun (ω : Ω) ↦ (fun (i : ι) ↦ X i ω, fun (j : κ) ↦ Y j ω)) P
h : ∀ (i : ι) (j : κ), cov[X i, Y j; P] = 0
this_1 : IsProbabilityMeasure P
hX :
  Eq (α := (ω : Ω) → (i : ι) → ℝ) (fun (ω : Ω) (i : ι) ↦ X i ω)
    (Function.comp (β := WithLp 2 ((i : ι) → ℝ)) ofLp (toLp 2 ∘ fun (ω : Ω) (i : ι) ↦ X i ω))
hY :
  Eq (α := (ω : Ω) → (j : κ) → ℝ) (fun (ω : Ω) (j : κ) ↦ Y j ω)
    (Function.comp (β := WithLp 2 ((j : κ) → ℝ)) ofLp (toLp 2 ∘ fun (ω : Ω) (j : κ) ↦ Y j ω))
this_2 : Fintype ι := Fintype.ofFinite ι
this : Fintype κ := Fintype.ofFinite κ
x : WithLp 2 ((i : ι) → ℝ)
y : WithLp 2 ((j : κ) → ℝ)
⊢ ∀ (i : ι), MemLp (ε := ℝ) (fun (ω : Ω) ↦ x.ofLp i * X i ω) 2 P

Tactic:
fun i ↦ (hXY.fst.eval i).memLp_two.const_mul _

Premises used: MeasureTheory.MemLp.const_mul, ProbabilityTheory.HasGaussianLaw.fst, ProbabilityTheory.HasGaussianLaw.eval, WithLp.ofLp, ProbabilityTheory.HasGaussianLaw.memLp_two
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_4
κ : Type u_5
inst : Finite ι
inst_1 : Finite κ
X : ι → Ω → ℝ
Y : κ → Ω → ℝ
hXY :
  HasGaussianLaw (E := Prod.{u_4, u_5} ((i : ι) → ℝ) ((j : κ) → ℝ))
    (fun (ω : Ω) ↦ (fun (i : ι) ↦ X i ω, fun (j : κ) ↦ Y j ω)) P
h : ∀ (i : ι) (j : κ), cov[X i, Y j; P] = 0
this_1 : IsProbabilityMeasure P
hX :
  Eq (α := (ω : Ω) → (i : ι) → ℝ) (fun (ω : Ω) (i : ι) ↦ X i ω)
    (Function.comp (β := WithLp 2 ((i : ι) → ℝ)) ofLp (toLp 2 ∘ fun (ω : Ω) (i : ι) ↦ X i ω))
hY :
  Eq (α := (ω : Ω) → (j : κ) → ℝ) (fun (ω : Ω) (j : κ) ↦ Y j ω)
    (Function.comp (β := WithLp 2 ((j : κ) → ℝ)) ofLp (toLp 2 ∘ fun (ω : Ω) (j : κ) ↦ Y j ω))
this_2 : Fintype ι := Fintype.ofFinite ι
this : Fintype κ := Fintype.ofFinite κ
x : WithLp 2 ((i : ι) → ℝ)
y : WithLp 2 ((j : κ) → ℝ)
⊢ ∀ (i : ι), MemLp (ε := ℝ) (fun (ω : Ω) ↦ x.ofLp i * X i ω) 2 P

Tactic:
exact fun i ↦ (hXY.fst.eval i).memLp_two.const_mul _

Premises used: MeasureTheory.MemLp.const_mul, ProbabilityTheory.HasGaussianLaw.fst, ProbabilityTheory.HasGaussianLaw.eval, ProbabilityTheory.HasGaussianLaw.memLp_two
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_4
κ : Type u_5
inst : Finite ι
inst_1 : Finite κ
X : ι → Ω → ℝ
Y : κ → Ω → ℝ
hXY :
  HasGaussianLaw (E := Prod.{u_4, u_5} ((i : ι) → ℝ) ((j : κ) → ℝ))
    (fun (ω : Ω) ↦ (fun (i : ι) ↦ X i ω, fun (j : κ) ↦ Y j ω)) P
h : ∀ (i : ι) (j : κ), cov[X i, Y j; P] = 0
this_1 : IsProbabilityMeasure P
hX :
  Eq (α := (ω : Ω) → (i : ι) → ℝ) (fun (ω : Ω) (i : ι) ↦ X i ω)
    (Function.comp (β := WithLp 2 ((i : ι) → ℝ)) ofLp (toLp 2 ∘ fun (ω : Ω) (i : ι) ↦ X i ω))
hY :
  Eq (α := (ω : Ω) → (j : κ) → ℝ) (fun (ω : Ω) (j : κ) ↦ Y j ω)
    (Function.comp (β := WithLp 2 ((j : κ) → ℝ)) ofLp (toLp 2 ∘ fun (ω : Ω) (j : κ) ↦ Y j ω))
this_2 : Fintype ι := Fintype.ofFinite ι
this : Fintype κ := Fintype.ofFinite κ
x : WithLp 2 ((i : ι) → ℝ)
y : WithLp 2 ((j : κ) → ℝ)
refine_2 : ∀ (i : κ), MemLp (ε := ℝ) (fun (ω : Ω) ↦ y.ofLp i * Y i ω) 2 P
⊢ ∀ (i : κ),
    MemLp (ε := ℝ)
      (fun (ω : Ω) ↦
        HMul.hMul (α := ℝ)
          ((starRingEnd ℝ : (a : ℝ) → ℝ)
              (ofLp (p := 2)
                ((OrthonormalBasis.repr (EuclideanSpace.basisFun κ ℝ) : (a : EuclideanSpace ℝ κ) → EuclideanSpace ℝ κ)
                  y)
                i) :
            ℝ)
          (inner ℝ (E := WithLp 2 ((j : κ) → ℝ))
            ((EuclideanSpace.basisFun κ ℝ : (a : κ) → EuclideanSpace ℝ κ) i : EuclideanSpace ℝ κ)
            ((toLp 2 ∘ fun (ω : Ω) (j : κ) ↦ Y j ω) ω : WithLp 2 ((j : κ) → ℝ))))
      2 P

Tactic:
simp only [EuclideanSpace.basisFun_repr, conj_trivial, Function.comp_apply,
      EuclideanSpace.basisFun_inner]

Premises used: conj_trivial, EuclideanSpace.basisFun_repr, EuclideanSpace.basisFun_inner, Function.comp_apply
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_4
κ : Type u_5
inst : Finite ι
inst_1 : Finite κ
X : ι → Ω → ℝ
Y : κ → Ω → ℝ
hXY :
  HasGaussianLaw (E := Prod.{u_4, u_5} ((i : ι) → ℝ) ((j : κ) → ℝ))
    (fun (ω : Ω) ↦ (fun (i : ι) ↦ X i ω, fun (j : κ) ↦ Y j ω)) P
h : ∀ (i : ι) (j : κ), cov[X i, Y j; P] = 0
this_1 : IsProbabilityMeasure P
hX :
  Eq (α := (ω : Ω) → (i : ι) → ℝ) (fun (ω : Ω) (i : ι) ↦ X i ω)
    (Function.comp (β := WithLp 2 ((i : ι) → ℝ)) ofLp (toLp 2 ∘ fun (ω : Ω) (i : ι) ↦ X i ω))
hY :
  Eq (α := (ω : Ω) → (j : κ) → ℝ) (fun (ω : Ω) (j : κ) ↦ Y j ω)
    (Function.comp (β := WithLp 2 ((j : κ) → ℝ)) ofLp (toLp 2 ∘ fun (ω : Ω) (j : κ) ↦ Y j ω))
this_2 : Fintype ι := Fintype.ofFinite ι
this : Fintype κ := Fintype.ofFinite κ
x : WithLp 2 ((i : ι) → ℝ)
y : WithLp 2 ((j : κ) → ℝ)
⊢ ∀ (i : κ), MemLp (ε := ℝ) (fun (ω : Ω) ↦ y.ofLp i * Y i ω) 2 P

Tactic:
fun j ↦ (hXY.snd.eval j).memLp_two.const_mul _

Premises used: MeasureTheory.MemLp.const_mul, ProbabilityTheory.HasGaussianLaw.snd, ProbabilityTheory.HasGaussianLaw.eval, WithLp.ofLp, ProbabilityTheory.HasGaussianLaw.memLp_two
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_4
κ : Type u_5
inst : Finite ι
inst_1 : Finite κ
X : ι → Ω → ℝ
Y : κ → Ω → ℝ
hXY :
  HasGaussianLaw (E := Prod.{u_4, u_5} ((i : ι) → ℝ) ((j : κ) → ℝ))
    (fun (ω : Ω) ↦ (fun (i : ι) ↦ X i ω, fun (j : κ) ↦ Y j ω)) P
h : ∀ (i : ι) (j : κ), cov[X i, Y j; P] = 0
this_1 : IsProbabilityMeasure P
hX :
  Eq (α := (ω : Ω) → (i : ι) → ℝ) (fun (ω : Ω) (i : ι) ↦ X i ω)
    (Function.comp (β := WithLp 2 ((i : ι) → ℝ)) ofLp (toLp 2 ∘ fun (ω : Ω) (i : ι) ↦ X i ω))
hY :
  Eq (α := (ω : Ω) → (j : κ) → ℝ) (fun (ω : Ω) (j : κ) ↦ Y j ω)
    (Function.comp (β := WithLp 2 ((j : κ) → ℝ)) ofLp (toLp 2 ∘ fun (ω : Ω) (j : κ) ↦ Y j ω))
this_2 : Fintype ι := Fintype.ofFinite ι
this : Fintype κ := Fintype.ofFinite κ
x : WithLp 2 ((i : ι) → ℝ)
y : WithLp 2 ((j : κ) → ℝ)
⊢ ∀ (i : κ), MemLp (ε := ℝ) (fun (ω : Ω) ↦ y.ofLp i * Y i ω) 2 P

Tactic:
exact fun j ↦ (hXY.snd.eval j).memLp_two.const_mul _

Premises used: MeasureTheory.MemLp.const_mul, ProbabilityTheory.HasGaussianLaw.snd, ProbabilityTheory.HasGaussianLaw.eval, ProbabilityTheory.HasGaussianLaw.memLp_two
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ
hXY : HasGaussianLaw (E := ℝ × ℝ) (fun (ω : Ω) ↦ (X ω, Y ω)) P
h : cov[X, Y; P] = 0
L₁ L₂ : StrongDual ℝ ℝ
⊢ cov[(⇑L₁ : (a : ℝ) → ℝ) ∘ X, (⇑L₂ : (a : ℝ) → ℝ) ∘ Y; P] = 0

Tactic:
simp [Function.comp_def, ← toDual_symm_apply, covariance_mul_const_right,
      covariance_mul_const_left, h]

Premises used: InnerProductSpace.toDual_symm_apply, ProbabilityTheory.covariance_mul_const_left, Function.comp_def, ProbabilityTheory.covariance_mul_const_right
-- 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
inst_5 : CompleteSpace E
ι : Type u_3
inst_6 : Fintype ι
X : ι → Ω → E
hX1 : ∀ (i : ι), HasGaussianLaw (X i) P
hX2 : iIndepFun (β := fun (x : ι) ↦ E) X P
⊢ HasGaussianLaw.{u_1, u_2} (E := E) (∑ i : ι, X i) P

Tactic:
(hX2.hasGaussianLaw hX1).sum

Premises used: ProbabilityTheory.iIndepFun.hasGaussianLaw, ProbabilityTheory.HasGaussianLaw.sum
-- 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
inst_5 : CompleteSpace E
ι : Type u_3
inst_6 : Fintype ι
X : ι → Ω → E
hX1 : ∀ (i : ι), HasGaussianLaw (X i) P
hX2 : iIndepFun (β := fun (x : ι) ↦ E) X P
⊢ HasGaussianLaw.{u_1, u_2} (E := E) (fun (ω : Ω) ↦ ∑ i : ι, X i ω) P

Tactic:
(hX2.hasGaussianLaw hX1).fun_sum

Premises used: ProbabilityTheory.iIndepFun.hasGaussianLaw, ProbabilityTheory.HasGaussianLaw.fun_sum
-- 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
inst_5 : CompleteSpace E
X Y : Ω → E
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
h : X ⟂ᵢ[P] Y
⊢ HasGaussianLaw (X + Y) P

Tactic:
(h.hasGaussianLaw hX hY).add

Premises used: ProbabilityTheory.HasGaussianLaw.add, ProbabilityTheory.IndepFun.hasGaussianLaw
-- 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
inst_5 : CompleteSpace E
X Y : Ω → E
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
h : X ⟂ᵢ[P] Y
⊢ HasGaussianLaw.{u_1, u_2} (E := E) (fun (ω : Ω) ↦ X ω + Y ω) P

Tactic:
(h.hasGaussianLaw hX hY).add

Premises used: ProbabilityTheory.HasGaussianLaw.add, ProbabilityTheory.IndepFun.hasGaussianLaw
-- 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
inst_5 : CompleteSpace E
X Y : Ω → E
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
h : X ⟂ᵢ[P] Y
⊢ HasGaussianLaw (X - Y) P

Tactic:
(h.hasGaussianLaw hX hY).sub

Premises used: ProbabilityTheory.HasGaussianLaw.sub, ProbabilityTheory.IndepFun.hasGaussianLaw
-- 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
inst_5 : CompleteSpace E
X Y : Ω → E
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
h : X ⟂ᵢ[P] Y
⊢ HasGaussianLaw.{u_1, u_2} (E := E) (fun (ω : Ω) ↦ X ω - Y ω) P

Tactic:
(h.hasGaussianLaw hX hY).sub

Premises used: ProbabilityTheory.HasGaussianLaw.sub, ProbabilityTheory.IndepFun.hasGaussianLaw
-- 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
⊢ IsProbabilityMeasure P

Tactic:
have : IsProbabilityMeasure P := hX.isProbabilityMeasure
-- 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
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
rw :
  ∀ (L : StrongDual ℝ E),
    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)
⊢ HasGaussianLaw (Y - X) P

Tactic:
rw [hasGaussianLaw_iff_charFunDual_map_eq (by fun_prop)]

Premises used: ProbabilityTheory.hasGaussianLaw_iff_charFunDual_map_eq