awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence (goal)
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
inst_4 : CompleteSpace E
S : Type u_4
X : S → Ω → E
Y : T → Ω → E
inst_5 : 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₁ : (a : E) → ℝ) ∘ X s, (⇑L₂ : (a : E) → ℝ) ∘ Y t; P] = 0
this : IsProbabilityMeasure P
refine_1 :
  ∀ (I : Finset S) (J : Finset T),
    HasGaussianLaw (E := ((i : ↥I) → E) × ((j : ↥J) → E))
      (fun (ω : Ω) ↦ (fun (i : ↥I) ↦ X (↑i : S) ω, fun (j : ↥J) ↦ Y (↑j : T) ω)) P
⊢ (fun (ω : Ω) (s : S) ↦ X s ω) ⟂ᵢ[P] fun (ω : Ω) (t : T) ↦ Y t ω
have refine_2 : ∀ (I : Finset S) (J : Finset T) (L₁ : StrongDual ℝ ((i : ↥I) → E)) (L₂ : StrongDual ℝ ((j : ↥J) → E)),
  cov[Function.comp (β := (i : ↥I) → E) (⇑L₁ : (a : (i : ↥I) → E) → ℝ) fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω,
      Function.comp (β := (j : ↥J) → E) (⇑L₂ : (a : (j : ↥J) → E) → ℝ) fun (ω : Ω) (j : ↥J) ↦ Y (↑j : T) ω; P] =
    0
Tactic: refine IndepFun.process_indepFun_process₀ mX mY fun I J ↦
    HasGaussianLaw.indepFun_of_covariance_strongDual ?_ fun L₁ L₂ ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence (goal)
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
inst_4 : CompleteSpace E
S : Type u_4
X : S → Ω → E
Y : T → Ω → E
inst_5 : 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₁ : (a : E) → ℝ) ∘ X s, (⇑L₂ : (a : E) → ℝ) ∘ Y t; P] = 0
this : IsProbabilityMeasure P
I : Finset S
J : Finset T
x y : ↥(I.disjSum J) → E
⊢ (fun (s : ↥I) ↦ (x + y) (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inl (↑s : S)) ⋯), fun (t : ↥J) ↦
      (x + y) (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inr (↑t : T)) ⋯)) =
    HAdd.hAdd (α := (↥I → E) × (↥J → E))
      (fun (s : ↥I) ↦ x (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inl (↑s : S)) ⋯), fun (t : ↥J) ↦
        x (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inr (↑t : T)) ⋯))
      (fun (s : ↥I) ↦ y (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inl (↑s : S)) ⋯), fun (t : ↥J) ↦
        y (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inr (↑t : T)) ⋯))
have fst : ∀ (x_1 : ↥I),
  (fun (s : ↥I) ↦ (x + y) (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inl (↑s : S)) sorry), fun (t : ↥J) ↦
          (x + y) (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inr (↑t : T)) sorry)).1
      x_1 =
    (HAdd.hAdd (α := (↥I → E) × (↥J → E))
          (fun (s : ↥I) ↦ x (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inl (↑s : S)) sorry), fun (t : ↥J) ↦
            x (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inr (↑t : T)) sorry))
          (fun (s : ↥I) ↦ y (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inl (↑s : S)) sorry), fun (t : ↥J) ↦
            y (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inr (↑t : T)) sorry))).1
      x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence (goal)
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
inst_4 : CompleteSpace E
S : Type u_4
X : S → Ω → E
Y : T → Ω → E
inst_5 : 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₁ : (a : E) → ℝ) ∘ X s, (⇑L₂ : (a : E) → ℝ) ∘ Y t; P] = 0
this : IsProbabilityMeasure P
I : Finset S
J : Finset T
x y : ↥(I.disjSum J) → E
fst :
  ∀ (x_1 : ↥I),
    (fun (s : ↥I) ↦ (x + y) (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inl (↑s : S)) ⋯), fun (t : ↥J) ↦
            (x + y) (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inr (↑t : T)) ⋯)).1
        x_1 =
      (HAdd.hAdd (α := (↥I → E) × (↥J → E))
            (fun (s : ↥I) ↦ x (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inl (↑s : S)) ⋯), fun (t : ↥J) ↦
              x (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inr (↑t : T)) ⋯))
            (fun (s : ↥I) ↦ y (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inl (↑s : S)) ⋯), fun (t : ↥J) ↦
              y (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inr (↑t : T)) ⋯))).1
        x_1
