awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic (goal)
Goal:
S : Type u_1
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
F : Type u_6
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℝ F
inst_7 : MeasurableSpace F
inst_8 : BorelSpace F
inst_9 : SecondCountableTopology F
Y : S → Ω → F
hX : IsGaussianProcess X P
I : Finset S
J : (s : S) → Finset T
L : (s : S) → (↥(J s) → E) →L[ℝ] F
hL :
  ∀ (s : S) (ω : Ω),
    Y s ω = (L s : (a : ↥(J s) → E) → F) ((J s).restrict (π := fun (x : T) ↦ E) fun (x : T) ↦ X x ω : (i : ↥(J s)) → E)
x y : ↥(I.biUnion J) → E
⊢ (fun (s : ↥I) ↦
      (L (↑s : S) : (a : ↥(J (↑s : S)) → E) → F) fun (t : ↥(J (↑s : S))) ↦
        (x + y) (Subtype.mk (p := fun (x : T) ↦ x ∈ I.biUnion J) (↑t : T) ⋯)) =
    HAdd.hAdd (α := ↥I → F)
      (fun (s : ↥I) ↦
        (L (↑s : S) : (a : ↥(J (↑s : S)) → E) → F) fun (t : ↥(J (↑s : S))) ↦
          x (Subtype.mk (p := fun (x : T) ↦ x ∈ I.biUnion J) (↑t : T) ⋯))
      fun (s : ↥I) ↦
      (L (↑s : S) : (a : ↥(J (↑s : S)) → E) → F) fun (t : ↥(J (↑s : S))) ↦
        y (Subtype.mk (p := fun (x : T) ↦ x ∈ I.biUnion J) (↑t : T) ⋯)
have h : ∀ (x_1 : ↥I),
  ((L (↑x_1 : S) : (a : ↥(J (↑x_1 : S)) → E) → F) fun (t : ↥(J (↑x_1 : S))) ↦
      (x + y) (Subtype.mk (p := fun (x : T) ↦ x ∈ I.biUnion J) (↑t : T) sorry)) =
    HAdd.hAdd (α := ↥I → F) (β := ↥I → F)
      (fun (s : ↥I) ↦
        (L (↑s : S) : (a : ↥(J (↑s : S)) → E) → F) fun (t : ↥(J (↑s : S))) ↦
          x (Subtype.mk (p := fun (x : T) ↦ x ∈ I.biUnion J) (↑t : T) sorry))
      (fun (s : ↥I) ↦
        (L (↑s : S) : (a : ↥(J (↑s : S)) → E) → F) fun (t : ↥(J (↑s : S))) ↦
          y (Subtype.mk (p := fun (x : T) ↦ x ∈ I.biUnion J) (↑t : T) sorry))
      x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic (goal)
Goal:
S : Type u_1
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
F : Type u_6
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℝ F
inst_7 : MeasurableSpace F
inst_8 : BorelSpace F
inst_9 : SecondCountableTopology F
Y : S → Ω → F
hX : IsGaussianProcess X P
I : Finset S
J : (s : S) → Finset T
L : (s : S) → (↥(J s) → E) →L[ℝ] F
hL :
  ∀ (s : S) (ω : Ω),
    Y s ω = (L s : (a : ↥(J s) → E) → F) ((J s).restrict (π := fun (x : T) ↦ E) fun (x : T) ↦ X x ω : (i : ↥(J s)) → E)
c : ℝ
x : ↥(I.biUnion J) → E
⊢ (fun (s : ↥I) ↦
      (L (↑s : S) : (a : ↥(J (↑s : S)) → E) → F) fun (t : ↥(J (↑s : S))) ↦
        (c • x) (Subtype.mk (p := fun (x : T) ↦ x ∈ I.biUnion J) (↑t : T) ⋯)) =
    HSMul.hSMul (α := ℝ) (β := ↥I → F) ((RingHom.id ℝ : (a : ℝ) → ℝ) c : ℝ) fun (s : ↥I) ↦
      (L (↑s : S) : (a : ↥(J (↑s : S)) → E) → F) fun (t : ↥(J (↑s : S))) ↦
        x (Subtype.mk (p := fun (x : T) ↦ x ∈ I.biUnion J) (↑t : T) ⋯)
