awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)))
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:
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)
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)))

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]
-- 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)))
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)))
x : ↥(J i)
h_1 : Membership.mem (γ := Finset ↥(J i)) univ x
x_1 : ↥(J j)
h_2 : Membership.mem (γ := Finset ↥(J j)) univ x_1
⊢ (↑i : T) ≠ (↑j : T)

Tactic:
simpa
-- 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)))
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

Tactic:
exact sum_eq_zero fun _ _ ↦ sum_eq_zero fun _ _ ↦ h i j (by simpa) ..

Premises used: Finset.sum_eq_zero, 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
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)))
⊢ ∀ (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:
fun k ↦ ((hX.hasGaussianLaw_eval ⟨i, k⟩).map _).memLp_two

Premises used: ContinuousLinearMap.comp, ContinuousLinearMap.single, Real, ProbabilityTheory.HasGaussianLaw.map, ProbabilityTheory.IsGaussianProcess.hasGaussianLaw_eval, Sigma.mk, Subtype.val, ProbabilityTheory.HasGaussianLaw.memLp_two
-- 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)))
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:
exact fun k ↦ ((hX.hasGaussianLaw_eval ⟨i, k⟩).map _).memLp_two

Premises used: ProbabilityTheory.HasGaussianLaw.map, ProbabilityTheory.IsGaussianProcess.hasGaussianLaw_eval, Sigma.mk, Subtype.val, ProbabilityTheory.HasGaussianLaw.memLp_two
-- 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)))
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 : ↥(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:
fun k ↦ ((hX.hasGaussianLaw_eval ⟨j, k⟩).map _).memLp_two

Premises used: ContinuousLinearMap.comp, ContinuousLinearMap.single, Real, ProbabilityTheory.HasGaussianLaw.map, ProbabilityTheory.IsGaussianProcess.hasGaussianLaw_eval, Sigma.mk, Subtype.val, ProbabilityTheory.HasGaussianLaw.memLp_two
-- 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)))
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 : ↥(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:
exact fun k ↦ ((hX.hasGaussianLaw_eval ⟨j, k⟩).map _).memLp_two

Premises used: ProbabilityTheory.HasGaussianLaw.map, ProbabilityTheory.IsGaussianProcess.hasGaussianLaw_eval, Sigma.mk, Subtype.val, ProbabilityTheory.HasGaussianLaw.memLp_two
-- 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 : InnerProductSpace ℝ 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₂) (x y : E), cov[fun (ω : Ω) ↦ ⟪x, X t₁ s₁ ω⟫, fun (ω : Ω) ↦ ⟪y, X t₂ s₂ ω⟫; P] = 0
t₁ t₂ : T
ht : 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

Tactic:
simpa using h t₁ t₂ ht s₁ s₂ ((toDual ℝ E).symm L₁) ((toDual ℝ E).symm L₂)

Premises used: InnerProductSpace.toDual, Real, LinearIsometryEquiv.symm, DFunLike.coe
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence
Goal:
T : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
S : T → Type u_4
X : (t : T) → (s : S t) → Ω → ℝ
hX :
  IsGaussianProcess (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₂), cov[X t₁ s₁, X t₂ s₂; P] = 0
x x_1 : T
h' : x ≠ x_1
x_2 : S x
x_3 : S x_1
x_4 x_5 : ℝ
⊢ cov[fun (ω : Ω) ↦ ⟪x_4, X x x_2 ω⟫, fun (ω : Ω) ↦ ⟪x_5, X x_1 x_3 ω⟫; P] = 0

Tactic:
simp [covariance_mul_const_left, covariance_mul_const_right, h _ _ h']

Premises used: ProbabilityTheory.covariance_mul_const_left, ProbabilityTheory.covariance_mul_const_right
-- 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 : 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
⊢ IsProbabilityMeasure P

Tactic:
have := hXY.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 : 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 ω

Tactic:
IndepFun.process_indepFun_process₀ mX mY fun I J ↦
    HasGaussianLaw.indepFun_of_covariance_strongDual ?_ fun L₁ L₂ ↦ ?_

Premises used: ProbabilityTheory.HasGaussianLaw.indepFun_of_covariance_strongDual, ProbabilityTheory.IndepFun.process_indepFun_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 : 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
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
⊢ (fun (ω : Ω) (s : S) ↦ X s ω) ⟂ᵢ[P] fun (ω : Ω) (t : T) ↦ Y t ω

Tactic:
refine IndepFun.process_indepFun_process₀ mX mY fun I J ↦
    HasGaussianLaw.indepFun_of_covariance_strongDual ?_ fun L₁ L₂ ↦ ?_

Premises used: ProbabilityTheory.HasGaussianLaw.indepFun_of_covariance_strongDual, ProbabilityTheory.IndepFun.process_indepFun_process₀