awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
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 : κ) → ℝ)
⊢ 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
have refine_2 : 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: rw [covariance_fun_sum_fun_sum]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
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 (α := ℝ)
    (∑ 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
have 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
Tactic: simp only [EuclideanSpace.basisFun_repr, conj_trivial, Function.comp_apply,
      EuclideanSpace.basisFun_inner]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
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
have 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
Tactic: refine sum_eq_zero fun k _ ↦ sum_eq_zero fun l _ ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
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
⊢ cov[fun (ω : Ω) ↦ x.ofLp k * X k ω, fun (ω : Ω) ↦ y.ofLp l * Y l ω; P] = 0
have refine_2 : x.ofLp k * cov[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]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
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
⊢ cov[fun (ω : Ω) ↦ x.ofLp k * X k ω, fun (ω : Ω) ↦ y.ofLp l * Y l ω; P] = 0
have refine_2₁ : x.ofLp k * (y.ofLp l * cov[X k, Y l; P]) = 0
Tactic: rw [covariance_const_mul_left, covariance_const_mul_right, h, mul_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
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
⊢ cov[fun (ω : Ω) ↦ x.ofLp k * X k ω, fun (ω : Ω) ↦ y.ofLp l * Y l ω; P] = 0
have refine_2₂ : x.ofLp k * (y.ofLp l * 0) = 0
Tactic: rw [covariance_const_mul_left, covariance_const_mul_right, h, mul_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
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
⊢ cov[fun (ω : Ω) ↦ x.ofLp k * X k ω, fun (ω : Ω) ↦ y.ofLp l * Y l ω; P] = 0
have refine_2₃ : x.ofLp k * 0 = 0
Tactic: rw [covariance_const_mul_left, covariance_const_mul_right, h, mul_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
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
⊢ cov[fun (ω : Ω) ↦ x.ofLp k * X k ω, fun (ω : Ω) ↦ y.ofLp l * Y l ω; P] = 0
have refine_2₄ : Eq (α := ℝ) 0 0
Tactic: rw [covariance_const_mul_left, covariance_const_mul_right, h, mul_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
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 (ω : Ω) ↦
        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
have refine_2 : ∀ (i : ι), MemLp (ε := ℝ) (fun (ω : Ω) ↦ x.ofLp i * X i ω) 2 P
Tactic: simp only [EuclideanSpace.basisFun_repr, conj_trivial, Function.comp_apply,
    EuclideanSpace.basisFun_inner]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
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 (ω : Ω) ↦
        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
have refine_2 : ∀ (i : κ), MemLp (ε := ℝ) (fun (ω : Ω) ↦ y.ofLp i * Y i ω) 2 P
Tactic: simp only [EuclideanSpace.basisFun_repr, conj_trivial, Function.comp_apply,
      EuclideanSpace.basisFun_inner]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (hypothesis)
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
⊢ HasGaussianLaw (Y - X) P
have this : IsProbabilityMeasure P
Tactic: have : IsProbabilityMeasure P := hX.isProbabilityMeasure
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
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
⊢ AEMeasurable (Y - X) P
have funProp : AEFinStronglyMeasurable.{u_1, u_2} (β := E) (fun (a : Ω) ↦ Y a) P
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
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
⊢ AEMeasurable (Y - X) P
have funProp₁ : AEFinStronglyMeasurable.{u_1, u_2} (β := E) (fun (a : Ω) ↦ X a) P
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
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
⊢ HasGaussianLaw (Y - X) P
have 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)
Tactic: rw [hasGaussianLaw_iff_charFunDual_map_eq (by fun_prop)]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
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 (Y - X) P) L =
    cexp ((↑(∫ (x : Ω), ((⇑L : (a : E) → ℝ) ∘ (Y - X)) x ∂P) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ) ∘ (Y - X); P] : ℂ) / 2)
have ha : charFunDual (mE := inst_2) (Measure.map X P) L ≠ 0
Tactic: apply mul_left_cancel₀ (a := charFunDual (P.map X) L)
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
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
⊢ 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)
have 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)
Tactic: apply mul_left_cancel₀ (a := charFunDual (P.map X) L)
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
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 * 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
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)
⊢ 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)
have h₂ : MemLp (ε := ℝ) ((⇑L : (a : E) → ℝ) ∘ X) 2 P
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]