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 : T → Type u_4
X : (t : T) → (s : S t) → Ω → E
inst_5 : NormedSpace ℝ E
hX :
  IsGaussianProcess (E := E)
    (fun (p : (t : T) × S t) (ω : Ω) ↦ X (p.fst (β := fun (t : T) ↦ S t)) (p.snd (β := fun (t : T) ↦ S t)) ω) P
mX : ∀ (t : T) (s : S t), AEMeasurable (X t s) P
h :
  ∀ (t₁ t₂ : T),
    t₁ ≠ t₂ →
      ∀ (s₁ : S t₁) (s₂ : S t₂) (L₁ L₂ : StrongDual ℝ E),
        cov[(⇑L₁ : (a : E) → ℝ) ∘ X t₁ s₁, (⇑L₂ : (a : E) → ℝ) ∘ X t₂ s₂; P] = 0
this : IsProbabilityMeasure P
I : Finset T
J : (i : ↥I) → Finset (S (↑i : T))
i j : ↥I
hij : i ≠ j
L₁ : StrongDual ℝ ((j : ↥(J i)) → E)
L₂ : StrongDual ℝ ((j : ↥(J j)) → E)
⊢ Eq.{u_2 + 1} (α := Ω → ℝ)
    (Function.comp (β := (j : ↥(J i)) → E) (⇑L₁ : (a : (j : ↥(J i)) → E) → ℝ) fun (ω : Ω) (k : ↥(J i)) ↦
      X (↑i : T) (↑k : S (↑i : T)) ω)
    (∑ k : ↥(J i),
      (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₁
              (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (j : ↥(J i)) ↦ E) k)) :
          (a : E) → ℝ) ∘
        X (↑i : T) (↑k : S (↑i : T)))
have h₁ : ∀ (x : Ω),
  Eq (α := ℝ)
    (Function.comp (β := (j : ↥(J i)) → E) (⇑L₁ : (a : (j : ↥(J i)) → E) → ℝ)
      (fun (ω : Ω) (k : ↥(J i)) ↦ X (↑i : T) (↑k : S (↑i : T)) ω) x)
    ((∑ k : ↥(J i),
        (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₁
                (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (j : ↥(J i)) ↦ E) k)) :
            (a : E) → ℝ) ∘
          X (↑i : T) (↑k : S (↑i : 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 : T → Type u_4
X : (t : T) → (s : S t) → Ω → E
inst_5 : NormedSpace ℝ E
hX :
  IsGaussianProcess (E := E)
    (fun (p : (t : T) × S t) (ω : Ω) ↦ X (p.fst (β := fun (t : T) ↦ S t)) (p.snd (β := fun (t : T) ↦ S t)) ω) P
mX : ∀ (t : T) (s : S t), AEMeasurable (X t s) P
h :
  ∀ (t₁ t₂ : T),
    t₁ ≠ t₂ →
      ∀ (s₁ : S t₁) (s₂ : S t₂) (L₁ L₂ : StrongDual ℝ E),
        cov[(⇑L₁ : (a : E) → ℝ) ∘ X t₁ s₁, (⇑L₂ : (a : E) → ℝ) ∘ X t₂ s₂; P] = 0
this : IsProbabilityMeasure P
I : Finset T
J : (i : ↥I) → Finset (S (↑i : T))
i j : ↥I
hij : i ≠ j
L₁ : StrongDual ℝ ((j : ↥(J i)) → E)
L₂ : StrongDual ℝ ((j : ↥(J j)) → E)
⊢ cov[Function.comp (β := (j : ↥(J i)) → E) (⇑L₁ : (a : (j : ↥(J i)) → E) → ℝ) fun (ω : Ω) (j : ↥(J i)) ↦
        X (↑i : T) (↑j : S (↑i : T)) ω,
      Function.comp (β := (j : ↥(J j)) → E) (⇑L₂ : (a : (j : ↥(J j)) → E) → ℝ) fun (ω : Ω) (j_1 : ↥(J j)) ↦
        X (↑j : T) (↑j_1 : S (↑j : T)) ω;
      P] =
    0
have h1 : Eq.{u_2 + 1} (α := Ω → ℝ)
  (Function.comp (β := (j : ↥(J i)) → E) (⇑L₁ : (a : (j : ↥(J i)) → E) → ℝ) fun (ω : Ω) (k : ↥(J i)) ↦
    X (↑i : T) (↑k : S (↑i : T)) ω)
  (∑ k : ↥(J i),
    (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₁
            (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (j : ↥(J i)) ↦ E) k)) :
        (a : E) → ℝ) ∘
      X (↑i : T) (↑k : S (↑i : T)))
