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

Goal state before:
pp: case refine_2
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
S : Type u_4
X : S → Ω → E
Y : T → Ω → E
inst✝ : NormedSpace ℝ E
hXY : IsGaussianProcess (Sum.elim X Y) P
mX : ∀ (s : S), AEMeasurable (X s) P
mY : ∀ (t : T), AEMeasurable (Y t) P
h : ∀ (s : S) (t : T) (L₁ L₂ : StrongDual ℝ E), cov[⇑L₁ ∘ X s, ⇑L₂ ∘ Y t; P] = 0
this : IsProbabilityMeasure P
I : Finset S
J : Finset T
L₁ : StrongDual ℝ (↥I → E)
L₂ : StrongDual ℝ (↥J → E)
h1 : (⇑L₁ ∘ fun ω i ↦ X (↑i) ω) = ∑ i, ⇑(L₁ ∘SL ContinuousLinearMap.single ℝ (fun i ↦ E) i) ∘ X ↑i
h2 : (⇑L₂ ∘ fun ω j ↦ Y (↑j) ω) = ∑ j, ⇑(L₂ ∘SL ContinuousLinearMap.single ℝ (fun j ↦ E) j) ∘ Y ↑j
⊢ ∑ i,
      ∑ j,
        cov[⇑(L₁ ∘SL ContinuousLinearMap.single ℝ (fun i ↦ E) i) ∘ X ↑i,
          ⇑(L₂ ∘SL ContinuousLinearMap.single ℝ (fun j ↦ E) j) ∘ Y ↑j; P] =
    0

pp: case refine_2.hX
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
S : Type u_4
X : S → Ω → E
Y : T → Ω → E
inst✝ : NormedSpace ℝ E
hXY : IsGaussianProcess (Sum.elim X Y) P
mX : ∀ (s : S), AEMeasurable (X s) P
mY : ∀ (t : T), AEMeasurable (Y t) P
h : ∀ (s : S) (t : T) (L₁ L₂ : StrongDual ℝ E), cov[⇑L₁ ∘ X s, ⇑L₂ ∘ Y t; P] = 0
this : IsProbabilityMeasure P
I : Finset S
J : Finset T
L₁ : StrongDual ℝ (↥I → E)
L₂ : StrongDual ℝ (↥J → E)
h1 : (⇑L₁ ∘ fun ω i ↦ X (↑i) ω) = ∑ i, ⇑(L₁ ∘SL ContinuousLinearMap.single ℝ (fun i ↦ E) i) ∘ X ↑i
h2 : (⇑L₂ ∘ fun ω j ↦ Y (↑j) ω) = ∑ j, ⇑(L₂ ∘SL ContinuousLinearMap.single ℝ (fun j ↦ E) j) ∘ Y ↑j
⊢ ∀ (i : ↥I), MemLp (⇑(L₁ ∘SL ContinuousLinearMap.single ℝ (fun i ↦ E) i) ∘ X ↑i) 2 P

pp: case refine_2.hY
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
S : Type u_4
X : S → Ω → E
Y : T → Ω → E
inst✝ : NormedSpace ℝ E
hXY : IsGaussianProcess (Sum.elim X Y) P
mX : ∀ (s : S), AEMeasurable (X s) P
mY : ∀ (t : T), AEMeasurable (Y t) P
h : ∀ (s : S) (t : T) (L₁ L₂ : StrongDual ℝ E), cov[⇑L₁ ∘ X s, ⇑L₂ ∘ Y t; P] = 0
this : IsProbabilityMeasure P
I : Finset S
J : Finset T
L₁ : StrongDual ℝ (↥I → E)
L₂ : StrongDual ℝ (↥J → E)
h1 : (⇑L₁ ∘ fun ω i ↦ X (↑i) ω) = ∑ i, ⇑(L₁ ∘SL ContinuousLinearMap.single ℝ (fun i ↦ E) i) ∘ X ↑i
h2 : (⇑L₂ ∘ fun ω j ↦ Y (↑j) ω) = ∑ j, ⇑(L₂ ∘SL ContinuousLinearMap.single ℝ (fun j ↦ E) j) ∘ Y ↑j
⊢ ∀ (i : ↥J), MemLp (⇑(L₂ ∘SL ContinuousLinearMap.single ℝ (fun j ↦ E) i) ∘ Y ↑i) 2 P

Tactic:
· exact sum_eq_zero fun i _ ↦ sum_eq_zero fun j _ ↦ h ..

Goal state after:
case refine_2.hX
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
S : Type u_4
X : S → Ω → E
Y : T → Ω → E
inst✝ : NormedSpace ℝ E
hXY : IsGaussianProcess (Sum.elim X Y) P
mX : ∀ (s : S), AEMeasurable (X s) P
mY : ∀ (t : T), AEMeasurable (Y t) P
h : ∀ (s : S) (t : T) (L₁ L₂ : StrongDual ℝ E), cov[⇑L₁ ∘ X s, ⇑L₂ ∘ Y t; P] = 0
this : IsProbabilityMeasure P
I : Finset S
J : Finset T
L₁ : StrongDual ℝ (↥I → E)
L₂ : StrongDual ℝ (↥J → E)
h1 : (⇑L₁ ∘ fun ω i ↦ X (↑i) ω) = ∑ i, ⇑(L₁ ∘SL ContinuousLinearMap.single ℝ (fun i ↦ E) i) ∘ X ↑i
h2 : (⇑L₂ ∘ fun ω j ↦ Y (↑j) ω) = ∑ j, ⇑(L₂ ∘SL ContinuousLinearMap.single ℝ (fun j ↦ E) j) ∘ Y ↑j
⊢ ∀ (i : ↥I), MemLp (⇑(L₁ ∘SL ContinuousLinearMap.single ℝ (fun i ↦ E) i) ∘ X ↑i) 2 P

case refine_2.hY
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
S : Type u_4
X : S → Ω → E
Y : T → Ω → E
inst✝ : NormedSpace ℝ E
hXY : IsGaussianProcess (Sum.elim X Y) P
mX : ∀ (s : S), AEMeasurable (X s) P
mY : ∀ (t : T), AEMeasurable (Y t) P
h : ∀ (s : S) (t : T) (L₁ L₂ : StrongDual ℝ E), cov[⇑L₁ ∘ X s, ⇑L₂ ∘ Y t; P] = 0
this : IsProbabilityMeasure P
I : Finset S
J : Finset T
L₁ : StrongDual ℝ (↥I → E)
L₂ : StrongDual ℝ (↥J → E)
h1 : (⇑L₁ ∘ fun ω i ↦ X (↑i) ω) = ∑ i, ⇑(L₁ ∘SL ContinuousLinearMap.single ℝ (fun i ↦ E) i) ∘ X ↑i
h2 : (⇑L₂ ∘ fun ω j ↦ Y (↑j) ω) = ∑ j, ⇑(L₂ ∘SL ContinuousLinearMap.single ℝ (fun j ↦ E) j) ∘ Y ↑j
⊢ ∀ (i : ↥J), MemLp (⇑(L₂ ∘SL ContinuousLinearMap.single ℝ (fun j ↦ E) i) ∘ Y ↑i) 2 P