-- 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
refine_2 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
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))
    (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
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))
    (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
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))
    (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)))),
    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
⊢ 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))
  (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))))
  (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: 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