Tactic: have h1 : L₁ ∘ (fun ω k ↦ X i k ω) = ∑ k : J i, (L₁ ∘L .single ℝ _ k) ∘ X i k := 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 : T → Type u_4
X : (t : T) → (s : S t) → Ω → E
inst_5 : NormedSpace ℝ E
hX :
  IsGaussianProcess (E := E)
    (fun (p : (t : T) × S t) (ω : Ω) ↦ X (p.fst (β := fun (t : T) ↦ S t)) (p.snd (β := fun (t : T) ↦ S t)) ω) P
mX : ∀ (t : T) (s : S t), AEMeasurable (X t s) P
h :
  ∀ (t₁ t₂ : T),
    t₁ ≠ t₂ →
      ∀ (s₁ : S t₁) (s₂ : S t₂) (L₁ L₂ : StrongDual ℝ E),
        cov[(⇑L₁ : (a : E) → ℝ) ∘ X t₁ s₁, (⇑L₂ : (a : E) → ℝ) ∘ X t₂ s₂; P] = 0
this : IsProbabilityMeasure P
I : Finset T
J : (i : ↥I) → Finset (S (↑i : T))
i j : ↥I
hij : i ≠ j
L₁ : StrongDual ℝ ((j : ↥(J i)) → E)
L₂ : StrongDual ℝ ((j : ↥(J j)) → E)
h1 :
  Eq.{u_2 + 1} (α := Ω → ℝ)
    (Function.comp (β := (j : ↥(J i)) → E) (⇑L₁ : (a : (j : ↥(J i)) → E) → ℝ) fun (ω : Ω) (k : ↥(J i)) ↦
      X (↑i : T) (↑k : S (↑i : T)) ω)
    (∑ k : ↥(J i),
      (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₁
              (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (j : ↥(J i)) ↦ E) k)) :
          (a : E) → ℝ) ∘
        X (↑i : T) (↑k : S (↑i : T)))
⊢ Eq.{u_2 + 1} (α := Ω → ℝ)
    (Function.comp (β := (j : ↥(J j)) → E) (⇑L₂ : (a : (j : ↥(J j)) → E) → ℝ) fun (ω : Ω) (k : ↥(J j)) ↦
      X (↑j : T) (↑k : S (↑j : T)) ω)
    (∑ k : ↥(J j),
      (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₂
              (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (j : ↥(J j)) ↦ E) k)) :
          (a : E) → ℝ) ∘
        X (↑j : T) (↑k : S (↑j : T)))
have h₁ : ∀ (x : Ω),
  Eq (α := ℝ)
    (Function.comp (β := (j : ↥(J j)) → E) (⇑L₂ : (a : (j : ↥(J j)) → E) → ℝ)
      (fun (ω : Ω) (k : ↥(J j)) ↦ X (↑j : T) (↑k : S (↑j : T)) ω) x)
    ((∑ k : ↥(J j),
        (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₂
                (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (j : ↥(J j)) ↦ E) k)) :
            (a : E) → ℝ) ∘
          X (↑j : T) (↑k : S (↑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 : T → Type u_4
X : (t : T) → (s : S t) → Ω → E
inst_5 : NormedSpace ℝ E
hX :
  IsGaussianProcess (E := E)
    (fun (p : (t : T) × S t) (ω : Ω) ↦ X (p.fst (β := fun (t : T) ↦ S t)) (p.snd (β := fun (t : T) ↦ S t)) ω) P
mX : ∀ (t : T) (s : S t), AEMeasurable (X t s) P
h :
  ∀ (t₁ t₂ : T),
    t₁ ≠ t₂ →
      ∀ (s₁ : S t₁) (s₂ : S t₂) (L₁ L₂ : StrongDual ℝ E),
        cov[(⇑L₁ : (a : E) → ℝ) ∘ X t₁ s₁, (⇑L₂ : (a : E) → ℝ) ∘ X t₂ s₂; P] = 0
this : IsProbabilityMeasure P
I : Finset T
J : (i : ↥I) → Finset (S (↑i : T))
i j : ↥I
hij : i ≠ j
L₁ : StrongDual ℝ ((j : ↥(J i)) → E)
L₂ : StrongDual ℝ ((j : ↥(J j)) → E)
h1 :
  Eq.{u_2 + 1} (α := Ω → ℝ)
    (Function.comp (β := (j : ↥(J i)) → E) (⇑L₁ : (a : (j : ↥(J i)) → E) → ℝ) fun (ω : Ω) (k : ↥(J i)) ↦
      X (↑i : T) (↑k : S (↑i : T)) ω)
    (∑ k : ↥(J i),
      (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₁
              (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (j : ↥(J i)) ↦ E) k)) :
          (a : E) → ℝ) ∘
        X (↑i : T) (↑k : S (↑i : T)))