⊢ (fun (s : ↥I) ↦ (x + y) (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inl (↑s : S)) ⋯), fun (t : ↥J) ↦
      (x + y) (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inr (↑t : T)) ⋯)) =
    HAdd.hAdd (α := (↥I → E) × (↥J → E))
      (fun (s : ↥I) ↦ x (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inl (↑s : S)) ⋯), fun (t : ↥J) ↦
        x (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inr (↑t : T)) ⋯))
      (fun (s : ↥I) ↦ y (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inl (↑s : S)) ⋯), fun (t : ↥J) ↦
        y (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inr (↑t : T)) ⋯))
have snd : ∀ (x_1 : ↥J),
  (fun (s : ↥I) ↦ (x + y) (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inl (↑s : S)) sorry), fun (t : ↥J) ↦
          (x + y) (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inr (↑t : T)) sorry)).2
      x_1 =
    (HAdd.hAdd (α := (↥I → E) × (↥J → E))
          (fun (s : ↥I) ↦ x (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inl (↑s : S)) sorry), fun (t : ↥J) ↦
            x (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inr (↑t : T)) sorry))
          (fun (s : ↥I) ↦ y (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inl (↑s : S)) sorry), fun (t : ↥J) ↦
            y (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inr (↑t : T)) sorry))).2
      x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence (goal)
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
inst_4 : CompleteSpace E
S : Type u_4
X : S → Ω → E
Y : T → Ω → E
inst_5 : 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₁ : (a : E) → ℝ) ∘ X s, (⇑L₂ : (a : E) → ℝ) ∘ Y t; P] = 0
this : IsProbabilityMeasure P
I : Finset S
J : Finset T
c : ℝ
x : ↥(I.disjSum J) → E
⊢ (fun (s : ↥I) ↦ (c • x) (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inl (↑s : S)) ⋯), fun (t : ↥J) ↦
      (c • x) (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inr (↑t : T)) ⋯)) =
    HSMul.hSMul (α := ℝ) (β := (↥I → E) × (↥J → E)) ((RingHom.id ℝ : (a : ℝ) → ℝ) c : ℝ)
      (fun (s : ↥I) ↦ x (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inl (↑s : S)) ⋯), fun (t : ↥J) ↦
        x (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inr (↑t : T)) ⋯))
have fst : ∀ (x_1 : ↥I),
  (fun (s : ↥I) ↦ (c • x) (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inl (↑s : S)) sorry), fun (t : ↥J) ↦
          (c • x) (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inr (↑t : T)) sorry)).1
      x_1 =
    (HSMul.hSMul (α := ℝ) (β := (↥I → E) × (↥J → E)) ((RingHom.id ℝ : (a : ℝ) → ℝ) c : ℝ)
          (fun (s : ↥I) ↦ x (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inl (↑s : S)) sorry), fun (t : ↥J) ↦
            x (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inr (↑t : T)) sorry))).1
      x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence (goal)
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
inst_4 : CompleteSpace E
S : Type u_4
X : S → Ω → E
Y : T → Ω → E
inst_5 : 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₁ : (a : E) → ℝ) ∘ X s, (⇑L₂ : (a : E) → ℝ) ∘ Y t; P] = 0
this : IsProbabilityMeasure P
I : Finset S
J : Finset T
c : ℝ
x : ↥(I.disjSum J) → E
fst :
  ∀ (x_1 : ↥I),
    (fun (s : ↥I) ↦ (c • x) (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inl (↑s : S)) ⋯), fun (t : ↥J) ↦
            (c • x) (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inr (↑t : T)) ⋯)).1
        x_1 =
      (HSMul.hSMul (α := ℝ) (β := (↥I → E) × (↥J → E)) ((RingHom.id ℝ : (a : ℝ) → ℝ) c : ℝ)
            (fun (s : ↥I) ↦ x (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inl (↑s : S)) ⋯), fun (t : ↥J) ↦
              x (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inr (↑t : T)) ⋯))).1
        x_1
