awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
Goal:
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedSpace ℝ E
inst_4 : SecondCountableTopology E
h : IsGaussianProcess X P
s : Set T
⊢ IsGaussianProcess.{u_3, u_4, u_2} (E := E) (fun (t : (↑s : Type u_2)) ↦ X (↑t : T)) P

Tactic:
h.comp_right Subtype.val

Premises used: ProbabilityTheory.IsGaussianProcess.comp_right, Subtype.val
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence
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
⊢ IsProbabilityMeasure P

Tactic:
have := hX.isProbabilityMeasure
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence
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

Tactic:
iIndepFun.iIndepFun_process₀ mX fun I J ↦
    HasGaussianLaw.iIndepFun_of_covariance_strongDual ?_ fun i j hij L₁ L₂ ↦ ?_

Premises used: ProbabilityTheory.HasGaussianLaw.iIndepFun_of_covariance_strongDual, ProbabilityTheory.iIndepFun.iIndepFun_process₀
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence
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 :
  ∀ (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
⊢ iIndepFun (β := fun (t : T) ↦ (s : S t) → E) (fun (t : T) (ω : Ω) (s : S t) ↦ X t s ω) P

Tactic:
refine iIndepFun.iIndepFun_process₀ mX fun I J ↦
    HasGaussianLaw.iIndepFun_of_covariance_strongDual ?_ fun i j hij L₁ L₂ ↦ ?_

Premises used: ProbabilityTheory.HasGaussianLaw.iIndepFun_of_covariance_strongDual, ProbabilityTheory.iIndepFun.iIndepFun_process₀
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence
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))
x : ↥(I.sigma (α := S) fun (i : T) ↦ if hi : i ∈ I then J (Subtype.mk (p := fun (x : T) ↦ x ∈ I) i hi) else ∅) → E
i : ↥I
j : ↥(J i)
⊢ Membership.mem (γ := Finset ((i : T) × S i))
    (I.sigma (α := S) fun (i : T) ↦ if hi : i ∈ I then J (Subtype.mk (p := fun (x : T) ↦ x ∈ I) i hi) else ∅)
    (Sigma.mk (β := fun (i : T) ↦ S i) (↑i : T) (↑j : S (↑i : T)))

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence
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))
x y : ↥(I.sigma (α := S) fun (i : T) ↦ if hi : i ∈ I then J (Subtype.mk (p := fun (x : T) ↦ x ∈ I) i hi) else ∅) → E
x_1 : ↥I
x_2 : ↥(J x_1)
⊢ (x + y)
      (Subtype.mk (p := fun (x : (i : T) × S i) ↦
        Membership.mem (γ := Finset ((i : T) × S i))
          (I.sigma (α := S) fun (i : T) ↦ if hi : i ∈ I then J (Subtype.mk (p := fun (x : T) ↦ x ∈ I) i hi) else ∅) x)
        (Sigma.mk (β := fun (i : T) ↦ S i) (↑x_1 : T) (↑x_2 : S (↑x_1 : T))) ⋯) =
    HAdd.hAdd (α := (i : ↥I) → ↥(J i) → E) (β := (i : ↥I) → ↥(J i) → E)
      (fun (i : ↥I) (j : ↥(J i)) ↦
        x
          (Subtype.mk (p := fun (x : (i : T) × S i) ↦
            Membership.mem (γ := Finset ((i : T) × S i))
              (I.sigma (α := S) fun (i : T) ↦ if hi : i ∈ I then J (Subtype.mk (p := fun (x : T) ↦ x ∈ I) i hi) else ∅)
              x)
            (Sigma.mk (β := fun (i : T) ↦ S i) (↑i : T) (↑j : S (↑i : T))) ⋯))
      (fun (i : ↥I) (j : ↥(J i)) ↦
        y
          (Subtype.mk (p := fun (x : (i : T) × S i) ↦
            Membership.mem (γ := Finset ((i : T) × S i))
              (I.sigma (α := S) fun (i : T) ↦ if hi : i ∈ I then J (Subtype.mk (p := fun (x : T) ↦ x ∈ I) i hi) else ∅)
              x)
            (Sigma.mk (β := fun (i : T) ↦ S i) (↑i : T) (↑j : S (↑i : T))) ⋯))
      x_1 x_2

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence
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))
c : ℝ
x : ↥(I.sigma (α := S) fun (i : T) ↦ if hi : i ∈ I then J (Subtype.mk (p := fun (x : T) ↦ x ∈ I) i hi) else ∅) → E
h₁ :
  ∀ (x_1 : ↥I) (x_2 : ↥(J x_1)),
    (c • x)
        (Subtype.mk (p := fun (x : (i : T) × S i) ↦
          Membership.mem (γ := Finset ((i : T) × S i))
            (I.sigma (α := S) fun (i : T) ↦ if hi : i ∈ I then J (Subtype.mk (p := fun (x : T) ↦ x ∈ I) i hi) else ∅) x)
          (Sigma.mk (β := fun (i : T) ↦ S i) (↑x_1 : T) (↑x_2 : S (↑x_1 : T))) ⋯) =
      HSMul.hSMul (α := ℝ) (β := (i : ↥I) → ↥(J i) → E) ((RingHom.id ℝ : (a : ℝ) → ℝ) c : ℝ)
        (fun (i : ↥I) (j : ↥(J i)) ↦
          x
            (Subtype.mk (p := fun (x : (i : T) × S i) ↦
              Membership.mem (γ := Finset ((i : T) × S i))
                (I.sigma (α := S) fun (i : T) ↦
                  if hi : i ∈ I then J (Subtype.mk (p := fun (x : T) ↦ x ∈ I) i hi) else ∅)
                x)
              (Sigma.mk (β := fun (i : T) ↦ S i) (↑i : T) (↑j : S (↑i : T))) ⋯))
        x_1 x_2