⊢ cov[Function.comp (β := (j : ↥(J i)) → E) (⇑L₁ : (a : (j : ↥(J i)) → E) → ℝ) fun (ω : Ω) (j : ↥(J i)) ↦
        X (↑i : T) (↑j : S (↑i : T)) ω,
      Function.comp (β := (j : ↥(J j)) → E) (⇑L₂ : (a : (j : ↥(J j)) → E) → ℝ) fun (ω : Ω) (j_1 : ↥(J j)) ↦
        X (↑j : T) (↑j_1 : S (↑j : T)) ω;
      P] =
    0
have h2 : Eq.{u_2 + 1} (α := Ω → ℝ)
  (Function.comp (β := (j : ↥(J j)) → E) (⇑L₂ : (a : (j : ↥(J j)) → E) → ℝ) fun (ω : Ω) (k : ↥(J j)) ↦
    X (↑j : T) (↑k : S (↑j : T)) ω)
  (∑ k : ↥(J j),
    (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₂
            (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (j : ↥(J j)) ↦ E) k)) :
        (a : E) → ℝ) ∘
      X (↑j : T) (↑k : S (↑j : T)))
Tactic: have h2 : L₂ ∘ (fun ω k ↦ X j k ω) = ∑ k : J j, (L₂ ∘L .single ℝ _ k) ∘ X j k := 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 : T → Type u_4
X : (t : T) → (s : S t) → Ω → E
inst_5 : NormedSpace ℝ E
hX :
  IsGaussianProcess (E := E)
    (fun (p : (t : T) × S t) (ω : Ω) ↦ X (p.fst (β := fun (t : T) ↦ S t)) (p.snd (β := fun (t : T) ↦ S t)) ω) P
mX : ∀ (t : T) (s : S t), AEMeasurable (X t s) P
h :
  ∀ (t₁ t₂ : T),
    t₁ ≠ t₂ →
      ∀ (s₁ : S t₁) (s₂ : S t₂) (L₁ L₂ : StrongDual ℝ E),
        cov[(⇑L₁ : (a : E) → ℝ) ∘ X t₁ s₁, (⇑L₂ : (a : E) → ℝ) ∘ X t₂ s₂; P] = 0
this : IsProbabilityMeasure P
I : Finset T
J : (i : ↥I) → Finset (S (↑i : T))
i j : ↥I
hij : i ≠ j
L₁ : StrongDual ℝ ((j : ↥(J i)) → E)
L₂ : StrongDual ℝ ((j : ↥(J j)) → E)
h1 :
  Eq.{u_2 + 1} (α := Ω → ℝ)
    (Function.comp (β := (j : ↥(J i)) → E) (⇑L₁ : (a : (j : ↥(J i)) → E) → ℝ) fun (ω : Ω) (k : ↥(J i)) ↦
      X (↑i : T) (↑k : S (↑i : T)) ω)
    (∑ k : ↥(J i),
      (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₁
              (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (j : ↥(J i)) ↦ E) k)) :
          (a : E) → ℝ) ∘
        X (↑i : T) (↑k : S (↑i : T)))