have h : ∀ (x_1 : ↥I),
  ((L (↑x_1 : S) : (a : ↥(J (↑x_1 : S)) → E) → F) fun (t : ↥(J (↑x_1 : S))) ↦
      (c • x) (Subtype.mk (p := fun (x : T) ↦ x ∈ I.biUnion J) (↑t : T) sorry)) =
    HSMul.hSMul (α := ℝ) (β := ↥I → F) ((RingHom.id ℝ : (a : ℝ) → ℝ) c : ℝ)
      (fun (s : ↥I) ↦
        (L (↑s : S) : (a : ↥(J (↑s : S)) → E) → F) fun (t : ↥(J (↑s : S))) ↦
          x (Subtype.mk (p := fun (x : T) ↦ x ∈ I.biUnion J) (↑t : T) sorry))
      x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic (goal)
Goal:
S : Type u_1
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
F : Type u_6
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℝ F
inst_7 : MeasurableSpace F
inst_8 : BorelSpace F
inst_9 : SecondCountableTopology F
Y : S → Ω → F
hX : IsGaussianProcess X P
I : Finset S
J : (s : S) → Finset T
L : (s : S) → (↥(J s) → E) →L[ℝ] F
hL :
  ∀ (s : S) (ω : Ω),
    Y s ω = (L s : (a : ↥(J s) → E) → F) ((J s).restrict (π := fun (x : T) ↦ E) fun (x : T) ↦ X x ω : (i : ↥(J s)) → E)
