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

Goal state before:
pp: case fst
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
x y : ↥(I.disjSum J) → E
x✝ : ↥I
⊢ (fun s ↦ (x + y) ⟨Sum.inl ↑s, ⋯⟩, fun t ↦ (x + y) ⟨Sum.inr ↑t, ⋯⟩).1 x✝ =
    ((fun s ↦ x ⟨Sum.inl ↑s, ⋯⟩, fun t ↦ x ⟨Sum.inr ↑t, ⋯⟩) + (fun s ↦ y ⟨Sum.inl ↑s, ⋯⟩, fun t ↦ y ⟨Sum.inr ↑t, ⋯⟩)).1
      x✝

pp: case snd
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
x y : ↥(I.disjSum J) → E
x✝ : ↥J
⊢ (fun s ↦ (x + y) ⟨Sum.inl ↑s, ⋯⟩, fun t ↦ (x + y) ⟨Sum.inr ↑t, ⋯⟩).2 x✝ =
    ((fun s ↦ x ⟨Sum.inl ↑s, ⋯⟩, fun t ↦ x ⟨Sum.inr ↑t, ⋯⟩) + (fun s ↦ y ⟨Sum.inl ↑s, ⋯⟩, fun t ↦ y ⟨Sum.inr ↑t, ⋯⟩)).2
      x✝

Tactic:
<;>

Goal state after:
case fst
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
x y : ↥(I.disjSum J) → E
x✝ : ↥I
⊢ (fun s ↦ (x + y) ⟨Sum.inl ↑s, ⋯⟩, fun t ↦ (x + y) ⟨Sum.inr ↑t, ⋯⟩).1 x✝ =
    ((fun s ↦ x ⟨Sum.inl ↑s, ⋯⟩, fun t ↦ x ⟨Sum.inr ↑t, ⋯⟩) + (fun s ↦ y ⟨Sum.inl ↑s, ⋯⟩, fun t ↦ y ⟨Sum.inr ↑t, ⋯⟩)).1
      x✝

case snd
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
x y : ↥(I.disjSum J) → E
x✝ : ↥J
⊢ (fun s ↦ (x + y) ⟨Sum.inl ↑s, ⋯⟩, fun t ↦ (x + y) ⟨Sum.inr ↑t, ⋯⟩).2 x✝ =
    ((fun s ↦ x ⟨Sum.inl ↑s, ⋯⟩, fun t ↦ x ⟨Sum.inr ↑t, ⋯⟩) + (fun s ↦ y ⟨Sum.inl ↑s, ⋯⟩, fun t ↦ y ⟨Sum.inr ↑t, ⋯⟩)).2
      x✝