awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
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 ω)

Tactic:
have : (fun ω ↦ I.restrict (Y · ω)) = K ∘ (fun ω ↦ (I.biUnion J).restrict (X · ω)) := by
      ext; simp [K, hL, Finset.restrict_def]
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
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 ω)
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
⊢ HasGaussianLaw (E := (i : ↥I) → F) (fun (ω : Ω) ↦ I.restrict (π := fun (x : S) ↦ F) fun (x : S) ↦ Y x ω) P

Tactic:
rw [this]
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
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)
    (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:
(hX.hasGaussianLaw _).map _

Premises used: ProbabilityTheory.IsGaussianProcess.hasGaussianLaw, ProbabilityTheory.HasGaussianLaw.map
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
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)
    (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:
exact (hX.hasGaussianLaw _).map _

Premises used: ProbabilityTheory.IsGaussianProcess.hasGaussianLaw, ProbabilityTheory.HasGaussianLaw.map
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
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
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)
      (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
⊢ 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 _

Premises used: ProbabilityTheory.IsGaussianProcess.hasGaussianLaw, ProbabilityTheory.HasGaussianLaw.map
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
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
h : IsGaussianProcess X P
f : S → T
s : S
x : ↥{f s} → E
⊢ Membership.mem (γ := Finset T) {f s} (f s)

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
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
h : IsGaussianProcess X P
f : S → T
s : S
⊢ ∀ (x y : ↥{f s} → E),
    (x + y) (Subtype.mk (p := fun (x : T) ↦ Membership.mem (γ := Finset T) {f s} x) (f s) ⋯) =
      x (Subtype.mk (p := fun (x : T) ↦ Membership.mem (γ := Finset T) {f s} x) (f s) ⋯) +
        y (Subtype.mk (p := fun (x : T) ↦ Membership.mem (γ := Finset T) {f s} x) (f s) ⋯)

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
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
h : IsGaussianProcess X P
f : S → T
s : S
⊢ ∀ (m : ℝ) (x : ↥{f s} → E),
    (m • x) (Subtype.mk (p := fun (x : T) ↦ Membership.mem (γ := Finset T) {f s} x) (f s) ⋯) =
      HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) m : ℝ)
        (x (Subtype.mk (p := fun (x : T) ↦ Membership.mem (γ := Finset T) {f s} x) (f s) ⋯))

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
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
h : IsGaussianProcess X P
f : S → T
s : S
⊢ ∀ (ω : Ω),
    (X ∘ f) s ω =
      ({
            toFun := fun (x : ↥{f s} → E) ↦
              x (Subtype.mk (p := fun (x : T) ↦ Membership.mem (γ := Finset T) {f s} x) (f s) ⋯),
            map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } :
          (a : ↥{f s} → E) → E)
        (restrict (π := fun (x : T) ↦ E) {f s} fun (x : T) ↦ X x ω : (i : ↥{f s}) → E)

Tactic:
simp
-- 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
F : Type u_6
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℝ F
inst_7 : MeasurableSpace F
inst_8 : BorelSpace F
inst_9 : SecondCountableTopology F
L : T → E →L[ℝ] F
h : IsGaussianProcess X P
t : T
x : ↥{t} → E
⊢ Membership.mem (γ := Finset T) {t} t

Tactic:
simp
-- 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
F : Type u_6
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℝ F
inst_7 : MeasurableSpace F
inst_8 : BorelSpace F
inst_9 : SecondCountableTopology F
L : T → E →L[ℝ] F
h : IsGaussianProcess X P
t : T
⊢ ∀ (x y : ↥{t} → E),
    (L t : (a : E) → F) ((x + y) (Subtype.mk (p := fun (x : T) ↦ Membership.mem (γ := Finset T) {t} x) t ⋯)) =
      HAdd.hAdd (α := F) (β := F)
        ((L t : (a : E) → F) (x (Subtype.mk (p := fun (x : T) ↦ Membership.mem (γ := Finset T) {t} x) t ⋯)) : F)
        ((L t : (a : E) → F) (y (Subtype.mk (p := fun (x : T) ↦ Membership.mem (γ := Finset T) {t} x) t ⋯)) : F)

Tactic:
simp
-- 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
F : Type u_6
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℝ F
inst_7 : MeasurableSpace F
inst_8 : BorelSpace F
inst_9 : SecondCountableTopology F
L : T → E →L[ℝ] F
h : IsGaussianProcess X P
t : T
⊢ ∀ (m : ℝ) (x : ↥{t} → E),
    (L t : (a : E) → F) ((m • x) (Subtype.mk (p := fun (x : T) ↦ Membership.mem (γ := Finset T) {t} x) t ⋯)) =
      HSMul.hSMul (α := ℝ) (β := F) ((RingHom.id ℝ : (a : ℝ) → ℝ) m : ℝ)
        ((L t : (a : E) → F) (x (Subtype.mk (p := fun (x : T) ↦ Membership.mem (γ := Finset T) {t} x) t ⋯)) : F)

