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

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

Tactic:
rw [covariance_fun_sum_fun_sum]

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

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

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