awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic (goal)
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
F : Type u_4
G : Type u_5
inst_2 : MeasurableSpace G
inst_3 : FunLike F E G
inst_4 : AddGroup E
inst_5 : SubtractionMonoid G
inst_6 : AddMonoidHomClass F E G
f : F
hf : Measurable.{u_3, u_5} (α := E) (β := G) (⇑f : (a : E) → G)
hX : HasIndepIncrements X P
n : ℕ
t : Fin (n + 1) → T
ht : Monotone t
⊢ iIndepFun (β := fun (i : Fin n) ↦ G)
    (fun (i : Fin n) (ω : Ω) ↦
      HSub.hSub (α := G) ((fun (t : T) (ω : Ω) ↦ ((f : (a : E) → G) (X t ω) : G)) (t i.succ) ω)
        ((fun (t : T) (ω : Ω) ↦ ((f : (a : E) → G) (X t ω) : G)) (t i.castSucc) ω))
    P
have simp_rw : iIndepFun (β := fun (i : Fin n) ↦ G) (fun (i : Fin n) (ω : Ω) ↦ (f : (a : E) → G) (X (t i.succ) ω - X (t i.castSucc) ω))
  P
Tactic: simp_rw [← map_sub]
-- Lean 4 proof step from Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess (goal)
Goal:
T : Type u_1
inst : LinearOrder T
I : Finset T
inst_1 : Bot T
i : Fin (#I + 1)
hi : i ≠ 0
⊢ I.orderEmbOfFinWithBot i = (I.orderEmbOfFin ⋯ : (a : Fin #I) → T) (i.pred hi)
have rw : Eq (α := T) (if h : i = 0 then ⊥ else (I.orderEmbOfFin sorry : (a : Fin #I) → T) (i.pred h) : T)
  ((I.orderEmbOfFin sorry : (a : Fin #I) → T) (i.pred hi) : T)
Tactic: rw [orderEmbOfFinWithBot, dif_neg hi]
-- Lean 4 proof step from Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess (goal)
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)
⊢ I.orderEmbOfFinWithBot i = (I.orderEmbOfFin ⋯ : (a : Fin #I) → T) (i.pred hi)
have rw₁ : Eq (α := T) ((I.orderEmbOfFin sorry : (a : Fin #I) → T) (i.pred hi) : T)
  ((I.orderEmbOfFin sorry : (a : Fin #I) → T) (i.pred hi) : T)
Tactic: rw [orderEmbOfFinWithBot, dif_neg hi]
-- Lean 4 proof step from Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess (goal)
Goal:
T : Type u_1
inst : LinearOrder T
I : Finset T
inst_1 : Bot T
i : Fin #I
⊢ I.orderEmbOfFinWithBot i.succ = (I.orderEmbOfFin ⋯ : (a : Fin #I) → T) i
have hi : i.succ ≠ 0
Tactic: rw [orderEmbOfFinWithBot_of_ne_zero, Fin.pred_succ]
-- Lean 4 proof step from Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess (goal)
Goal:
T : Type u_1
inst : LinearOrder T
I : Finset T
inst_1 : OrderBot T
i j : Fin (#I + 1)
hij : i ≤ j
⊢ I.orderEmbOfFinWithBot i ≤ I.orderEmbOfFinWithBot j
have inl : ∀ (hij : 0 ≤ j), I.orderEmbOfFinWithBot 0 ≤ I.orderEmbOfFinWithBot j
Tactic: obtain rfl | hi := eq_or_ne i 0
Cleared hypotheses: i, hij
-- Lean 4 proof step from Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess (goal)
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
⊢ I.orderEmbOfFinWithBot i ≤ I.orderEmbOfFinWithBot j
have inr : ∀ (hi : i ≠ 0), I.orderEmbOfFinWithBot i ≤ I.orderEmbOfFinWithBot j
Tactic: obtain rfl | hi := eq_or_ne i 0
-- Lean 4 proof step from Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess (goal)
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.orderEmbOfFinWithBot i ≤ I.orderEmbOfFinWithBot j
have inr : LE.le (α := T) ((I.orderEmbOfFin sorry : (a : Fin #I) → T) (i.pred hi) : T)
  ((I.orderEmbOfFin sorry : (a : Fin #I) → T) (j.pred sorry) : T)
Tactic: rw [orderEmbOfFinWithBot_of_ne_zero I i hi, orderEmbOfFinWithBot_of_ne_zero I j (by grind)]
-- Lean 4 proof step from Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess (goal)
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
⊢ (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
have h : ∀ (x_1 : ↥I),
  ∑ j ∈ (Iic (((OrderIso.symm (I.orderIsoOfFin sorry) : ↥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 sorry) : ↥I ≃o Fin #I) : (a : ↥I) → Fin #I) i) : Finset (Fin #I)), x j)
      (fun (i : ↥I) ↦
        ∑ j ∈ (Iic (((OrderIso.symm (I.orderIsoOfFin sorry) : ↥I ≃o Fin #I) : (a : ↥I) → Fin #I) i) : Finset (Fin #I)), y j)
      x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess (goal)
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
⊢ (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
have h : ∀ (x_1 : ↥I),
  ∑ j ∈ (Iic (((OrderIso.symm (I.orderIsoOfFin sorry) : ↥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 sorry) : ↥I ≃o Fin #I) : (a : ↥I) → Fin #I) i) : Finset (Fin #I)), x j)
      x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess (goal)
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
⊢ (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) ω)
have 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)
Tactic: filter_upwards [h] with ω hω
-- Lean 4 proof step from Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess (goal)
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
⊢ 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)
have 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)
Tactic: ext t
-- Lean 4 proof step from Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess (goal)
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
⊢ 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)
have h₁ : X (↑t : T) ω =
  ∑ x ∈ (Iic (((OrderIso.symm (I.orderIsoOfFin sorry) : ↥I ≃o Fin #I) : (a : ↥I) → Fin #I) t) : Finset (Fin #I)),
    (X (I.orderEmbOfFinWithBot x.succ) ω - X (I.orderEmbOfFinWithBot x.castSucc) ω)
Tactic: simp only [restrict, incrementsToRestrict, ContinuousLinearMap.coe_mk', LinearMap.coe_mk,
    AddHom.coe_mk, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess (goal)
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 ∈ (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) ω)
have h₁ : X (↑t : T) ω =
  X (I.orderEmbOfFinWithBot (Fin.succ (((OrderIso.symm (I.orderIsoOfFin sorry) : ↥I ≃o Fin #I) : (a : ↥I) → Fin #I) t))) ω -
    X (I.orderEmbOfFinWithBot 0) ω
Tactic: rw [Fin.sum_Iic_sub _ (fun j ↦ X (I.orderEmbOfFinWithBot j) ω)]
-- Lean 4 proof step from Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess (hypothesis)
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
⊢ HasGaussianLaw (E := (i : ↥I) → E) (fun (ω : Ω) ↦ I.restrict (π := fun (x : T) ↦ E) fun (x : T) ↦ X x ω) P
have this : IsProbabilityMeasure P
Tactic: have := (law ⊥).isProbabilityMeasure
-- Lean 4 proof step from Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess (goal)
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
⊢ HasGaussianLaw (E := (i : ↥I) → E) (fun (ω : Ω) ↦ I.restrict (π := fun (x : T) ↦ E) fun (x : T) ↦ X x ω) P
have inl : HasGaussianLaw (E := (i : ↥∅) → E) (fun (ω : Ω) ↦ restrict (π := fun (x : T) ↦ E) ∅ fun (x : T) ↦ X x ω) P
Tactic: obtain rfl | hI := I.eq_empty_or_nonempty
Cleared hypotheses: I
-- Lean 4 proof step from Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess (goal)
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
⊢ HasGaussianLaw (E := (i : ↥I) → E) (fun (ω : Ω) ↦ I.restrict (π := fun (x : T) ↦ E) fun (x : T) ↦ X x ω) P
have inr : ∀ (hI : I.Nonempty),
  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
-- Lean 4 proof step from Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess (hypothesis)
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
⊢ HasGaussianLaw (E := (i : ↥I) → E) (fun (ω : Ω) ↦ I.restrict (π := fun (x : T) ↦ E) fun (x : T) ↦ X x ω) P
have 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) ω)
Tactic: have := incrementsToRestrict_increments_orderEmbOfFinWithBot_ae_eq_restrict ℝ h_bot I
-- Lean 4 proof step from Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess (goal)
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
have 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
Tactic: refine .congr (.map ?_ _) this.symm
-- Lean 4 proof step from Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess (goal)
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
have inr : ∀ (i : Fin #I),
  HasGaussianLaw.{u_2, u_3} (E := E)
    (fun (ω : Ω) ↦ X (I.orderEmbOfFinWithBot i.succ) ω - X (I.orderEmbOfFinWithBot i.castSucc) ω) P
Tactic: refine (incr _ _ (monotone_orderEmbOfFinWithBot I)).hasGaussianLaw fun i ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess (goal)
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
have inr : X (I.orderEmbOfFinWithBot i.castSucc) ⟂ᵢ[P] X (I.orderEmbOfFinWithBot i.succ) - X (I.orderEmbOfFinWithBot i.castSucc)
Tactic: refine IndepFun.hasGaussianLaw_sub_of_sub (law _) (law _) ?_
-- Lean 4 proof step from Mathlib.Probability.Independence.ZeroOne (hypothesis)
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
t : Set Ω
h_indep : IndepSet t t κ μα
⊢ ∀ᵐ (a : α) ∂μα,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) ∨
      Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (1 : ℝ≥0∞) ∨
        Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
have h_indep₁ : ∀ᵐ (a : α) ∂μα,
  (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t ∩ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: specialize h_indep t t (measurableSet_generateFrom (Set.mem_singleton t))
    (measurableSet_generateFrom (Set.mem_singleton t))
Cleared hypotheses: h_indep
-- Lean 4 proof step from Mathlib.Probability.Independence.ZeroOne (goal)
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
t : Set Ω
h_indep :
  ∀ᵐ (a : α) ∂μα,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t ∩ t) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
⊢ ∀ᵐ (a : α) ∂μα,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) ∨
      Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (1 : ℝ≥0∞) ∨
        Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
have h : ∀ (a : α)
  (ha :
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t ∩ t) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)),
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) ∨
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (1 : ℝ≥0∞) ∨
      Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: filter_upwards [h_indep] with a ha
-- Lean 4 proof step from Mathlib.Probability.Independence.ZeroOne (goal)
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
t : Set Ω
h_indep :
  ∀ᵐ (a : α) ∂μα,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t ∩ t) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
a : α
ha :
  (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t ∩ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) ∨
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (1 : ℝ≥0∞) ∨
      Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
have pos : ∀ (h0 : Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)),
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) ∨
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (1 : ℝ≥0∞) ∨
      Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: by_cases h0 : κ a t = 0
-- Lean 4 proof step from Mathlib.Probability.Independence.ZeroOne (goal)
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
t : Set Ω
h_indep :
  ∀ᵐ (a : α) ∂μα,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t ∩ t) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
a : α
ha :
  (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t ∩ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
pos :
  ∀ (h0 : Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)),
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) ∨
      Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (1 : ℝ≥0∞) ∨
        Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) ∨
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (1 : ℝ≥0∞) ∨
      Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
have neg : ∀ (h0 : ¬Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)),
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) ∨
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (1 : ℝ≥0∞) ∨
      Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: by_cases h0 : κ a t = 0