h2 :
  Eq.{u_2 + 1} (α := Ω → ℝ)
    (Function.comp (β := (j : ↥(J j)) → E) (⇑L₂ : (a : (j : ↥(J j)) → E) → ℝ) fun (ω : Ω) (k : ↥(J j)) ↦
      X (↑j : T) (↑k : S (↑j : T)) ω)
    (∑ k : ↥(J j),
      (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₂
              (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (j : ↥(J j)) ↦ E) k)) :
          (a : E) → ℝ) ∘
        X (↑j : T) (↑k : S (↑j : T)))
⊢ cov[Function.comp (β := (j : ↥(J i)) → E) (⇑L₁ : (a : (j : ↥(J i)) → E) → ℝ) fun (ω : Ω) (j : ↥(J i)) ↦
        X (↑i : T) (↑j : S (↑i : T)) ω,
      Function.comp (β := (j : ↥(J j)) → E) (⇑L₂ : (a : (j : ↥(J j)) → E) → ℝ) fun (ω : Ω) (j_1 : ↥(J j)) ↦
        X (↑j : T) (↑j_1 : S (↑j : T)) ω;
      P] =
    0
have refine_2 : Eq (α := ℝ)
  (∑ i_1 : ↥(J i),
    ∑ j_1 : ↥(J j),
      cov[(⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₁
                (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (j : ↥(J i)) ↦ E) i_1)) :
            (a : E) → ℝ) ∘
          X (↑i : T) (↑i_1 : S (↑i : T)),
        (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₂
                (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (j : ↥(J j)) ↦ E) j_1)) :
            (a : E) → ℝ) ∘
          X (↑j : T) (↑j_1 : S (↑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 : T → Type u_4
X : (t : T) → (s : S t) → Ω → E
inst_5 : NormedSpace ℝ E
hX :
  IsGaussianProcess (E := E)
    (fun (p : (t : T) × S t) (ω : Ω) ↦ X (p.fst (β := fun (t : T) ↦ S t)) (p.snd (β := fun (t : T) ↦ S t)) ω) P
mX : ∀ (t : T) (s : S t), AEMeasurable (X t s) P
h :
  ∀ (t₁ t₂ : T),
    t₁ ≠ t₂ →
      ∀ (s₁ : S t₁) (s₂ : S t₂) (L₁ L₂ : StrongDual ℝ E),
        cov[(⇑L₁ : (a : E) → ℝ) ∘ X t₁ s₁, (⇑L₂ : (a : E) → ℝ) ∘ X t₂ s₂; P] = 0
this : IsProbabilityMeasure P
I : Finset T
J : (i : ↥I) → Finset (S (↑i : T))
i j : ↥I
hij : i ≠ j
L₁ : StrongDual ℝ ((j : ↥(J i)) → E)
L₂ : StrongDual ℝ ((j : ↥(J j)) → E)
h1 :
  Eq.{u_2 + 1} (α := Ω → ℝ)
    (Function.comp (β := (j : ↥(J i)) → E) (⇑L₁ : (a : (j : ↥(J i)) → E) → ℝ) fun (ω : Ω) (k : ↥(J i)) ↦
      X (↑i : T) (↑k : S (↑i : T)) ω)
    (∑ k : ↥(J i),
      (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₁
              (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (j : ↥(J i)) ↦ E) k)) :
          (a : E) → ℝ) ∘
        X (↑i : T) (↑k : S (↑i : T)))
h2 :
  Eq.{u_2 + 1} (α := Ω → ℝ)
    (Function.comp (β := (j : ↥(J j)) → E) (⇑L₂ : (a : (j : ↥(J j)) → E) → ℝ) fun (ω : Ω) (k : ↥(J j)) ↦
      X (↑j : T) (↑k : S (↑j : T)) ω)
    (∑ k : ↥(J j),
      (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₂
              (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (j : ↥(J j)) ↦ E) k)) :
          (a : E) → ℝ) ∘
        X (↑j : T) (↑k : S (↑j : T)))
refine_2 :
  Eq (α := ℝ)
    (∑ i_1 : ↥(J i),
      ∑ j_1 : ↥(J j),
        cov[(⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₁
                  (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (j : ↥(J i)) ↦ E) i_1)) :
              (a : E) → ℝ) ∘
            X (↑i : T) (↑i_1 : S (↑i : T)),
          (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₂
                  (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (j : ↥(J j)) ↦ E) j_1)) :
              (a : E) → ℝ) ∘
            X (↑j : T) (↑j_1 : S (↑j : T));
          P])
    0