⊢ (fun (s : ↥I) ↦ (c • x) (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inl (↑s : S)) ⋯), fun (t : ↥J) ↦
      (c • x) (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inr (↑t : T)) ⋯)) =
    HSMul.hSMul (α := ℝ) (β := (↥I → E) × (↥J → E)) ((RingHom.id ℝ : (a : ℝ) → ℝ) c : ℝ)
      (fun (s : ↥I) ↦ x (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inl (↑s : S)) ⋯), fun (t : ↥J) ↦
        x (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inr (↑t : T)) ⋯))
have snd : ∀ (x_1 : ↥J),
  (fun (s : ↥I) ↦ (c • x) (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inl (↑s : S)) sorry), fun (t : ↥J) ↦
          (c • x) (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inr (↑t : T)) sorry)).2
      x_1 =
    (HSMul.hSMul (α := ℝ) (β := (↥I → E) × (↥J → E)) ((RingHom.id ℝ : (a : ℝ) → ℝ) c : ℝ)
          (fun (s : ↥I) ↦ x (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inl (↑s : S)) sorry), fun (t : ↥J) ↦
            x (Subtype.mk (p := fun (x : S ⊕ T) ↦ x ∈ I.disjSum J) (Sum.inr (↑t : T)) sorry))).2
      x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence (goal)
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
inst_4 : CompleteSpace E
S : Type u_4
X : S → Ω → E
Y : T → Ω → E
inst_5 : 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₁ : (a : E) → ℝ) ∘ X s, (⇑L₂ : (a : E) → ℝ) ∘ Y t; P] = 0
this : IsProbabilityMeasure P
I : Finset S
J : Finset T
L₁ : StrongDual ℝ ((i : ↥I) → E)
L₂ : StrongDual ℝ ((j : ↥J) → E)
⊢ Eq.{u_2 + 1} (α := Ω → ℝ)
    (Function.comp (β := (i : ↥I) → E) (⇑L₁ : (a : (i : ↥I) → E) → ℝ) fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω)
    (∑ i : ↥I,
      (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₁
              (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (i : ↥I) ↦ E) i)) :
          (a : E) → ℝ) ∘
        X (↑i : S))
have h₁ : ∀ (x : Ω),
  Eq (α := ℝ) (Function.comp (β := (i : ↥I) → E) (⇑L₁ : (a : (i : ↥I) → E) → ℝ) (fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω) x)
    ((∑ i : ↥I,
        (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₁
                (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (i : ↥I) ↦ E) i)) :
            (a : E) → ℝ) ∘
          X (↑i : S))
      x)
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence (hypothesis)
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
inst_4 : CompleteSpace E
S : Type u_4
X : S → Ω → E
Y : T → Ω → E
inst_5 : 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₁ : (a : E) → ℝ) ∘ X s, (⇑L₂ : (a : E) → ℝ) ∘ Y t; P] = 0
this : IsProbabilityMeasure P
I : Finset S
J : Finset T
L₁ : StrongDual ℝ ((i : ↥I) → E)
L₂ : StrongDual ℝ ((j : ↥J) → E)
⊢ cov[Function.comp (β := (i : ↥I) → E) (⇑L₁ : (a : (i : ↥I) → E) → ℝ) fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω,
      Function.comp (β := (j : ↥J) → E) (⇑L₂ : (a : (j : ↥J) → E) → ℝ) fun (ω : Ω) (j : ↥J) ↦ Y (↑j : T) ω; P] =
    0
have h1 : Eq.{u_2 + 1} (α := Ω → ℝ)
  (Function.comp (β := (i : ↥I) → E) (⇑L₁ : (a : (i : ↥I) → E) → ℝ) fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω)
  (∑ i : ↥I,
    (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₁
            (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (i : ↥I) ↦ E) i)) :
        (a : E) → ℝ) ∘
      X (↑i : S))
