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 → ℝ)
⊢ ∑ 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

pp: 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

pp: 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

Tactic:
· simp only [EuclideanSpace.basisFun_repr, conj_trivial, Function.comp_apply,
      EuclideanSpace.basisFun_inner]
    refine sum_eq_zero fun k _ ↦ sum_eq_zero fun l _ ↦ ?_
    rw [covariance_const_mul_left, covariance_const_mul_right, h i j hij k l, mul_zero, mul_zero]

Goal state after:
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