⊢ (fun (i : ↥I) (j : ↥(J i)) ↦
      (c • x)
        (Subtype.mk (p := fun (x : (i : T) × S i) ↦
          Membership.mem (γ := Finset ((i : T) × S i))
            (I.sigma (α := S) fun (i : T) ↦ if hi : i ∈ I then J (Subtype.mk (p := fun (x : T) ↦ x ∈ I) i hi) else ∅) x)
          (Sigma.mk (β := fun (i : T) ↦ S i) (↑i : T) (↑j : S (↑i : T))) ⋯)) =
    HSMul.hSMul (α := ℝ) (β := (i : ↥I) → ↥(J i) → E) ((RingHom.id ℝ : (a : ℝ) → ℝ) c : ℝ) fun (i : ↥I) (j : ↥(J i)) ↦
      x
        (Subtype.mk (p := fun (x : (i : T) × S i) ↦
          Membership.mem (γ := Finset ((i : T) × S i))
            (I.sigma (α := S) fun (i : T) ↦ if hi : i ∈ I then J (Subtype.mk (p := fun (x : T) ↦ x ∈ I) i hi) else ∅) x)
          (Sigma.mk (β := fun (i : T) ↦ S i) (↑i : T) (↑j : S (↑i : T))) ⋯)

Tactic:
ext
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence
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))
c : ℝ
x : ↥(I.sigma (α := S) fun (i : T) ↦ if hi : i ∈ I then J (Subtype.mk (p := fun (x : T) ↦ x ∈ I) i hi) else ∅) → E
x_1 : ↥I
x_2 : ↥(J x_1)
⊢ (c • x)
      (Subtype.mk (p := fun (x : (i : T) × S i) ↦
        Membership.mem (γ := Finset ((i : T) × S i))
          (I.sigma (α := S) fun (i : T) ↦ if hi : i ∈ I then J (Subtype.mk (p := fun (x : T) ↦ x ∈ I) i hi) else ∅) x)
        (Sigma.mk (β := fun (i : T) ↦ S i) (↑x_1 : T) (↑x_2 : S (↑x_1 : T))) ⋯) =
    HSMul.hSMul (α := ℝ) (β := (i : ↥I) → ↥(J i) → E) ((RingHom.id ℝ : (a : ℝ) → ℝ) c : ℝ)
      (fun (i : ↥I) (j : ↥(J i)) ↦
        x
          (Subtype.mk (p := fun (x : (i : T) × S i) ↦
            Membership.mem (γ := Finset ((i : T) × S i))
              (I.sigma (α := S) fun (i : T) ↦ if hi : i ∈ I then J (Subtype.mk (p := fun (x : T) ↦ x ∈ I) i hi) else ∅)
              x)
            (Sigma.mk (β := fun (i : T) ↦ S i) (↑i : T) (↑j : S (↑i : T))) ⋯))
      x_1 x_2

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence
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))
L : (↥(I.sigma (α := S) fun (i : T) ↦ if hi : i ∈ I then J (Subtype.mk (p := fun (x : T) ↦ x ∈ I) i hi) else ∅) →
    E) →L[ℝ]
  (i : ↥I) → ↥(J i) → E :=
  {
    toFun :=
      fun
        (x :
          ↥(I.sigma (α := S) fun (i : T) ↦ if hi : i ∈ I then J (Subtype.mk (p := fun (x : T) ↦ x ∈ I) i hi) else ∅) →
            E)
        (i : ↥I) (j : ↥(J i)) ↦
      x
        (Subtype.mk (p := fun (x : (i : T) × S i) ↦
          Membership.mem (γ := Finset ((i : T) × S i))
            (I.sigma (α := S) fun (i : T) ↦ if hi : i ∈ I then J (Subtype.mk (p := fun (x : T) ↦ x ∈ I) i hi) else ∅) x)
          (Sigma.mk (β := fun (i : T) ↦ S i) (↑i : T) (↑j : S (↑i : T))) ⋯),
    map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
⊢ HasGaussianLaw (E := (i : ↥I) → (j : ↥(J i)) → E) (fun (ω : Ω) (i : ↥I) (j : ↥(J i)) ↦ X (↑i : T) (↑j : S (↑i : T)) ω)
    P

Tactic:
(hX.hasGaussianLaw _).map L

Premises used: ProbabilityTheory.IsGaussianProcess.hasGaussianLaw, Finset.restrict, ProbabilityTheory.HasGaussianLaw.map
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence
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))
L : (↥(I.sigma (α := S) fun (i : T) ↦ if hi : i ∈ I then J (Subtype.mk (p := fun (x : T) ↦ x ∈ I) i hi) else ∅) →
    E) →L[ℝ]
  (i : ↥I) → ↥(J i) → E :=
  {
    toFun :=
      fun
        (x :
          ↥(I.sigma (α := S) fun (i : T) ↦ if hi : i ∈ I then J (Subtype.mk (p := fun (x : T) ↦ x ∈ I) i hi) else ∅) →
            E)
        (i : ↥I) (j : ↥(J i)) ↦
      x
        (Subtype.mk (p := fun (x : (i : T) × S i) ↦
          Membership.mem (γ := Finset ((i : T) × S i))
            (I.sigma (α := S) fun (i : T) ↦ if hi : i ∈ I then J (Subtype.mk (p := fun (x : T) ↦ x ∈ I) i hi) else ∅) x)
          (Sigma.mk (β := fun (i : T) ↦ S i) (↑i : T) (↑j : S (↑i : T))) ⋯),
    map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
⊢ HasGaussianLaw (E := (i : ↥I) → (j : ↥(J i)) → E) (fun (ω : Ω) (i : ↥I) (j : ↥(J i)) ↦ X (↑i : T) (↑j : S (↑i : T)) ω)
    P

Tactic:
exact (hX.hasGaussianLaw _).map L

Premises used: ProbabilityTheory.IsGaussianProcess.hasGaussianLaw, ProbabilityTheory.HasGaussianLaw.map
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence
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)
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)
⊢ 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:
ext
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence
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)
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:
simp [-ContinuousLinearMap.coe_comp', ← L₁.sum_comp_single]

Premises used: ContinuousLinearMap.sum_comp_single, ContinuousLinearMap.coe_comp'
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence
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)))

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]
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence
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)))
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)
⊢ 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:
ext