Tactic: have h1 : L₁ ∘ (fun ω i ↦ X i ω) = ∑ i : I, (L₁ ∘L .single ℝ _ i) ∘ X i := by
    ext; simp [-ContinuousLinearMap.coe_comp', ← L₁.sum_comp_single]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence (goal)
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
inst_4 : CompleteSpace E
S : Type u_4
X : S → Ω → E
Y : T → Ω → E
inst_5 : 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₁ : (a : E) → ℝ) ∘ X s, (⇑L₂ : (a : E) → ℝ) ∘ Y t; P] = 0
this : IsProbabilityMeasure P
I : Finset S
J : Finset T
L₁ : StrongDual ℝ ((i : ↥I) → E)
L₂ : StrongDual ℝ ((j : ↥J) → E)
h1 :
  Eq.{u_2 + 1} (α := Ω → ℝ)
    (Function.comp (β := (i : ↥I) → E) (⇑L₁ : (a : (i : ↥I) → E) → ℝ) fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω)
    (∑ i : ↥I,
      (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₁
              (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (i : ↥I) ↦ E) i)) :
          (a : E) → ℝ) ∘
        X (↑i : S))
⊢ Eq.{u_2 + 1} (α := Ω → ℝ)
    (Function.comp (β := (j : ↥J) → E) (⇑L₂ : (a : (j : ↥J) → E) → ℝ) fun (ω : Ω) (j : ↥J) ↦ Y (↑j : T) ω)
    (∑ j : ↥J,
      (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₂
              (ContinuousLinearMap.single.{0, u_1, u_3} ℝ (fun (j : ↥J) ↦ E) j)) :
          (a : E) → ℝ) ∘
        Y (↑j : T))
have h₁ : ∀ (x : Ω),
  Eq (α := ℝ) (Function.comp (β := (j : ↥J) → E) (⇑L₂ : (a : (j : ↥J) → E) → ℝ) (fun (ω : Ω) (j : ↥J) ↦ Y (↑j : T) ω) x)
    ((∑ j : ↥J,
        (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₂
                (ContinuousLinearMap.single.{0, u_1, u_3} ℝ (fun (j : ↥J) ↦ E) j)) :
            (a : E) → ℝ) ∘
          Y (↑j : T))
      x)
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence (hypothesis)
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
inst_4 : CompleteSpace E
S : Type u_4
X : S → Ω → E
Y : T → Ω → E
inst_5 : 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₁ : (a : E) → ℝ) ∘ X s, (⇑L₂ : (a : E) → ℝ) ∘ Y t; P] = 0
this : IsProbabilityMeasure P
I : Finset S
J : Finset T
L₁ : StrongDual ℝ ((i : ↥I) → E)
L₂ : StrongDual ℝ ((j : ↥J) → E)
h1 :
  Eq.{u_2 + 1} (α := Ω → ℝ)
    (Function.comp (β := (i : ↥I) → E) (⇑L₁ : (a : (i : ↥I) → E) → ℝ) fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω)
    (∑ i : ↥I,
      (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₁
              (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (i : ↥I) ↦ E) i)) :
          (a : E) → ℝ) ∘
        X (↑i : S))
⊢ cov[Function.comp (β := (i : ↥I) → E) (⇑L₁ : (a : (i : ↥I) → E) → ℝ) fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω,
      Function.comp (β := (j : ↥J) → E) (⇑L₂ : (a : (j : ↥J) → E) → ℝ) fun (ω : Ω) (j : ↥J) ↦ Y (↑j : T) ω; P] =
    0
have h2 : Eq.{u_2 + 1} (α := Ω → ℝ)
  (Function.comp (β := (j : ↥J) → E) (⇑L₂ : (a : (j : ↥J) → E) → ℝ) fun (ω : Ω) (j : ↥J) ↦ Y (↑j : T) ω)
  (∑ j : ↥J,
    (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₂
            (ContinuousLinearMap.single.{0, u_1, u_3} ℝ (fun (j : ↥J) ↦ E) j)) :
        (a : E) → ℝ) ∘
      Y (↑j : T))