⊢ cov[Function.comp (β := (j : ↥(J i)) → E) (⇑L₁ : (a : (j : ↥(J i)) → E) → ℝ) fun (ω : Ω) (j : ↥(J i)) ↦
        X (↑i : T) (↑j : S (↑i : T)) ω,
      Function.comp (β := (j : ↥(J j)) → E) (⇑L₂ : (a : (j : ↥(J j)) → E) → ℝ) fun (ω : Ω) (j_1 : ↥(J j)) ↦
        X (↑j : T) (↑j_1 : S (↑j : T)) ω;
      P] =
    0
have refine_2₁ : ∀ (i_1 : ↥(J i)),
  MemLp (ε := ℝ)
    ((⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₁
            (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (j : ↥(J i)) ↦ E) i_1)) :
        (a : E) → ℝ) ∘
      X (↑i : T) (↑i_1 : S (↑i : T)))
    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 : T → Type u_4
X : (t : T) → (s : S t) → Ω → E
inst_5 : NormedSpace ℝ E
hX :
  IsGaussianProcess (E := E)
    (fun (p : (t : T) × S t) (ω : Ω) ↦ X (p.fst (β := fun (t : T) ↦ S t)) (p.snd (β := fun (t : T) ↦ S t)) ω) P
mX : ∀ (t : T) (s : S t), AEMeasurable (X t s) P
h :
  ∀ (t₁ t₂ : T),
    t₁ ≠ t₂ →
      ∀ (s₁ : S t₁) (s₂ : S t₂) (L₁ L₂ : StrongDual ℝ E),
        cov[(⇑L₁ : (a : E) → ℝ) ∘ X t₁ s₁, (⇑L₂ : (a : E) → ℝ) ∘ X t₂ s₂; P] = 0
this : IsProbabilityMeasure P
I : Finset T
J : (i : ↥I) → Finset (S (↑i : T))
i j : ↥I
hij : i ≠ j
L₁ : StrongDual ℝ ((j : ↥(J i)) → E)
L₂ : StrongDual ℝ ((j : ↥(J j)) → E)
h1 :
  Eq.{u_2 + 1} (α := Ω → ℝ)
    (Function.comp (β := (j : ↥(J i)) → E) (⇑L₁ : (a : (j : ↥(J i)) → E) → ℝ) fun (ω : Ω) (k : ↥(J i)) ↦
      X (↑i : T) (↑k : S (↑i : T)) ω)
    (∑ k : ↥(J i),
      (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₁
              (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (j : ↥(J i)) ↦ E) k)) :
          (a : E) → ℝ) ∘
        X (↑i : T) (↑k : S (↑i : T)))
h2 :
  Eq.{u_2 + 1} (α := Ω → ℝ)
    (Function.comp (β := (j : ↥(J j)) → E) (⇑L₂ : (a : (j : ↥(J j)) → E) → ℝ) fun (ω : Ω) (k : ↥(J j)) ↦
      X (↑j : T) (↑k : S (↑j : T)) ω)
    (∑ k : ↥(J j),
      (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₂
              (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (j : ↥(J j)) ↦ E) k)) :
          (a : E) → ℝ) ∘
        X (↑j : T) (↑k : S (↑j : T)))
refine_2 :
  Eq (α := ℝ)
    (∑ i_1 : ↥(J i),
      ∑ j_1 : ↥(J j),
        cov[(⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₁
                  (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (j : ↥(J i)) ↦ E) i_1)) :
              (a : E) → ℝ) ∘
            X (↑i : T) (↑i_1 : S (↑i : T)),
          (⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₂
                  (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (j : ↥(J j)) ↦ E) j_1)) :
              (a : E) → ℝ) ∘
            X (↑j : T) (↑j_1 : S (↑j : T));
          P])
    0
refine_2₁ :
  ∀ (i_1 : ↥(J i)),
    MemLp (ε := ℝ)
      ((⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₁
              (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (j : ↥(J i)) ↦ E) i_1)) :
          (a : E) → ℝ) ∘
        X (↑i : T) (↑i_1 : S (↑i : T)))
      2 P