K : (↥(I.biUnion J) → E) →L[ℝ] ↥I → F :=
  {
    toFun := fun (x : ↥(I.biUnion J) → E) (s : ↥I) ↦
      (L (↑s : S) : (a : ↥(J (↑s : S)) → E) → F) fun (t : ↥(J (↑s : S))) ↦
        x (Subtype.mk (p := fun (x : T) ↦ x ∈ I.biUnion J) (↑t : T) ⋯),
    map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
⊢ Eq (α := (ω : Ω) → (i : ↥I) → F) (fun (ω : Ω) ↦ I.restrict (π := fun (x : S) ↦ F) fun (x : S) ↦ Y x ω)
    (Function.comp (β := ↥(I.biUnion J) → E) (⇑K : (a : ↥(I.biUnion J) → E) → ↥I → F) fun (ω : Ω) ↦
      (I.biUnion J).restrict (π := fun (x : T) ↦ E) fun (x : T) ↦ X x ω)
have h : ∀ (x : Ω) (x_1 : ↥I),
  Eq.{u_6 + 1} (α := F) (I.restrict (π := fun (x : S) ↦ F) (fun (x_2 : S) ↦ Y x_2 x) x_1 : F)
    (Function.comp (β := ↥(I.biUnion J) → E) (⇑K : (a : ↥(I.biUnion J) → E) → ↥I → F)
        (fun (ω : Ω) ↦ (I.biUnion J).restrict (π := fun (x : T) ↦ E) fun (x : T) ↦ X x ω) x x_1 :
      F)
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic (hypothesis)
Goal:
S : Type u_1
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
F : Type u_6
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℝ F
inst_7 : MeasurableSpace F
inst_8 : BorelSpace F
inst_9 : SecondCountableTopology F
Y : S → Ω → F
hX : IsGaussianProcess X P
I : Finset S
J : (s : S) → Finset T
L : (s : S) → (↥(J s) → E) →L[ℝ] F
hL :
  ∀ (s : S) (ω : Ω),
    Y s ω = (L s : (a : ↥(J s) → E) → F) ((J s).restrict (π := fun (x : T) ↦ E) fun (x : T) ↦ X x ω : (i : ↥(J s)) → E)
K : (↥(I.biUnion J) → E) →L[ℝ] ↥I → F :=
  {
    toFun := fun (x : ↥(I.biUnion J) → E) (s : ↥I) ↦
      (L (↑s : S) : (a : ↥(J (↑s : S)) → E) → F) fun (t : ↥(J (↑s : S))) ↦
        x (Subtype.mk (p := fun (x : T) ↦ x ∈ I.biUnion J) (↑t : T) ⋯),
    map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
⊢ HasGaussianLaw (E := (i : ↥I) → F) (fun (ω : Ω) ↦ I.restrict (π := fun (x : S) ↦ F) fun (x : S) ↦ Y x ω) P
have this : Eq (α := (ω : Ω) → (i : ↥I) → F) (fun (ω : Ω) ↦ I.restrict (π := fun (x : S) ↦ F) fun (x : S) ↦ Y x ω)
  (Function.comp (β := ↥(I.biUnion J) → E) (⇑K : (a : ↥(I.biUnion J) → E) → ↥I → F) fun (ω : Ω) ↦
    (I.biUnion J).restrict (π := fun (x : T) ↦ E) fun (x : T) ↦ X x ω)
Tactic: have : (fun ω ↦ I.restrict (Y · ω)) = K ∘ (fun ω ↦ (I.biUnion J).restrict (X · ω)) := by
      ext; simp [K, hL, Finset.restrict_def]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic (goal)
Goal:
S : Type u_1
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
F : Type u_6
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℝ F
inst_7 : MeasurableSpace F
inst_8 : BorelSpace F
inst_9 : SecondCountableTopology F
Y : S → Ω → F
hX : IsGaussianProcess X P
I : Finset S
J : (s : S) → Finset T
L : (s : S) → (↥(J s) → E) →L[ℝ] F
hL :
  ∀ (s : S) (ω : Ω),
    Y s ω = (L s : (a : ↥(J s) → E) → F) ((J s).restrict (π := fun (x : T) ↦ E) fun (x : T) ↦ X x ω : (i : ↥(J s)) → E)
K : (↥(I.biUnion J) → E) →L[ℝ] ↥I → F :=
  {
    toFun := fun (x : ↥(I.biUnion J) → E) (s : ↥I) ↦
      (L (↑s : S) : (a : ↥(J (↑s : S)) → E) → F) fun (t : ↥(J (↑s : S))) ↦
        x (Subtype.mk (p := fun (x : T) ↦ x ∈ I.biUnion J) (↑t : T) ⋯),
    map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
this :
  Eq (α := (ω : Ω) → (i : ↥I) → F) (fun (ω : Ω) ↦ I.restrict (π := fun (x : S) ↦ F) fun (x : S) ↦ Y x ω)
    (Function.comp (β := ↥(I.biUnion J) → E) (⇑K : (a : ↥(I.biUnion J) → E) → ↥I → F) fun (ω : Ω) ↦
      (I.biUnion J).restrict (π := fun (x : T) ↦ E) fun (x : T) ↦ X x ω)
⊢ HasGaussianLaw (E := (i : ↥I) → F) (fun (ω : Ω) ↦ I.restrict (π := fun (x : S) ↦ F) fun (x : S) ↦ Y x ω) P
have rw : HasGaussianLaw (E := (i : ↥I) → F)
  (Function.comp (β := ↥(I.biUnion J) → E) (⇑K : (a : ↥(I.biUnion J) → E) → ↥I → F) fun (ω : Ω) ↦
    (I.biUnion J).restrict (π := fun (x : T) ↦ E) fun (x : T) ↦ X x ω)
  P
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic (goal)
Goal:
S : Type u_1
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
F : Type u_6
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℝ F
inst_7 : MeasurableSpace F
inst_8 : BorelSpace F
inst_9 : SecondCountableTopology F
Y : S → Ω → F
hX : IsGaussianProcess X P
I : Finset S
J : (s : S) → Finset T
L : (s : S) → (↥(J s) → E) →L[ℝ] F
hL :
  ∀ (s : S) (ω : Ω),
    Y s ω = (L s : (a : ↥(J s) → E) → F) ((J s).restrict (π := fun (x : T) ↦ E) fun (x : T) ↦ X x ω : (i : ↥(J s)) → E)
let let₁ let₂ :
  HasGaussianLaw (E := (i : ↥I) → F) (fun (ω : Ω) ↦ I.restrict (π := fun (x : S) ↦ F) fun (x : S) ↦ Y x ω) P
⊢ HasGaussianLaw (E := (i : ↥I) → F) (fun (ω : Ω) ↦ I.restrict (π := fun (x : S) ↦ F) fun (x : S) ↦ Y x ω) P
have let₃ : let K : (↥(I.biUnion J) → E) →L[ℝ] ↥I → F :=
  {
    toFun := fun (x : ↥(I.biUnion J) → E) (s : ↥I) ↦
      (L (↑s : S) : (a : ↥(J (↑s : S)) → E) → F) fun (t : ↥(J (↑s : S))) ↦
        x (Subtype.mk (p := fun (x : T) ↦ x ∈ I.biUnion J) (↑t : T) sorry),
    map_add' := sorry, map_smul' := sorry, cont := sorry };
∀
  (this :
    Eq (α := (ω : Ω) → (i : ↥I) → F) (fun (ω : Ω) ↦ I.restrict (π := fun (x : S) ↦ F) fun (x : S) ↦ Y x ω)
      (Function.comp (β := ↥(I.biUnion J) → E) (⇑K : (a : ↥(I.biUnion J) → E) → ↥I → F) fun (ω : Ω) ↦
        (I.biUnion J).restrict (π := fun (x : T) ↦ E) fun (x : T) ↦ X x ω)),
  HasGaussianLaw (E := (i : ↥I) → F) (fun (ω : Ω) ↦ I.restrict (π := fun (x : S) ↦ F) fun (x : S) ↦ Y x ω) P
Tactic: classical
    let K : (I.biUnion J → E) →L[ℝ] I → F :=
      { toFun x s := L s (fun t ↦ x ⟨t.1, mem_biUnion.2 ⟨s.1, s.2, t.2⟩⟩)
        map_add' x y := by ext; simp [← Pi.add_def]
        map_smul' c x := by ext; simp [← Pi.smul_def] }
    have : (fun ω ↦ I.restrict (Y · ω)) = K ∘ (fun ω ↦ (I.biUnion J).restrict (X · ω)) := by
      ext; simp [K, hL, Finset.restrict_def]
    rw [this]
    exact (hX.hasGaussianLaw _).map _
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic (goal)
Goal:
S : Type u_1
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
F : Type u_6
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℝ F
inst_7 : MeasurableSpace F
inst_8 : BorelSpace F
inst_9 : SecondCountableTopology F
Y : S → Ω → F
hX : IsGaussianProcess X P
I : Finset S
J : (s : S) → Finset T
L : (s : S) → (↥(J s) → E) →L[ℝ] F
hL :
  ∀ (s : S) (ω : Ω),
    Y s ω = (L s : (a : ↥(J s) → E) → F) ((J s).restrict (π := fun (x : T) ↦ E) fun (x : T) ↦ X x ω : (i : ↥(J s)) → E)
let let₁ let₂ :
  HasGaussianLaw (E := (i : ↥I) → F) (fun (ω : Ω) ↦ I.restrict (π := fun (x : S) ↦ F) fun (x : S) ↦ Y x ω) P
let₃ :
  let K : (↥(I.biUnion J) → E) →L[ℝ] ↥I → F :=
    {
      toFun := fun (x : ↥(I.biUnion J) → E) (s : ↥I) ↦
        (L (↑s : S) : (a : ↥(J (↑s : S)) → E) → F) fun (t : ↥(J (↑s : S))) ↦
          x (Subtype.mk (p := fun (x : T) ↦ x ∈ I.biUnion J) (↑t : T) ⋯),
      map_add' := ⋯, map_smul' := ⋯, cont := ⋯ };
  ∀
    (this :
      Eq (α := (ω : Ω) → (i : ↥I) → F) (fun (ω : Ω) ↦ I.restrict (π := fun (x : S) ↦ F) fun (x : S) ↦ Y x ω)
        (Function.comp (β := ↥(I.biUnion J) → E) (⇑K : (a : ↥(I.biUnion J) → E) → ↥I → F) fun (ω : Ω) ↦
          (I.biUnion J).restrict (π := fun (x : T) ↦ E) fun (x : T) ↦ X x ω)),
    HasGaussianLaw (E := (i : ↥I) → F) (fun (ω : Ω) ↦ I.restrict (π := fun (x : S) ↦ F) fun (x : S) ↦ Y x ω) P
⊢ HasGaussianLaw (E := (i : ↥I) → F) (fun (ω : Ω) ↦ I.restrict (π := fun (x : S) ↦ F) fun (x : S) ↦ Y x ω) P
have let₄ : let K : (↥(I.biUnion J) → E) →L[ℝ] ↥I → F :=
  {
    toFun := fun (x : ↥(I.biUnion J) → E) (s : ↥I) ↦
      (L (↑s : S) : (a : ↥(J (↑s : S)) → E) → F) fun (t : ↥(J (↑s : S))) ↦
        x (Subtype.mk (p := fun (x : T) ↦ x ∈ I.biUnion J) (↑t : T) sorry),
    map_add' := sorry, map_smul' := sorry, cont := sorry };
∀
  (this :
    Eq (α := (ω : Ω) → (i : ↥I) → F) (fun (ω : Ω) ↦ I.restrict (π := fun (x : S) ↦ F) fun (x : S) ↦ Y x ω)
      (Function.comp (β := ↥(I.biUnion J) → E) (⇑K : (a : ↥(I.biUnion J) → E) → ↥I → F) fun (ω : Ω) ↦
        (I.biUnion J).restrict (π := fun (x : T) ↦ E) fun (x : T) ↦ X x ω)),
  HasGaussianLaw (E := (i : ↥I) → F)
    (Function.comp (β := ↥(I.biUnion J) → E) (⇑K : (a : ↥(I.biUnion J) → E) → ↥I → F) fun (ω : Ω) ↦
      (I.biUnion J).restrict (π := fun (x : T) ↦ E) fun (x : T) ↦ X x ω)
    P
Tactic: classical
    let K : (I.biUnion J → E) →L[ℝ] I → F :=
      { toFun x s := L s (fun t ↦ x ⟨t.1, mem_biUnion.2 ⟨s.1, s.2, t.2⟩⟩)
        map_add' x y := by ext; simp [← Pi.add_def]
        map_smul' c x := by ext; simp [← Pi.smul_def] }
    have : (fun ω ↦ I.restrict (Y · ω)) = K ∘ (fun ω ↦ (I.biUnion J).restrict (X · ω)) := by
      ext; simp [K, hL, Finset.restrict_def]
    rw [this]
    exact (hX.hasGaussianLaw _).map _
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic (goal)
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
inst_5 : Add T
h : IsGaussianProcess X P
t₀ t : T
x y : ↥{t₀, t₀ + t} → E
⊢ (x + y) (Subtype.mk (p := fun (x : T) ↦ Membership.mem (γ := Finset T) {t₀, t₀ + t} x) (t₀ + t) ⋯) -
      (x + y) (Subtype.mk (p := fun (x : T) ↦ Membership.mem (γ := Finset T) {t₀, t₀ + t} x) t₀ ⋯) =
    x (Subtype.mk (p := fun (x : T) ↦ Membership.mem (γ := Finset T) {t₀, t₀ + t} x) (t₀ + t) ⋯) -
        x (Subtype.mk (p := fun (x : T) ↦ Membership.mem (γ := Finset T) {t₀, t₀ + t} x) t₀ ⋯) +
      (y (Subtype.mk (p := fun (x : T) ↦ Membership.mem (γ := Finset T) {t₀, t₀ + t} x) (t₀ + t) ⋯) -
        y (Subtype.mk (p := fun (x : T) ↦ Membership.mem (γ := Finset T) {t₀, t₀ + t} x) t₀ ⋯))
have simp : x (Subtype.mk (p := fun (x : T) ↦ Membership.mem (γ := Finset T) {t₀, t₀ + t} x) (t₀ + t) sorry) +
      y (Subtype.mk (p := fun (x : T) ↦ Membership.mem (γ := Finset T) {t₀, t₀ + t} x) (t₀ + t) sorry) -
    (x (Subtype.mk (p := fun (x : T) ↦ Membership.mem (γ := Finset T) {t₀, t₀ + t} x) t₀ sorry) +
      y (Subtype.mk (p := fun (x : T) ↦ Membership.mem (γ := Finset T) {t₀, t₀ + t} x) t₀ sorry)) =
  x (Subtype.mk (p := fun (x : T) ↦ Membership.mem (γ := Finset T) {t₀, t₀ + t} x) (t₀ + t) sorry) -
      x (Subtype.mk (p := fun (x : T) ↦ Membership.mem (γ := Finset T) {t₀, t₀ + t} x) t₀ sorry) +
    (y (Subtype.mk (p := fun (x : T) ↦ Membership.mem (γ := Finset T) {t₀, t₀ + t} x) (t₀ + t) sorry) -
      y (Subtype.mk (p := fun (x : T) ↦ Membership.mem (γ := Finset T) {t₀, t₀ + t} x) t₀ sorry))
Tactic: simp
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic (goal)
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
inst_5 : Add T
h : IsGaussianProcess X P
t₀ t : T
c : ℝ
x : ↥{t₀, t₀ + t} → E
⊢ (c • x) (Subtype.mk (p := fun (x : T) ↦ Membership.mem (γ := Finset T) {t₀, t₀ + t} x) (t₀ + t) ⋯) -
      (c • x) (Subtype.mk (p := fun (x : T) ↦ Membership.mem (γ := Finset T) {t₀, t₀ + t} x) t₀ ⋯) =
    HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) c : ℝ)
      (x (Subtype.mk (p := fun (x : T) ↦ Membership.mem (γ := Finset T) {t₀, t₀ + t} x) (t₀ + t) ⋯) -
        x (Subtype.mk (p := fun (x : T) ↦ Membership.mem (γ := Finset T) {t₀, t₀ + t} x) t₀ ⋯))
have simp : c • x (Subtype.mk (p := fun (x : T) ↦ Membership.mem (γ := Finset T) {t₀, t₀ + t} x) (t₀ + t) sorry) -
    c • x (Subtype.mk (p := fun (x : T) ↦ Membership.mem (γ := Finset T) {t₀, t₀ + t} x) t₀ sorry) =
  c •
    (x (Subtype.mk (p := fun (x : T) ↦ Membership.mem (γ := Finset T) {t₀, t₀ + t} x) (t₀ + t) sorry) -
      x (Subtype.mk (p := fun (x : T) ↦ Membership.mem (γ := Finset T) {t₀, t₀ + t} x) t₀ sorry))
Tactic: simp
-- 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
⊢ iIndepFun (β := fun (t : T) ↦ (s : S t) → E) (fun (t : T) (ω : Ω) (s : S t) ↦ X t s ω) P
have this : IsProbabilityMeasure P
Tactic: have := hX.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 : 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: refine iIndepFun.iIndepFun_process₀ mX fun I J ↦
    HasGaussianLaw.iIndepFun_of_covariance_strongDual ?_ fun i j hij 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 : 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: refine iIndepFun.iIndepFun_process₀ mX fun I J ↦
    HasGaussianLaw.iIndepFun_of_covariance_strongDual ?_ fun i j hij 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 : 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
⊢ (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))) ⋯)
have 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))) sorry) =
    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))) sorry))
      x_1 x_2
Tactic: ext