Tactic: have h2 : L₂ ∘ (fun ω j ↦ Y j ω) = ∑ j : J, (L₂ ∘L .single ℝ _ j) ∘ Y j := by
    ext; simp [-ContinuousLinearMap.coe_comp', ← L₂.sum_comp_single]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence (goal)
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
inst_4 : CompleteSpace E
S : Type u_4
X : S → Ω → E
Y : T → Ω → E
inst_5 : 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₁ : (a : E) → ℝ) ∘ X s, (⇑L₂ : (a : E) → ℝ) ∘ Y t; P] = 0
this : IsProbabilityMeasure P
I : Finset S
J : Finset T
L₁ : StrongDual ℝ ((i : ↥I) → E)
L₂ : StrongDual ℝ ((j : ↥J) → E)
h1 :
  Eq.{u_2 + 1} (α := Ω → ℝ)
    (Function.comp (β := (i : ↥I) → E) (⇑L₁ : (a : (i : ↥I) → E) → ℝ) fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω)
    (∑ i : ↥I,
      (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₁
              (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (i : ↥I) ↦ E) i)) :
          (a : E) → ℝ) ∘
        X (↑i : S))
h2 :
  Eq.{u_2 + 1} (α := Ω → ℝ)
    (Function.comp (β := (j : ↥J) → E) (⇑L₂ : (a : (j : ↥J) → E) → ℝ) fun (ω : Ω) (j : ↥J) ↦ Y (↑j : T) ω)
    (∑ j : ↥J,
      (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₂
              (ContinuousLinearMap.single.{0, u_1, u_3} ℝ (fun (j : ↥J) ↦ E) j)) :
          (a : E) → ℝ) ∘
        Y (↑j : T))
⊢ cov[Function.comp (β := (i : ↥I) → E) (⇑L₁ : (a : (i : ↥I) → E) → ℝ) fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω,
      Function.comp (β := (j : ↥J) → E) (⇑L₂ : (a : (j : ↥J) → E) → ℝ) fun (ω : Ω) (j : ↥J) ↦ Y (↑j : T) ω; P] =
    0
have refine_2 : Eq (α := ℝ)
  (∑ i : ↥I,
    ∑ j : ↥J,
      cov[(⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₁
                (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (i : ↥I) ↦ E) i)) :
            (a : E) → ℝ) ∘
          X (↑i : S),
        (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₂
                (ContinuousLinearMap.single.{0, u_1, u_3} ℝ (fun (j : ↥J) ↦ E) j)) :
            (a : E) → ℝ) ∘
          Y (↑j : T);
        P])
  0
Tactic: rw [h1, h2, covariance_sum_sum]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence (goal)
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
inst_4 : CompleteSpace E
S : Type u_4
X : S → Ω → E
Y : T → Ω → E
inst_5 : 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₁ : (a : E) → ℝ) ∘ X s, (⇑L₂ : (a : E) → ℝ) ∘ Y t; P] = 0
this : IsProbabilityMeasure P
I : Finset S
J : Finset T
L₁ : StrongDual ℝ ((i : ↥I) → E)
L₂ : StrongDual ℝ ((j : ↥J) → E)
h1 :
  Eq.{u_2 + 1} (α := Ω → ℝ)
    (Function.comp (β := (i : ↥I) → E) (⇑L₁ : (a : (i : ↥I) → E) → ℝ) fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω)
    (∑ i : ↥I,
      (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₁
              (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (i : ↥I) ↦ E) i)) :
          (a : E) → ℝ) ∘
        X (↑i : S))
h2 :
  Eq.{u_2 + 1} (α := Ω → ℝ)
    (Function.comp (β := (j : ↥J) → E) (⇑L₂ : (a : (j : ↥J) → E) → ℝ) fun (ω : Ω) (j : ↥J) ↦ Y (↑j : T) ω)
    (∑ j : ↥J,
      (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₂
              (ContinuousLinearMap.single.{0, u_1, u_3} ℝ (fun (j : ↥J) ↦ E) j)) :
          (a : E) → ℝ) ∘
        Y (↑j : T))
