awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst : Preorder T
inst_1 : MeasurableSpace E
inst_2 : AddCommGroup E
inst_3 : MeasurableNeg E
hX : HasIndepIncrements X P
⊢ HasIndepIncrements (-X) P

Tactic:
hX.map' (f := negAddMonoidHom) measurable_neg

Premises used: MeasurableNeg.measurable_neg, ProbabilityTheory.HasIndepIncrements.map'
-- Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess
Goal:
T : Type u_1
inst : LinearOrder T
I : Finset T
inst_1 : Bot T
⊢ I.orderEmbOfFinWithBot 0 = ⊥

Tactic:
rfl

Premises used: _private.0.Finset.orderEmbOfFinWithBot, dite, rfl
-- Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess
Goal:
T : Type u_1
inst : LinearOrder T
I : Finset T
inst_1 : Bot T
i : Fin (#I + 1)
hi : i ≠ 0
rw :
  Eq (α := T) (if h : i = 0 then ⊥ else (I.orderEmbOfFin ⋯ : (a : Fin #I) → T) (i.pred h) : T)
    ((I.orderEmbOfFin ⋯ : (a : Fin #I) → T) (i.pred hi) : T)
rw₁ rw₂ :
  Eq (α := T) ((I.orderEmbOfFin ⋯ : (a : Fin #I) → T) (i.pred hi) : T)
    ((I.orderEmbOfFin ⋯ : (a : Fin #I) → T) (i.pred hi) : T)
⊢ I.orderEmbOfFinWithBot i = (I.orderEmbOfFin ⋯ : (a : Fin #I) → T) (i.pred hi)

Tactic:
rw [orderEmbOfFinWithBot, dif_neg hi]

Premises used: _private.0.Finset.orderEmbOfFinWithBot, dif_neg
-- Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess
Goal:
T : Type u_1
inst : LinearOrder T
I : Finset T
inst_1 : Bot T
i : Fin #I
hi : i.succ ≠ 0
⊢ I.orderEmbOfFinWithBot i.succ = (I.orderEmbOfFin ⋯ : (a : Fin #I) → T) i

Tactic:
rw [orderEmbOfFinWithBot_of_ne_zero, Fin.pred_succ]

Premises used: _private.0.Finset.orderEmbOfFinWithBot_of_ne_zero, Fin.pred_succ
-- Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess
Goal:
T : Type u_1
inst : LinearOrder T
I : Finset T
inst_1 : Bot T
i : Fin #I
⊢ i.succ ≠ 0

Tactic:
simp
-- Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess
Goal:
T : Type u_1
inst : LinearOrder T
I : Finset T
inst_1 : OrderBot T
i j : Fin (#I + 1)
hij : i ≤ j
inl : ∀ (hij : 0 ≤ j), I.orderEmbOfFinWithBot 0 ≤ I.orderEmbOfFinWithBot j
inr : ∀ (hi : i ≠ 0), I.orderEmbOfFinWithBot i ≤ I.orderEmbOfFinWithBot j
⊢ I.orderEmbOfFinWithBot i ≤ I.orderEmbOfFinWithBot j

Tactic:
obtain rfl | hi := eq_or_ne i 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess
Goal:
T : Type u_1
inst : LinearOrder T
I : Finset T
inst_1 : OrderBot T
j : Fin (#I + 1)
hij : 0 ≤ j
⊢ I.orderEmbOfFinWithBot 0 ≤ I.orderEmbOfFinWithBot j

Tactic:
simp
-- Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess
Goal:
T : Type u_1
inst : LinearOrder T
I : Finset T
inst_1 : OrderBot T
i j : Fin (#I + 1)
hij : i ≤ j
hi : i ≠ 0
⊢ j ≠ 0

Tactic:
grind
-- Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess
Goal:
T : Type u_1
inst : LinearOrder T
I : Finset T
inst_1 : OrderBot T
i j : Fin (#I + 1)
hij : i ≤ j
hi : i ≠ 0
inr :
  LE.le (α := T) ((I.orderEmbOfFin ⋯ : (a : Fin #I) → T) (i.pred hi) : T)
    ((I.orderEmbOfFin ⋯ : (a : Fin #I) → T) (j.pred ⋯) : T)
⊢ I.orderEmbOfFinWithBot i ≤ I.orderEmbOfFinWithBot j

Tactic:
rw [orderEmbOfFinWithBot_of_ne_zero I i hi, orderEmbOfFinWithBot_of_ne_zero I j (by grind)]

Premises used: _private.0.Finset.orderEmbOfFinWithBot_of_ne_zero
-- Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess
Goal:
T : Type u_1
inst : LinearOrder T
I : Finset T
inst_1 : OrderBot T
i j : Fin (#I + 1)
hij : i ≤ j
hi : i ≠ 0
⊢ i.pred hi ≤ j.pred ⋯

Tactic:
simpa
-- Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess
Goal:
T : Type u_1
inst : LinearOrder T
I : Finset T
inst_1 : OrderBot T
i j : Fin (#I + 1)
hij : i ≤ j
hi : i ≠ 0
⊢ LE.le (α := T) ((I.orderEmbOfFin ⋯ : (a : Fin #I) → T) (i.pred hi) : T)
    ((I.orderEmbOfFin ⋯ : (a : Fin #I) → T) (j.pred ⋯) : T)

Tactic:
exact OrderEmbedding.monotone _ (by simpa)

Premises used: OrderEmbedding.monotone
-- Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : LinearOrder T
R : Type u_4
inst_1 : Semiring R
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : TopologicalSpace E
inst_5 : ContinuousAdd E
I : Finset T
x y : Fin #I → E
h :
  ∀ (x_1 : ↥I),
    ∑ j ∈ (Iic (((OrderIso.symm (I.orderIsoOfFin ⋯) : ↥I ≃o Fin #I) : (a : ↥I) → Fin #I) x_1) : Finset (Fin #I)),
        (x + y) j =
      HAdd.hAdd (α := ↥I → E) (β := ↥I → E)
        (fun (i : ↥I) ↦
          ∑ j ∈ (Iic (((OrderIso.symm (I.orderIsoOfFin ⋯) : ↥I ≃o Fin #I) : (a : ↥I) → Fin #I) i) : Finset (Fin #I)),
            x j)
        (fun (i : ↥I) ↦
          ∑ j ∈ (Iic (((OrderIso.symm (I.orderIsoOfFin ⋯) : ↥I ≃o Fin #I) : (a : ↥I) → Fin #I) i) : Finset (Fin #I)),
            y j)
        x_1
⊢ (fun (i : ↥I) ↦
      ∑ j ∈ (Iic (((OrderIso.symm (I.orderIsoOfFin ⋯) : ↥I ≃o Fin #I) : (a : ↥I) → Fin #I) i) : Finset (Fin #I)),
        (x + y) j) =
    HAdd.hAdd (α := ↥I → E)
      (fun (i : ↥I) ↦
        ∑ j ∈ (Iic (((OrderIso.symm (I.orderIsoOfFin ⋯) : ↥I ≃o Fin #I) : (a : ↥I) → Fin #I) i) : Finset (Fin #I)), x j)
      fun (i : ↥I) ↦
      ∑ j ∈ (Iic (((OrderIso.symm (I.orderIsoOfFin ⋯) : ↥I ≃o Fin #I) : (a : ↥I) → Fin #I) i) : Finset (Fin #I)), y j

Tactic:
ext
-- Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : LinearOrder T
R : Type u_4
inst_1 : Semiring R
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : TopologicalSpace E
inst_5 : ContinuousAdd E
I : Finset T
x y : Fin #I → E
x_1 : ↥I
⊢ ∑ j ∈ (Iic (((OrderIso.symm (I.orderIsoOfFin ⋯) : ↥I ≃o Fin #I) : (a : ↥I) → Fin #I) x_1) : Finset (Fin #I)),
      (x + y) j =
    HAdd.hAdd (α := ↥I → E) (β := ↥I → E)
      (fun (i : ↥I) ↦
        ∑ j ∈ (Iic (((OrderIso.symm (I.orderIsoOfFin ⋯) : ↥I ≃o Fin #I) : (a : ↥I) → Fin #I) i) : Finset (Fin #I)), x j)
      (fun (i : ↥I) ↦
        ∑ j ∈ (Iic (((OrderIso.symm (I.orderIsoOfFin ⋯) : ↥I ≃o Fin #I) : (a : ↥I) → Fin #I) i) : Finset (Fin #I)), y j)
      x_1

Tactic:
simp [sum_add_distrib]

Premises used: Finset.sum_add_distrib
-- Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : LinearOrder T
R : Type u_4
inst_1 : Semiring R
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : TopologicalSpace E
inst_5 : ContinuousAdd E
I : Finset T
m : R
x : Fin #I → E
h :
  ∀ (x_1 : ↥I),
    ∑ j ∈ (Iic (((OrderIso.symm (I.orderIsoOfFin ⋯) : ↥I ≃o Fin #I) : (a : ↥I) → Fin #I) x_1) : Finset (Fin #I)),
        (m • x) j =
      HSMul.hSMul (α := R) (β := ↥I → E) ((RingHom.id R : (a : R) → R) m : R)
        (fun (i : ↥I) ↦
          ∑ j ∈ (Iic (((OrderIso.symm (I.orderIsoOfFin ⋯) : ↥I ≃o Fin #I) : (a : ↥I) → Fin #I) i) : Finset (Fin #I)),
            x j)
        x_1
⊢ (fun (i : ↥I) ↦
      ∑ j ∈ (Iic (((OrderIso.symm (I.orderIsoOfFin ⋯) : ↥I ≃o Fin #I) : (a : ↥I) → Fin #I) i) : Finset (Fin #I)),
        (m • x) j) =
    HSMul.hSMul (α := R) (β := ↥I → E) ((RingHom.id R : (a : R) → R) m : R) fun (i : ↥I) ↦
      ∑ j ∈ (Iic (((OrderIso.symm (I.orderIsoOfFin ⋯) : ↥I ≃o Fin #I) : (a : ↥I) → Fin #I) i) : Finset (Fin #I)), x j

Tactic:
ext
-- Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : LinearOrder T
R : Type u_4
inst_1 : Semiring R
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : TopologicalSpace E
inst_5 : ContinuousAdd E
I : Finset T
m : R
x : Fin #I → E
x_1 : ↥I
⊢ ∑ j ∈ (Iic (((OrderIso.symm (I.orderIsoOfFin ⋯) : ↥I ≃o Fin #I) : (a : ↥I) → Fin #I) x_1) : Finset (Fin #I)),
      (m • x) j =
    HSMul.hSMul (α := R) (β := ↥I → E) ((RingHom.id R : (a : R) → R) m : R)
      (fun (i : ↥I) ↦
        ∑ j ∈ (Iic (((OrderIso.symm (I.orderIsoOfFin ⋯) : ↥I ≃o Fin #I) : (a : ↥I) → Fin #I) i) : Finset (Fin #I)), x j)
      x_1

Tactic:
simp [smul_sum]

Premises used: Finset.smul_sum
-- Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : LinearOrder T
R : Type u_4
inst_1 : Semiring R
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : TopologicalSpace E
inst_5 : ContinuousAdd E
I : Finset T
⊢ Continuous (Y := ↥I → E) fun (x : Fin #I → E) (i : ↥I) ↦
    ∑ j ∈ (Iic (((OrderIso.symm (I.orderIsoOfFin ⋯) : ↥I ≃o Fin #I) : (a : ↥I) → Fin #I) i) : Finset (Fin #I)), x j

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : LinearOrder T
inst_1 : Bot T
R : Type u_4
inst_2 : Semiring R
inst_3 : AddCommGroup E
inst_4 : Module R E
inst_5 : TopologicalSpace E
inst_6 : ContinuousAdd E
X : T → Ω → E
h : ∀ᵐ (ω : Ω) ∂P, X ⊥ ω = 0
I : Finset T
h₁ :
  ∀ (ω : Ω) (hω : X ⊥ ω = 0),
    Eq (α := (i : ↥I) → E) (I.restrict (π := fun (x : T) ↦ E) fun (x : T) ↦ X x ω : (i : ↥I) → E)
      (Function.comp (β := Fin #I → E) (⇑(incrementsToRestrict R I) : (a : Fin #I → E) → ↥I → E)
          (fun (ω : Ω) (i : Fin #I) ↦ X (I.orderEmbOfFinWithBot i.succ) ω - X (I.orderEmbOfFinWithBot i.castSucc) ω) ω :
        (i : ↥I) → E)
⊢ (ae P).EventuallyEq (β := (i : ↥I) → E) (fun (ω : Ω) ↦ I.restrict (π := fun (x : T) ↦ E) fun (x : T) ↦ X x ω)
    (Function.comp (β := Fin #I → E) (⇑(incrementsToRestrict R I) : (a : Fin #I → E) → ↥I → E)
      fun (ω : Ω) (i : Fin #I) ↦ X (I.orderEmbOfFinWithBot i.succ) ω - X (I.orderEmbOfFinWithBot i.castSucc) ω)

Tactic:
filter_upwards [h] with ω hω
-- Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : LinearOrder T
inst_1 : Bot T
R : Type u_4
inst_2 : Semiring R
inst_3 : AddCommGroup E
inst_4 : Module R E
inst_5 : TopologicalSpace E
inst_6 : ContinuousAdd E
X : T → Ω → E
h : ∀ᵐ (ω : Ω) ∂P, X ⊥ ω = 0
I : Finset T
ω : Ω
hω : X ⊥ ω = 0
h₁ :
  ∀ (t : ↥I),
    Eq.{u_3 + 1} (α := E) (I.restrict (π := fun (x : T) ↦ E) (fun (x : T) ↦ X x ω) t : E)
      (Function.comp (β := Fin #I → E) (⇑(incrementsToRestrict R I) : (a : Fin #I → E) → ↥I → E)
          (fun (ω : Ω) (i : Fin #I) ↦ X (I.orderEmbOfFinWithBot i.succ) ω - X (I.orderEmbOfFinWithBot i.castSucc) ω) ω
          t :
        E)
⊢ Eq (α := (i : ↥I) → E) (I.restrict (π := fun (x : T) ↦ E) fun (x : T) ↦ X x ω : (i : ↥I) → E)
    (Function.comp (β := Fin #I → E) (⇑(incrementsToRestrict R I) : (a : Fin #I → E) → ↥I → E)
        (fun (ω : Ω) (i : Fin #I) ↦ X (I.orderEmbOfFinWithBot i.succ) ω - X (I.orderEmbOfFinWithBot i.castSucc) ω) ω :
      (i : ↥I) → E)

Tactic:
ext t
-- Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : LinearOrder T
inst_1 : Bot T
R : Type u_4
inst_2 : Semiring R
inst_3 : AddCommGroup E
inst_4 : Module R E
inst_5 : TopologicalSpace E
inst_6 : ContinuousAdd E
X : T → Ω → E
h : ∀ᵐ (ω : Ω) ∂P, X ⊥ ω = 0
I : Finset T
ω : Ω
hω : X ⊥ ω = 0
t : ↥I
h₁ :
  X (↑t : T) ω =
    ∑ x ∈ (Iic (((OrderIso.symm (I.orderIsoOfFin ⋯) : ↥I ≃o Fin #I) : (a : ↥I) → Fin #I) t) : Finset (Fin #I)),
      (X (I.orderEmbOfFinWithBot x.succ) ω - X (I.orderEmbOfFinWithBot x.castSucc) ω)
⊢ Eq.{u_3 + 1} (α := E) (I.restrict (π := fun (x : T) ↦ E) (fun (x : T) ↦ X x ω) t : E)
    (Function.comp (β := Fin #I → E) (⇑(incrementsToRestrict R I) : (a : Fin #I → E) → ↥I → E)
        (fun (ω : Ω) (i : Fin #I) ↦ X (I.orderEmbOfFinWithBot i.succ) ω - X (I.orderEmbOfFinWithBot i.castSucc) ω) ω t :
      E)

Tactic:
simp only [restrict, incrementsToRestrict, ContinuousLinearMap.coe_mk', LinearMap.coe_mk,
    AddHom.coe_mk, Function.comp_apply]

Premises used: LinearMap.coe_mk, Finset.restrict, Function.comp_apply, AddHom.coe_mk, ContinuousLinearMap.coe_mk', _private.0.ProbabilityTheory.incrementsToRestrict
-- Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : LinearOrder T
inst_1 : Bot T
R : Type u_4
inst_2 : Semiring R
inst_3 : AddCommGroup E
inst_4 : Module R E
inst_5 : TopologicalSpace E
inst_6 : ContinuousAdd E
X : T → Ω → E
h : ∀ᵐ (ω : Ω) ∂P, X ⊥ ω = 0
I : Finset T
ω : Ω
hω : X ⊥ ω = 0
t : ↥I
h₁ :
  X (↑t : T) ω =
    X (I.orderEmbOfFinWithBot (Fin.succ (((OrderIso.symm (I.orderIsoOfFin ⋯) : ↥I ≃o Fin #I) : (a : ↥I) → Fin #I) t)))
        ω -
      X (I.orderEmbOfFinWithBot 0) ω
⊢ X (↑t : T) ω =
    ∑ x ∈ (Iic (((OrderIso.symm (I.orderIsoOfFin ⋯) : ↥I ≃o Fin #I) : (a : ↥I) → Fin #I) t) : Finset (Fin #I)),
      (X (I.orderEmbOfFinWithBot x.succ) ω - X (I.orderEmbOfFinWithBot x.castSucc) ω)

Tactic:
rw [Fin.sum_Iic_sub _ (fun j ↦ X (I.orderEmbOfFinWithBot j) ω)]

Premises used: _private.0.Finset.orderEmbOfFinWithBot, Fin.sum_Iic_sub
-- Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : LinearOrder T
inst_1 : Bot T
R : Type u_4
inst_2 : Semiring R
inst_3 : AddCommGroup E
inst_4 : Module R E
inst_5 : TopologicalSpace E
inst_6 : ContinuousAdd E
X : T → Ω → E
h : ∀ᵐ (ω : Ω) ∂P, X ⊥ ω = 0
I : Finset T
ω : Ω
hω : X ⊥ ω = 0
t : ↥I
⊢ X (↑t : T) ω =
    X (I.orderEmbOfFinWithBot (Fin.succ (((OrderIso.symm (I.orderIsoOfFin ⋯) : ↥I ≃o Fin #I) : (a : ↥I) → Fin #I) t)))
        ω -
      X (I.orderEmbOfFinWithBot 0) ω

Tactic:
simp [hω, orderEmbOfFin]

Premises used: Finset.orderEmbOfFin
-- Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : LinearOrder T
inst_1 : OrderBot T
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : SecondCountableTopology E
inst_7 : CompleteSpace E
X : T → Ω → E
law : ∀ (t : T), HasGaussianLaw (X t) P
h_bot : ∀ᵐ (ω : Ω) ∂P, X ⊥ ω = 0
incr : HasIndepIncrements X P
I : Finset T
⊢ IsProbabilityMeasure P

Tactic:
have := (law ⊥).isProbabilityMeasure
-- Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : LinearOrder T
inst_1 : OrderBot T
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : SecondCountableTopology E
inst_7 : CompleteSpace E
X : T → Ω → E
law : ∀ (t : T), HasGaussianLaw (X t) P
h_bot : ∀ᵐ (ω : Ω) ∂P, X ⊥ ω = 0
incr : HasIndepIncrements X P
I : Finset T
this : IsProbabilityMeasure P
inl : HasGaussianLaw (E := (i : ↥∅) → E) (fun (ω : Ω) ↦ restrict (π := fun (x : T) ↦ E) ∅ fun (x : T) ↦ X x ω) P
inr :
  ∀ (hI : I.Nonempty),
    HasGaussianLaw (E := (i : ↥I) → E) (fun (ω : Ω) ↦ I.restrict (π := fun (x : T) ↦ E) fun (x : T) ↦ X x ω) P
⊢ HasGaussianLaw (E := (i : ↥I) → E) (fun (ω : Ω) ↦ I.restrict (π := fun (x : T) ↦ E) fun (x : T) ↦ X x ω) P

Tactic:
obtain rfl | hI := I.eq_empty_or_nonempty

Premises used: rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : LinearOrder T
inst_1 : OrderBot T
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : SecondCountableTopology E
inst_7 : CompleteSpace E
X : T → Ω → E
law : ∀ (t : T), HasGaussianLaw (X t) P
h_bot : ∀ᵐ (ω : Ω) ∂P, X ⊥ ω = 0
incr : HasIndepIncrements X P
this : IsProbabilityMeasure P
⊢ HasGaussianLaw (E := (i : ↥∅) → E) (fun (ω : Ω) ↦ restrict (π := fun (x : T) ↦ E) ∅ fun (x : T) ↦ X x ω) P

Tactic:
.of_subsingleton

Premises used: ProbabilityTheory.HasGaussianLaw.of_subsingleton
-- Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : LinearOrder T
inst_1 : OrderBot T
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : SecondCountableTopology E
inst_7 : CompleteSpace E
X : T → Ω → E
law : ∀ (t : T), HasGaussianLaw (X t) P
h_bot : ∀ᵐ (ω : Ω) ∂P, X ⊥ ω = 0
incr : HasIndepIncrements X P
this : IsProbabilityMeasure P
⊢ HasGaussianLaw (E := (i : ↥∅) → E) (fun (ω : Ω) ↦ restrict (π := fun (x : T) ↦ E) ∅ fun (x : T) ↦ X x ω) P

Tactic:
exact .of_subsingleton
-- Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : LinearOrder T
inst_1 : OrderBot T
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : SecondCountableTopology E
inst_7 : CompleteSpace E
X : T → Ω → E
law : ∀ (t : T), HasGaussianLaw (X t) P
h_bot : ∀ᵐ (ω : Ω) ∂P, X ⊥ ω = 0
incr : HasIndepIncrements X P
I : Finset T
this : IsProbabilityMeasure P
hI : I.Nonempty
⊢ (ae P).EventuallyEq (β := (i : ↥I) → E) (fun (ω : Ω) ↦ I.restrict (π := fun (x : T) ↦ E) fun (x : T) ↦ X x ω)
    (Function.comp (β := Fin #I → E) (⇑(incrementsToRestrict ℝ I) : (a : Fin #I → E) → ↥I → E)
      fun (ω : Ω) (i : Fin #I) ↦ X (I.orderEmbOfFinWithBot i.succ) ω - X (I.orderEmbOfFinWithBot i.castSucc) ω)

Tactic:
have := incrementsToRestrict_increments_orderEmbOfFinWithBot_ae_eq_restrict ℝ h_bot I
-- Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : LinearOrder T
inst_1 : OrderBot T
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : SecondCountableTopology E
inst_7 : CompleteSpace E
X : T → Ω → E
law : ∀ (t : T), HasGaussianLaw (X t) P
h_bot : ∀ᵐ (ω : Ω) ∂P, X ⊥ ω = 0
incr : HasIndepIncrements X P
I : Finset T
this_1 : IsProbabilityMeasure P
hI : I.Nonempty
this :
  (ae P).EventuallyEq (β := (i : ↥I) → E) (fun (ω : Ω) ↦ I.restrict (π := fun (x : T) ↦ E) fun (x : T) ↦ X x ω)
    (Function.comp (β := Fin #I → E) (⇑(incrementsToRestrict ℝ I) : (a : Fin #I → E) → ↥I → E)
      fun (ω : Ω) (i : Fin #I) ↦ X (I.orderEmbOfFinWithBot i.succ) ω - X (I.orderEmbOfFinWithBot i.castSucc) ω)
⊢ HasGaussianLaw (E := (i : ↥I) → E) (fun (ω : Ω) ↦ I.restrict (π := fun (x : T) ↦ E) fun (x : T) ↦ X x ω) P

Tactic:
.congr (.map ?_ _) this.symm

Premises used: ProbabilityTheory.HasGaussianLaw.congr, ProbabilityTheory.HasGaussianLaw.map, Filter.EventuallyEq.symm
-- Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : LinearOrder T
inst_1 : OrderBot T
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : SecondCountableTopology E
inst_7 : CompleteSpace E
X : T → Ω → E
law : ∀ (t : T), HasGaussianLaw (X t) P
h_bot : ∀ᵐ (ω : Ω) ∂P, X ⊥ ω = 0
incr : HasIndepIncrements X P
I : Finset T
this_1 : IsProbabilityMeasure P
hI : I.Nonempty
this :
  (ae P).EventuallyEq (β := (i : ↥I) → E) (fun (ω : Ω) ↦ I.restrict (π := fun (x : T) ↦ E) fun (x : T) ↦ X x ω)
    (Function.comp (β := Fin #I → E) (⇑(incrementsToRestrict ℝ I) : (a : Fin #I → E) → ↥I → E)
      fun (ω : Ω) (i : Fin #I) ↦ X (I.orderEmbOfFinWithBot i.succ) ω - X (I.orderEmbOfFinWithBot i.castSucc) ω)
inr :
  HasGaussianLaw.{u_2, u_3} (E := Fin #I → E)
    (fun (ω : Ω) (i : Fin #I) ↦ X (I.orderEmbOfFinWithBot i.succ) ω - X (I.orderEmbOfFinWithBot i.castSucc) ω) P
⊢ HasGaussianLaw (E := (i : ↥I) → E) (fun (ω : Ω) ↦ I.restrict (π := fun (x : T) ↦ E) fun (x : T) ↦ X x ω) P

Tactic:
refine .congr (.map ?_ _) this.symm
-- Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : LinearOrder T
inst_1 : OrderBot T
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : SecondCountableTopology E
inst_7 : CompleteSpace E
X : T → Ω → E
law : ∀ (t : T), HasGaussianLaw (X t) P
h_bot : ∀ᵐ (ω : Ω) ∂P, X ⊥ ω = 0
incr : HasIndepIncrements X P
I : Finset T
this_1 : IsProbabilityMeasure P
hI : I.Nonempty
this :
  (ae P).EventuallyEq (β := (i : ↥I) → E) (fun (ω : Ω) ↦ I.restrict (π := fun (x : T) ↦ E) fun (x : T) ↦ X x ω)
    (Function.comp (β := Fin #I → E) (⇑(incrementsToRestrict ℝ I) : (a : Fin #I → E) → ↥I → E)
      fun (ω : Ω) (i : Fin #I) ↦ X (I.orderEmbOfFinWithBot i.succ) ω - X (I.orderEmbOfFinWithBot i.castSucc) ω)
⊢ HasGaussianLaw.{u_2, u_3} (E := Fin #I → E)
    (fun (ω : Ω) (i : Fin #I) ↦ X (I.orderEmbOfFinWithBot i.succ) ω - X (I.orderEmbOfFinWithBot i.castSucc) ω) P

Tactic:
(incr _ _ (monotone_orderEmbOfFinWithBot I)).hasGaussianLaw fun i ↦ ?_

Premises used: _private.0.Finset.monotone_orderEmbOfFinWithBot, ProbabilityTheory.iIndepFun.hasGaussianLaw
-- Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : LinearOrder T
inst_1 : OrderBot T
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : SecondCountableTopology E
inst_7 : CompleteSpace E
X : T → Ω → E
law : ∀ (t : T), HasGaussianLaw (X t) P
h_bot : ∀ᵐ (ω : Ω) ∂P, X ⊥ ω = 0
incr : HasIndepIncrements X P
I : Finset T
this_1 : IsProbabilityMeasure P
hI : I.Nonempty
this :
  (ae P).EventuallyEq (β := (i : ↥I) → E) (fun (ω : Ω) ↦ I.restrict (π := fun (x : T) ↦ E) fun (x : T) ↦ X x ω)
    (Function.comp (β := Fin #I → E) (⇑(incrementsToRestrict ℝ I) : (a : Fin #I → E) → ↥I → E)
      fun (ω : Ω) (i : Fin #I) ↦ X (I.orderEmbOfFinWithBot i.succ) ω - X (I.orderEmbOfFinWithBot i.castSucc) ω)
inr :
  ∀ (i : Fin #I),
    HasGaussianLaw.{u_2, u_3} (E := E)
      (fun (ω : Ω) ↦ X (I.orderEmbOfFinWithBot i.succ) ω - X (I.orderEmbOfFinWithBot i.castSucc) ω) P
⊢ HasGaussianLaw.{u_2, u_3} (E := Fin #I → E)
    (fun (ω : Ω) (i : Fin #I) ↦ X (I.orderEmbOfFinWithBot i.succ) ω - X (I.orderEmbOfFinWithBot i.castSucc) ω) P

Tactic:
refine (incr _ _ (monotone_orderEmbOfFinWithBot I)).hasGaussianLaw fun i ↦ ?_

Premises used: _private.0.Finset.monotone_orderEmbOfFinWithBot, ProbabilityTheory.iIndepFun.hasGaussianLaw
-- Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : LinearOrder T
inst_1 : OrderBot T
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : SecondCountableTopology E
inst_7 : CompleteSpace E
X : T → Ω → E
law : ∀ (t : T), HasGaussianLaw (X t) P
h_bot : ∀ᵐ (ω : Ω) ∂P, X ⊥ ω = 0
incr : HasIndepIncrements X P
I : Finset T
this_1 : IsProbabilityMeasure P
hI : I.Nonempty
this :
  (ae P).EventuallyEq (β := (i : ↥I) → E) (fun (ω : Ω) ↦ I.restrict (π := fun (x : T) ↦ E) fun (x : T) ↦ X x ω)
    (Function.comp (β := Fin #I → E) (⇑(incrementsToRestrict ℝ I) : (a : Fin #I → E) → ↥I → E)
      fun (ω : Ω) (i : Fin #I) ↦ X (I.orderEmbOfFinWithBot i.succ) ω - X (I.orderEmbOfFinWithBot i.castSucc) ω)
i : Fin #I
⊢ HasGaussianLaw.{u_2, u_3} (E := E)
    (fun (ω : Ω) ↦ X (I.orderEmbOfFinWithBot i.succ) ω - X (I.orderEmbOfFinWithBot i.castSucc) ω) P

Tactic:
IndepFun.hasGaussianLaw_sub_of_sub (law _) (law _) ?_

Premises used: ProbabilityTheory.IndepFun.hasGaussianLaw_sub_of_sub