⊢ cov[Function.comp (β := (j : ↥(J i)) → E) (⇑L₁ : (a : (j : ↥(J i)) → E) → ℝ) fun (ω : Ω) (j : ↥(J i)) ↦
        X (↑i : T) (↑j : S (↑i : T)) ω,
      Function.comp (β := (j : ↥(J j)) → E) (⇑L₂ : (a : (j : ↥(J j)) → E) → ℝ) fun (ω : Ω) (j_1 : ↥(J j)) ↦
        X (↑j : T) (↑j_1 : S (↑j : T)) ω;
      P] =
    0
have refine_2₂ : ∀ (i : ↥(J j)),
  MemLp (ε := ℝ)
    ((⇑(ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L₂
            (ContinuousLinearMap.single.{0, u_4, u_3} ℝ (fun (j : ↥(J j)) ↦ E) i)) :
        (a : E) → ℝ) ∘
      X (↑j : T) (↑i : S (↑j : T)))
    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 : T → Type u_4
X : (t : T) → (s : S t) → Ω → E
inst_5 : NormedSpace ℝ E
hX :
  IsGaussianProcess (E := E)
    (fun (p : (t : T) × S t) (ω : Ω) ↦ X (p.fst (β := fun (t : T) ↦ S t)) (p.snd (β := fun (t : T) ↦ S t)) ω) P
mX : ∀ (t : T) (s : S t), AEMeasurable (X t s) P
h :
  ∀ (t₁ t₂ : T),
    t₁ ≠ t₂ →
      ∀ (s₁ : S t₁) (s₂ : S t₂) (L₁ L₂ : StrongDual ℝ E),
        cov[(⇑L₁ : (a : E) → ℝ) ∘ X t₁ s₁, (⇑L₂ : (a : E) → ℝ) ∘ X t₂ s₂; P] = 0
this : IsProbabilityMeasure P
⊢ iIndepFun (β := fun (t : T) ↦ (s : S t) → E) (fun (t : T) (ω : Ω) (s : S t) ↦ X t s ω) P
have refine_1 : ∀ (I : Finset T) (J : (i : ↥I) → Finset (S (↑i : T))),
  HasGaussianLaw (E := (i : ↥I) → (j : ↥(J i)) → E) (fun (ω : Ω) (i : ↥I) (j : ↥(J i)) ↦ X (↑i : T) (↑j : S (↑i : T)) ω)
    P
