Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence

Goal state before:
pp: case refine_2
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_4
κ : Type u_5
inst✝¹ : Finite ι
inst✝ : Finite κ
X : ι → Ω → ℝ
Y : κ → Ω → ℝ
hXY : HasGaussianLaw (fun ω ↦ (fun i ↦ X i ω, fun j ↦ Y j ω)) P
h : ∀ (i : ι) (j : κ), cov[X i, Y j; P] = 0
this✝¹ : IsProbabilityMeasure P
hX : (fun ω i ↦ X i ω) = ofLp ∘ toLp 2 ∘ fun ω i ↦ X i ω
hY : (fun ω j ↦ Y j ω) = ofLp ∘ toLp 2 ∘ fun ω j ↦ Y j ω
this✝ : Fintype ι := Fintype.ofFinite ι
this : Fintype κ := Fintype.ofFinite κ
x : WithLp 2 (ι → ℝ)
y : WithLp 2 (κ → ℝ)
⊢ cov[fun ω ↦
      ∑ x_1,
        (starRingEnd ℝ) (((EuclideanSpace.basisFun ι ℝ).repr x).ofLp x_1) *
          ⟪(EuclideanSpace.basisFun ι ℝ) x_1, (toLp 2 ∘ fun ω i ↦ X i ω) ω⟫,
      fun ω ↦
      ∑ x,
        (starRingEnd ℝ) (((EuclideanSpace.basisFun κ ℝ).repr y).ofLp x) *
          ⟪(EuclideanSpace.basisFun κ ℝ) x, (toLp 2 ∘ fun ω j ↦ Y j ω) ω⟫;
      P] =
    0

Tactic:
rw [covariance_fun_sum_fun_sum]

Goal state after:
case refine_2
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_4
κ : Type u_5
inst✝¹ : Finite ι
inst✝ : Finite κ
X : ι → Ω → ℝ
Y : κ → Ω → ℝ
hXY : HasGaussianLaw (fun ω ↦ (fun i ↦ X i ω, fun j ↦ Y j ω)) P
h : ∀ (i : ι) (j : κ), cov[X i, Y j; P] = 0
this✝¹ : IsProbabilityMeasure P
hX : (fun ω i ↦ X i ω) = ofLp ∘ toLp 2 ∘ fun ω i ↦ X i ω
hY : (fun ω j ↦ Y j ω) = ofLp ∘ toLp 2 ∘ fun ω j ↦ Y j ω
this✝ : Fintype ι := Fintype.ofFinite ι
this : Fintype κ := Fintype.ofFinite κ
x : WithLp 2 (ι → ℝ)
y : WithLp 2 (κ → ℝ)
⊢ ∑ i,
      ∑ j,
        cov[fun ω ↦
          (starRingEnd ℝ) (((EuclideanSpace.basisFun ι ℝ).repr x).ofLp i) *
            ⟪(EuclideanSpace.basisFun ι ℝ) i, (toLp 2 ∘ fun ω i ↦ X i ω) ω⟫,
          fun ω ↦
          (starRingEnd ℝ) (((EuclideanSpace.basisFun κ ℝ).repr y).ofLp j) *
            ⟪(EuclideanSpace.basisFun κ ℝ) j, (toLp 2 ∘ fun ω j ↦ Y j ω) ω⟫;
          P] =
    0

case refine_2.hX
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_4
κ : Type u_5
inst✝¹ : Finite ι
inst✝ : Finite κ
X : ι → Ω → ℝ
Y : κ → Ω → ℝ
hXY : HasGaussianLaw (fun ω ↦ (fun i ↦ X i ω, fun j ↦ Y j ω)) P
h : ∀ (i : ι) (j : κ), cov[X i, Y j; P] = 0
this✝¹ : IsProbabilityMeasure P
hX : (fun ω i ↦ X i ω) = ofLp ∘ toLp 2 ∘ fun ω i ↦ X i ω
hY : (fun ω j ↦ Y j ω) = ofLp ∘ toLp 2 ∘ fun ω j ↦ Y j ω
this✝ : Fintype ι := Fintype.ofFinite ι
this : Fintype κ := Fintype.ofFinite κ
x : WithLp 2 (ι → ℝ)
y : WithLp 2 (κ → ℝ)
⊢ ∀ (i : ι),
    MemLp
      (fun ω ↦
        (starRingEnd ℝ) (((EuclideanSpace.basisFun ι ℝ).repr x).ofLp i) *
          ⟪(EuclideanSpace.basisFun ι ℝ) i, (toLp 2 ∘ fun ω i ↦ X i ω) ω⟫)
      2 P

case refine_2.hY
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_4
κ : Type u_5
inst✝¹ : Finite ι
inst✝ : Finite κ
X : ι → Ω → ℝ
Y : κ → Ω → ℝ
hXY : HasGaussianLaw (fun ω ↦ (fun i ↦ X i ω, fun j ↦ Y j ω)) P
h : ∀ (i : ι) (j : κ), cov[X i, Y j; P] = 0
this✝¹ : IsProbabilityMeasure P
hX : (fun ω i ↦ X i ω) = ofLp ∘ toLp 2 ∘ fun ω i ↦ X i ω
hY : (fun ω j ↦ Y j ω) = ofLp ∘ toLp 2 ∘ fun ω j ↦ Y j ω
this✝ : Fintype ι := Fintype.ofFinite ι
this : Fintype κ := Fintype.ofFinite κ
x : WithLp 2 (ι → ℝ)
y : WithLp 2 (κ → ℝ)
⊢ ∀ (i : κ),
    MemLp
      (fun ω ↦
        (starRingEnd ℝ) (((EuclideanSpace.basisFun κ ℝ).repr y).ofLp i) *
          ⟪(EuclideanSpace.basisFun κ ℝ) i, (toLp 2 ∘ fun ω j ↦ Y j ω) ω⟫)
      2 P