Tactic:
simp
-- 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
F : Type u_6
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℝ F
inst_7 : MeasurableSpace F
inst_8 : BorelSpace F
inst_9 : SecondCountableTopology F
L : T → E →L[ℝ] F
h : IsGaussianProcess X P
t : T
⊢ ∀ (ω : Ω),
    Eq.{u_6 + 1} (α := F) ((L t : (a : E) → F) (X t ω) : F)
      ((({
                toFun := fun (x : ↥{t} → E) ↦
                  (L t : (a : E) → F) (x (Subtype.mk (p := fun (x : T) ↦ Membership.mem (γ := Finset T) {t} x) t ⋯)),
                map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } :
              (↥{t} → E) →L[ℝ] F) :
            (a : ↥{t} → E) → F)
          (restrict (π := fun (x : T) ↦ E) {t} fun (x : T) ↦ X x ω : (i : ↥{t}) → E) :
        F)

Tactic:
simp
-- 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
c : T → ℝ
hX : IsGaussianProcess X P
⊢ IsGaussianProcess.{u_3, u_4, u_2} (E := E) (fun (t : T) (ω : Ω) ↦ c t • X t ω) P

Tactic:
hX.comp_left (fun t ↦ .lsmul ℝ ℝ (c t))

Premises used: Real, ProbabilityTheory.IsGaussianProcess.comp_left, ContinuousLinearMap.lsmul, DFunLike.coe
-- 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
inst_5 : Add T
h : IsGaussianProcess X P
t₀ t : T
x : ↥{t₀, t₀ + t} → E
⊢ Membership.mem (γ := Finset T) {t₀, t₀ + t} (t₀ + t)

Tactic:
simp
-- 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
inst_5 : Add T
h : IsGaussianProcess X P
t₀ t : T
x : ↥{t₀, t₀ + t} → E
⊢ Membership.mem (γ := Finset T) {t₀, t₀ + t} t₀

Tactic:
simp
-- 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
inst_5 : Add T
h : IsGaussianProcess X P
t₀ t : T
x y : ↥{t₀, t₀ + t} → E
simp :
  x (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₀ + 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₀ ⋯)) =
    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₀ ⋯))
⊢ (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₀ ⋯))

Tactic:
simp
-- 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
inst_5 : Add T
h : IsGaussianProcess X P
t₀ t : T
x y : ↥{t₀, t₀ + t} → E
⊢ x (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₀ + 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₀ ⋯)) =
    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₀ ⋯))

Tactic:
abel
-- 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
inst_5 : Add T
h : IsGaussianProcess X P
t₀ t : T
c : ℝ
x : ↥{t₀, t₀ + t} → E
simp :
  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₀ ⋯) =
    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₀ ⋯))
⊢ (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₀ ⋯))

Tactic:
simp
-- 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
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₀ ⋯) =
    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₀ ⋯))

Tactic:
module
-- 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
inst_5 : Add T
h : IsGaussianProcess X P
t₀ t : T
⊢ ∀ (ω : Ω),
    X (t₀ + t) ω - X t₀ ω =
      ({
            toFun := fun (x : ↥{t₀, t₀ + t} → E) ↦
              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₀ ⋯),
            map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } :
          (a : ↥{t₀, t₀ + t} → E) → E)
        (restrict (π := fun (x : T) ↦ E) {t₀, t₀ + t} fun (x : T) ↦ X x ω : (i : ↥{t₀, t₀ + t}) → E)

Tactic:
simp
-- 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
inst_5 : Add T
h : IsGaussianProcess X P
t₀ : T
⊢ IsGaussianProcess.{u_3, u_4, u_2} (E := E) (fun (t : T) (ω : Ω) ↦ X (t₀ + t) ω - X t₀ ω) P

Tactic:
exact h.of_isGaussianProcess fun t ↦ ⟨{t₀, t₀ + t},
    { toFun x := x ⟨t₀ + t, by simp⟩ - x ⟨t₀, by simp⟩
      map_add' x y := by simp; abel
      map_smul' c x := by simp; module },
    by simp⟩

Premises used: ContinuousLinearMap.mk, HSub.hSub, Insert.insert, Subtype.mk, ProbabilityTheory.IsGaussianProcess.of_isGaussianProcess, HAdd.hAdd, LinearMap.mk, Exists.intro, AddHom.mk, Singleton.singleton
-- 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
inst_5 : Add T
h : IsGaussianProcess X P
t₀ : T
⊢ IsGaussianProcess.{u_3, u_4, u_2} (E := E) (fun (t : T) (ω : Ω) ↦ X (t₀ + t) ω - X t₀ ω) P

Tactic:
classical
  exact h.of_isGaussianProcess fun t ↦ ⟨{t₀, t₀ + t},
    { toFun x := x ⟨t₀ + t, by simp⟩ - x ⟨t₀, by simp⟩
      map_add' x y := by simp; abel
      map_smul' c x := by simp; module },
    by simp⟩