Tactic: classical
  refine iIndepFun.iIndepFun_process₀ mX fun I J ↦
    HasGaussianLaw.iIndepFun_of_covariance_strongDual ?_ fun i j hij L₁ L₂ ↦ ?_
  · let L : (I.sigma (fun i ↦ if hi : i ∈ I then J ⟨i, hi⟩ else ∅) → E) →L[ℝ] (i : I) → J i → E :=
      { toFun x i j := x ⟨⟨i, j⟩, by simp⟩
        map_add' x y := by ext; simp
        map_smul' c x := by ext; simp }
    exact (hX.hasGaussianLaw _).map L
  have h1 : L₁ ∘ (fun ω k ↦ X i k ω) = ∑ k : J i, (L₁ ∘L .single ℝ _ k) ∘ X i k := by
    ext; simp [-ContinuousLinearMap.coe_comp', ← L₁.sum_comp_single]
  have h2 : L₂ ∘ (fun ω k ↦ X j k ω) = ∑ k : J j, (L₂ ∘L .single ℝ _ k) ∘ X j k := by
    ext; simp [-ContinuousLinearMap.coe_comp', ← L₂.sum_comp_single]
  rw [h1, h2, covariance_sum_sum]
  · exact sum_eq_zero fun _ _ ↦ sum_eq_zero fun _ _ ↦ h i j (by simpa) ..
  · exact fun k ↦ ((hX.hasGaussianLaw_eval ⟨i, k⟩).map _).memLp_two
  · exact fun k ↦ ((hX.hasGaussianLaw_eval ⟨j, k⟩).map _).memLp_two
-- 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 : T → Type u_4
X : (t : T) → (s : S t) → Ω → E
inst_5 : NormedSpace ℝ E
hX :
  IsGaussianProcess (E := E)
    (fun (p : (t : T) × S t) (ω : Ω) ↦ X (p.fst (β := fun (t : T) ↦ S t)) (p.snd (β := fun (t : T) ↦ S t)) ω) P
mX : ∀ (t : T) (s : S t), AEMeasurable (X t s) P
h :
  ∀ (t₁ t₂ : T),
    t₁ ≠ t₂ →
      ∀ (s₁ : S t₁) (s₂ : S t₂) (L₁ L₂ : StrongDual ℝ E),
        cov[(⇑L₁ : (a : E) → ℝ) ∘ X t₁ s₁, (⇑L₂ : (a : E) → ℝ) ∘ X t₂ s₂; P] = 0
this : IsProbabilityMeasure P
refine_1 :
  ∀ (I : Finset T) (J : (i : ↥I) → Finset (S (↑i : T))),
    HasGaussianLaw (E := (i : ↥I) → (j : ↥(J i)) → E)
      (fun (ω : Ω) (i : ↥I) (j : ↥(J i)) ↦ X (↑i : T) (↑j : S (↑i : T)) ω) P
⊢ iIndepFun (β := fun (t : T) ↦ (s : S t) → E) (fun (t : T) (ω : Ω) (s : S t) ↦ X t s ω) P
have refine_2 : ∀ (I : Finset T) (J : (i : ↥I) → Finset (S (↑i : T))) (i j : ↥I) (hij : i ≠ j) (L₁ : StrongDual ℝ ((j : ↥(J i)) → E))
  (L₂ : StrongDual ℝ ((j : ↥(J j)) → E)),
  cov[Function.comp (β := (j : ↥(J i)) → E) (⇑L₁ : (a : (j : ↥(J i)) → E) → ℝ) fun (ω : Ω) (j : ↥(J i)) ↦
        X (↑i : T) (↑j : S (↑i : T)) ω,
      Function.comp (β := (j : ↥(J j)) → E) (⇑L₂ : (a : (j : ↥(J j)) → E) → ℝ) fun (ω : Ω) (j_1 : ↥(J j)) ↦
        X (↑j : T) (↑j_1 : S (↑j : T)) ω;
      P] =
    0
Tactic: classical
  refine iIndepFun.iIndepFun_process₀ mX fun I J ↦
    HasGaussianLaw.iIndepFun_of_covariance_strongDual ?_ fun i j hij L₁ L₂ ↦ ?_
  · let L : (I.sigma (fun i ↦ if hi : i ∈ I then J ⟨i, hi⟩ else ∅) → E) →L[ℝ] (i : I) → J i → E :=
      { toFun x i j := x ⟨⟨i, j⟩, by simp⟩
        map_add' x y := by ext; simp
        map_smul' c x := by ext; simp }
    exact (hX.hasGaussianLaw _).map L
  have h1 : L₁ ∘ (fun ω k ↦ X i k ω) = ∑ k : J i, (L₁ ∘L .single ℝ _ k) ∘ X i k := by
    ext; simp [-ContinuousLinearMap.coe_comp', ← L₁.sum_comp_single]
  have h2 : L₂ ∘ (fun ω k ↦ X j k ω) = ∑ k : J j, (L₂ ∘L .single ℝ _ k) ∘ X j k := by
    ext; simp [-ContinuousLinearMap.coe_comp', ← L₂.sum_comp_single]
  rw [h1, h2, covariance_sum_sum]
  · exact sum_eq_zero fun _ _ ↦ sum_eq_zero fun _ _ ↦ h i j (by simpa) ..
  · exact fun k ↦ ((hX.hasGaussianLaw_eval ⟨i, k⟩).map _).memLp_two
  · exact fun k ↦ ((hX.hasGaussianLaw_eval ⟨j, k⟩).map _).memLp_two
-- 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
⊢ (fun (ω : Ω) (s : S) ↦ X s ω) ⟂ᵢ[P] fun (ω : Ω) (t : T) ↦ Y t ω
have this : IsProbabilityMeasure P
Tactic: have := hXY.isProbabilityMeasure
-- 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
⊢ (fun (ω : Ω) (s : S) ↦ X s ω) ⟂ᵢ[P] fun (ω : Ω) (t : T) ↦ Y t ω
have 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
Tactic: refine IndepFun.process_indepFun_process₀ mX mY fun I J ↦
    HasGaussianLaw.indepFun_of_covariance_strongDual ?_ fun L₁ L₂ ↦ ?_