refine_2 :
  Eq (α := ℝ)
    (∑ i : ↥I,
      ∑ j : ↥J,
        cov[(⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₁
                  (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (i : ↥I) ↦ E) i)) :
              (a : E) → ℝ) ∘
            X (↑i : S),
          (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₂
                  (ContinuousLinearMap.single.{0, u_1, u_3} ℝ (fun (j : ↥J) ↦ E) j)) :
              (a : E) → ℝ) ∘
            Y (↑j : T);
          P])
    0
⊢ cov[Function.comp (β := (i : ↥I) → E) (⇑L₁ : (a : (i : ↥I) → E) → ℝ) fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω,
      Function.comp (β := (j : ↥J) → E) (⇑L₂ : (a : (j : ↥J) → E) → ℝ) fun (ω : Ω) (j : ↥J) ↦ Y (↑j : T) ω; P] =
    0
have refine_2₁ : ∀ (i : ↥I),
  MemLp (ε := ℝ)
    ((⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₁
            (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (i : ↥I) ↦ E) i)) :
        (a : E) → ℝ) ∘
      X (↑i : S))
    2 P
Tactic: rw [h1, h2, covariance_sum_sum]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence (goal)
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
inst_4 : CompleteSpace E
S : Type u_4
X : S → Ω → E
Y : T → Ω → E
inst_5 : 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₁ : (a : E) → ℝ) ∘ X s, (⇑L₂ : (a : E) → ℝ) ∘ Y t; P] = 0
this : IsProbabilityMeasure P
I : Finset S
J : Finset T
L₁ : StrongDual ℝ ((i : ↥I) → E)
L₂ : StrongDual ℝ ((j : ↥J) → E)
h1 :
  Eq.{u_2 + 1} (α := Ω → ℝ)
    (Function.comp (β := (i : ↥I) → E) (⇑L₁ : (a : (i : ↥I) → E) → ℝ) fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω)
    (∑ i : ↥I,
      (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₁
              (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (i : ↥I) ↦ E) i)) :
          (a : E) → ℝ) ∘
        X (↑i : S))
h2 :
  Eq.{u_2 + 1} (α := Ω → ℝ)
    (Function.comp (β := (j : ↥J) → E) (⇑L₂ : (a : (j : ↥J) → E) → ℝ) fun (ω : Ω) (j : ↥J) ↦ Y (↑j : T) ω)
    (∑ j : ↥J,
      (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₂
              (ContinuousLinearMap.single.{0, u_1, u_3} ℝ (fun (j : ↥J) ↦ E) j)) :
          (a : E) → ℝ) ∘
        Y (↑j : T))
refine_2 :
  Eq (α := ℝ)
    (∑ i : ↥I,
      ∑ j : ↥J,
        cov[(⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₁
                  (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (i : ↥I) ↦ E) i)) :
              (a : E) → ℝ) ∘
            X (↑i : S),
          (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₂
                  (ContinuousLinearMap.single.{0, u_1, u_3} ℝ (fun (j : ↥J) ↦ E) j)) :
              (a : E) → ℝ) ∘
            Y (↑j : T);
          P])
    0
refine_2₁ :
  ∀ (i : ↥I),
    MemLp (ε := ℝ)
      ((⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₁
              (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (i : ↥I) ↦ E) i)) :
          (a : E) → ℝ) ∘
        X (↑i : S))
      2 P
⊢ cov[Function.comp (β := (i : ↥I) → E) (⇑L₁ : (a : (i : ↥I) → E) → ℝ) fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω,
      Function.comp (β := (j : ↥J) → E) (⇑L₂ : (a : (j : ↥J) → E) → ℝ) fun (ω : Ω) (j : ↥J) ↦ Y (↑j : T) ω; P] =
    0
have refine_2₂ : ∀ (i : ↥J),
  MemLp (ε := ℝ)
    ((⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₂
            (ContinuousLinearMap.single.{0, u_1, u_3} ℝ (fun (j : ↥J) ↦ E) i)) :
        (a : E) → ℝ) ∘
      Y (↑i : T))
    2 P
Tactic: rw [h1, h2, covariance_sum_sum]