awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Martingale.OptionalSampling
Goal:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
inst_6 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_7 : SigmaFiniteFiltration μ ℱ
τ : Ω → WithTop ι
f : ι → Ω → E
i n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
inst_8 : SigmaFinite (μ.trim ⋯)
hin : i ≤ n
refine :
  ∀ (t : Set Ω),
    MeasurableSet ({x : Ω | τ x = (↑i : WithTop ι)} ∩ t) ↔ MeasurableSet ({x : Ω | τ x = (↑i : WithTop ι)} ∩ t)
⊢ μ[f n | hτ.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x = (↑i : WithTop ι)})]
    μ[f n | (↑ℱ : ι → MeasurableSpace Ω) i]

Tactic:
refine condExp_ae_eq_restrict_of_measurableSpace_eq_on hτ.measurableSpace_le (ℱ.le i)
    (hτ.measurableSet_eq' i) fun t => ?_

Premises used: MeasureTheory.IsStoppingTime.measurableSpace_le, MeasureTheory.Filtration.le, MeasureTheory.IsStoppingTime.measurableSet_eq', MeasureTheory.condExp_ae_eq_restrict_of_measurableSpace_eq_on
-- Module: Mathlib.Probability.Martingale.OptionalSampling
Goal:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
inst_6 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_7 : SigmaFiniteFiltration μ ℱ
τ : Ω → WithTop ι
f : ι → Ω → E
i n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
inst_8 : SigmaFinite (μ.trim ⋯)
hin : i ≤ n
t : Set Ω
rw : MeasurableSet (t ∩ {x : Ω | τ x = (↑i : WithTop ι)}) ↔ MeasurableSet (t ∩ {x : Ω | τ x = (↑i : WithTop ι)})
rw₁ rw₂ : MeasurableSet (t ∩ {ω : Ω | τ ω = (↑i : WithTop ι)}) ↔ MeasurableSet (t ∩ {x : Ω | τ x = (↑i : WithTop ι)})
⊢ MeasurableSet ({x : Ω | τ x = (↑i : WithTop ι)} ∩ t) ↔ MeasurableSet ({x : Ω | τ x = (↑i : WithTop ι)} ∩ t)

Tactic:
rw [Set.inter_comm _ t, IsStoppingTime.measurableSet_inter_eq_iff]

Premises used: Set.inter_comm, MeasureTheory.IsStoppingTime.measurableSet_inter_eq_iff
-- Module: Mathlib.Probability.Martingale.OptionalSampling
Goal:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
inst_6 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_7 : SigmaFiniteFiltration μ ℱ
τ : Ω → WithTop ι
f : ι → Ω → E
n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ (↑n : WithTop ι)
inst_8 : SigmaFinite (μ.trim ⋯)
i : ι
pos : ∀ (hin : i ≤ n), μ[f n | hτ.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x = (↑i : WithTop ι)})] f i
neg : ∀ (hin : ¬i ≤ n), μ[f n | hτ.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x = (↑i : WithTop ι)})] f i
⊢ μ[f n | hτ.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x = (↑i : WithTop ι)})] f i

Tactic:
by_cases hin : i ≤ n
-- Module: Mathlib.Probability.Martingale.OptionalSampling
Goal:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
inst_6 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_7 : SigmaFiniteFiltration μ ℱ
τ : Ω → WithTop ι
f : ι → Ω → E
n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ (↑n : WithTop ι)
inst_8 : SigmaFinite (μ.trim ⋯)
i : ι
hin : i ≤ n
⊢ μ[f n | hτ.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x = (↑i : WithTop ι)})] f i

Tactic:
Filter.EventuallyEq.trans ?_ (ae_restrict_of_ae (h.condExp_ae_eq hin))

Premises used: Filter.EventuallyEq.trans, MeasureTheory.ae_restrict_of_ae, MeasureTheory.Martingale.condExp_ae_eq
-- Module: Mathlib.Probability.Martingale.OptionalSampling
Goal:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
inst_6 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_7 : SigmaFiniteFiltration μ ℱ
τ : Ω → WithTop ι
f : ι → Ω → E
n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ (↑n : WithTop ι)
inst_8 : SigmaFinite (μ.trim ⋯)
i : ι
hin : i ≤ n
pos :
  μ[f n | hτ.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x = (↑i : WithTop ι)})]
    μ[f n | (↑ℱ : ι → MeasurableSpace Ω) i]
⊢ μ[f n | hτ.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x = (↑i : WithTop ι)})] f i

Tactic:
refine Filter.EventuallyEq.trans ?_ (ae_restrict_of_ae (h.condExp_ae_eq hin))

Premises used: Filter.EventuallyEq.trans, MeasureTheory.ae_restrict_of_ae, MeasureTheory.Martingale.condExp_ae_eq
-- Module: Mathlib.Probability.Martingale.OptionalSampling
Goal:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
inst_6 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_7 : SigmaFiniteFiltration μ ℱ
τ : Ω → WithTop ι
f : ι → Ω → E
n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ (↑n : WithTop ι)
inst_8 : SigmaFinite (μ.trim ⋯)
i : ι
hin : i ≤ n
⊢ μ[f n | hτ.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x = (↑i : WithTop ι)})]
    μ[f n | (↑ℱ : ι → MeasurableSpace Ω) i]

Tactic:
condExp_ae_eq_restrict_of_measurableSpace_eq_on (hτ.measurableSpace_le_of_le hτ_le)
      (ℱ.le i) (hτ.measurableSet_eq' i) fun t => ?_

Premises used: MeasureTheory.Filtration.le, MeasureTheory.IsStoppingTime.measurableSet_eq', MeasureTheory.condExp_ae_eq_restrict_of_measurableSpace_eq_on, MeasureTheory.IsStoppingTime.measurableSpace_le_of_le
-- Module: Mathlib.Probability.Martingale.OptionalSampling
Goal:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
inst_6 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_7 : SigmaFiniteFiltration μ ℱ
τ : Ω → WithTop ι
f : ι → Ω → E
n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ (↑n : WithTop ι)
inst_8 : SigmaFinite (μ.trim ⋯)
i : ι
hin : i ≤ n
pos :
  ∀ (t : Set Ω),
    MeasurableSet ({x : Ω | τ x = (↑i : WithTop ι)} ∩ t) ↔ MeasurableSet ({x : Ω | τ x = (↑i : WithTop ι)} ∩ t)
⊢ μ[f n | hτ.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x = (↑i : WithTop ι)})]
    μ[f n | (↑ℱ : ι → MeasurableSpace Ω) i]

Tactic:
refine condExp_ae_eq_restrict_of_measurableSpace_eq_on (hτ.measurableSpace_le_of_le hτ_le)
      (ℱ.le i) (hτ.measurableSet_eq' i) fun t => ?_

Premises used: MeasureTheory.Filtration.le, MeasureTheory.IsStoppingTime.measurableSet_eq', MeasureTheory.condExp_ae_eq_restrict_of_measurableSpace_eq_on, MeasureTheory.IsStoppingTime.measurableSpace_le_of_le
-- Module: Mathlib.Probability.Martingale.OptionalSampling
Goal:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
inst_6 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_7 : SigmaFiniteFiltration μ ℱ
τ : Ω → WithTop ι
f : ι → Ω → E
n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ (↑n : WithTop ι)
inst_8 : SigmaFinite (μ.trim ⋯)
i : ι
hin : i ≤ n
t : Set Ω
pos : MeasurableSet (t ∩ {x : Ω | τ x = (↑i : WithTop ι)}) ↔ MeasurableSet (t ∩ {x : Ω | τ x = (↑i : WithTop ι)})
pos₁ pos₂ : MeasurableSet (t ∩ {ω : Ω | τ ω = (↑i : WithTop ι)}) ↔ MeasurableSet (t ∩ {x : Ω | τ x = (↑i : WithTop ι)})
⊢ MeasurableSet ({x : Ω | τ x = (↑i : WithTop ι)} ∩ t) ↔ MeasurableSet ({x : Ω | τ x = (↑i : WithTop ι)} ∩ t)

Tactic:
rw [Set.inter_comm _ t, IsStoppingTime.measurableSet_inter_eq_iff]

Premises used: Set.inter_comm, MeasureTheory.IsStoppingTime.measurableSet_inter_eq_iff
-- Module: Mathlib.Probability.Martingale.OptionalSampling
Goal:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
inst_6 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_7 : SigmaFiniteFiltration μ ℱ
τ : Ω → WithTop ι
f : ι → Ω → E
n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ (↑n : WithTop ι)
inst_8 : SigmaFinite (μ.trim ⋯)
i : ι
hin : ¬i ≤ n
this : Eq.{u_1 + 1} (α := Set Ω) {x : Ω | τ x = (↑i : WithTop ι)} ∅
simp : μ[f n | hτ.measurableSpace] =ᶠ[⊥] f i
⊢ μ[f n | hτ.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x = (↑i : WithTop ι)})] f i

Tactic:
simp [this]
-- Module: Mathlib.Probability.Martingale.OptionalSampling
Goal:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
inst_6 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_7 : SigmaFiniteFiltration μ ℱ
τ : Ω → WithTop ι
f : ι → Ω → E
n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ (↑n : WithTop ι)
inst_8 : SigmaFinite (μ.trim ⋯)
i : ι
hin : ¬i ≤ n
this : Eq.{u_1 + 1} (α := Set Ω) {x : Ω | τ x = (↑i : WithTop ι)} ∅
⊢ μ[f n | hτ.measurableSpace] =ᶠ[⊥] f i

Tactic:
norm_cast
-- Module: Mathlib.Probability.Martingale.OptionalSampling
Goal:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
inst_6 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_7 : SigmaFiniteFiltration μ ℱ
τ : Ω → WithTop ι
f : ι → Ω → E
n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ (↑n : WithTop ι)
inst_8 : SigmaFinite (μ.trim ⋯)
i : ι
hin : ¬i ≤ n
neg : Eq.{u_1 + 1} (α := Set Ω) {x : Ω | τ x = (↑i : WithTop ι)} ∅
⊢ μ[f n | hτ.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x = (↑i : WithTop ι)})] f i

Tactic:
suffices {x : Ω | τ x = i} = ∅ by simp [this]; norm_cast
-- Module: Mathlib.Probability.Martingale.OptionalSampling
Goal:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
inst_6 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_7 : SigmaFiniteFiltration μ ℱ
τ : Ω → WithTop ι
f : ι → Ω → E
n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ (↑n : WithTop ι)
inst_8 : SigmaFinite (μ.trim ⋯)
i : ι
hin : ¬i ≤ n
neg : ∀ (x : Ω), Membership.mem (γ := Set Ω) {x : Ω | τ x = (↑i : WithTop ι)} x ↔ Membership.mem (γ := Set Ω) ∅ x
⊢ Eq.{u_1 + 1} (α := Set Ω) {x : Ω | τ x = (↑i : WithTop ι)} ∅

Tactic:
ext1 x
-- Module: Mathlib.Probability.Martingale.OptionalSampling
Goal:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
inst_6 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_7 : SigmaFiniteFiltration μ ℱ
τ : Ω → WithTop ι
f : ι → Ω → E
n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ (↑n : WithTop ι)
inst_8 : SigmaFinite (μ.trim ⋯)
i : ι
hin : ¬i ≤ n
x : Ω
neg : ¬τ x = (↑i : WithTop ι)
⊢ Membership.mem (γ := Set Ω) {x : Ω | τ x = (↑i : WithTop ι)} x ↔ Membership.mem (γ := Set Ω) ∅ x

Tactic:
simp only [Set.mem_setOf_eq, Set.mem_empty_iff_false, iff_false]

Premises used: iff_false, Set.mem_setOf_eq, Set.mem_empty_iff_false
-- Module: Mathlib.Probability.Martingale.OptionalSampling
Goal:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
inst_6 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_7 : SigmaFiniteFiltration μ ℱ
τ : Ω → WithTop ι
f : ι → Ω → E
n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ (↑n : WithTop ι)
inst_8 : SigmaFinite (μ.trim ⋯)
i : ι
hin : ¬i ≤ n
x : Ω
neg : ∀ (hin : τ x = (↑i : WithTop ι)), i ≤ n
⊢ ¬τ x = (↑i : WithTop ι)

Tactic:
contrapose hin
-- Module: Mathlib.Probability.Martingale.OptionalSampling
Goal:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
inst_6 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_7 : SigmaFiniteFiltration μ ℱ
τ : Ω → WithTop ι
f : ι → Ω → E
n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ (↑n : WithTop ι)
inst_8 : SigmaFinite (μ.trim ⋯)
i : ι
x : Ω
hin : τ x = (↑i : WithTop ι)
⊢ i ≤ n

Tactic:
exact_mod_cast hin ▸ hτ_le x
-- Module: Mathlib.Probability.Martingale.OptionalSampling
Goal:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
inst_6 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_7 : SigmaFiniteFiltration μ ℱ
τ : Ω → WithTop ι
f : ι → Ω → E
n : ι
inst_8 : Nonempty ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ (↑n : WithTop ι)
inst_9 : SigmaFinite (μ.trim ⋯)
i : ι
⊢ stoppedValue f τ =ᶠ[ae (μ.restrict {x : Ω | τ x = (↑i : WithTop ι)})] μ[f n | hτ.measurableSpace]

Tactic:
Filter.EventuallyEq.trans ?_
    (condExp_stopping_time_ae_eq_restrict_eq_const_of_le_const h hτ hτ_le i).symm

Premises used: Filter.EventuallyEq.trans, MeasureTheory.Martingale.condExp_stopping_time_ae_eq_restrict_eq_const_of_le_const, Filter.EventuallyEq.symm
-- Module: Mathlib.Probability.Martingale.OptionalSampling
Goal:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
inst_6 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_7 : SigmaFiniteFiltration μ ℱ
τ : Ω → WithTop ι
f : ι → Ω → E
n : ι
inst_8 : Nonempty ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ (↑n : WithTop ι)
inst_9 : SigmaFinite (μ.trim ⋯)
i : ι
refine : stoppedValue f τ =ᶠ[ae (μ.restrict {x : Ω | τ x = (↑i : WithTop ι)})] f i
⊢ stoppedValue f τ =ᶠ[ae (μ.restrict {x : Ω | τ x = (↑i : WithTop ι)})] μ[f n | hτ.measurableSpace]

Tactic:
refine Filter.EventuallyEq.trans ?_
    (condExp_stopping_time_ae_eq_restrict_eq_const_of_le_const h hτ hτ_le i).symm

Premises used: Filter.EventuallyEq.trans, MeasureTheory.Martingale.condExp_stopping_time_ae_eq_restrict_eq_const_of_le_const, Filter.EventuallyEq.symm
-- Module: Mathlib.Probability.Martingale.OptionalSampling
Goal:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
inst_6 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_7 : SigmaFiniteFiltration μ ℱ
τ : Ω → WithTop ι
f : ι → Ω → E
n : ι
inst_8 : Nonempty ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ (↑n : WithTop ι)
inst_9 : SigmaFinite (μ.trim ⋯)
i : ι
rw : ∀ᵐ (x : Ω) ∂μ, Membership.mem (γ := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)} x → stoppedValue f τ x = f i x
⊢ stoppedValue f τ =ᶠ[ae (μ.restrict {x : Ω | τ x = (↑i : WithTop ι)})] f i

Tactic:
rw [Filter.EventuallyEq, ae_restrict_iff' (ℱ.le _ _ (hτ.measurableSet_eq i))]

Premises used: Filter.EventuallyEq, MeasureTheory.IsStoppingTime.measurableSet_eq, MeasureTheory.Filtration.le, MeasureTheory.ae_restrict_iff'
-- Module: Mathlib.Probability.Martingale.OptionalSampling
Goal:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
inst_6 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_7 : SigmaFiniteFiltration μ ℱ
τ : Ω → WithTop ι
f : ι → Ω → E
n : ι
inst_8 : Nonempty ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ (↑n : WithTop ι)
inst_9 : SigmaFinite (μ.trim ⋯)
i : ι
⊢ ∀ᵐ (x : Ω) ∂μ, Membership.mem (γ := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)} x → stoppedValue f τ x = f i x

Tactic:
Filter.Eventually.of_forall fun x hx => ?_

Premises used: Filter.Eventually.of_forall
-- Module: Mathlib.Probability.Martingale.OptionalSampling
Goal:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
inst_6 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_7 : SigmaFiniteFiltration μ ℱ
τ : Ω → WithTop ι
f : ι → Ω → E
n : ι
inst_8 : Nonempty ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ (↑n : WithTop ι)
inst_9 : SigmaFinite (μ.trim ⋯)
i : ι
refine : ∀ (x : Ω) (hx : Membership.mem (γ := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)} x), stoppedValue f τ x = f i x
⊢ ∀ᵐ (x : Ω) ∂μ, Membership.mem (γ := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)} x → stoppedValue f τ x = f i x

Tactic:
refine Filter.Eventually.of_forall fun x hx => ?_

Premises used: Filter.Eventually.of_forall
-- Module: Mathlib.Probability.Martingale.OptionalSampling
Goal:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
inst_6 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_7 : SigmaFiniteFiltration μ ℱ
τ : Ω → WithTop ι
f : ι → Ω → E
n : ι
inst_8 : Nonempty ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ (↑n : WithTop ι)
inst_9 : SigmaFinite (μ.trim ⋯)
i : ι
x : Ω
hx : Membership.mem (γ := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)} x
⊢ τ x = (↑i : WithTop ι)

Tactic:
rw [Set.mem_setOf_eq] at hx

Premises used: Set.mem_setOf_eq
-- Module: Mathlib.Probability.Martingale.OptionalSampling
Goal:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
inst_6 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_7 : SigmaFiniteFiltration μ ℱ
τ : Ω → WithTop ι
f : ι → Ω → E
n : ι
inst_8 : Nonempty ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ (↑n : WithTop ι)
inst_9 : SigmaFinite (μ.trim ⋯)
i : ι
x : Ω
hx : τ x = (↑i : WithTop ι)
⊢ stoppedValue f τ x = f i x

Tactic:
simp [stoppedValue, hx]

Premises used: MeasureTheory.stoppedValue
-- Module: Mathlib.Probability.Martingale.OptionalSampling
Goal:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
inst_6 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_7 : SigmaFiniteFiltration μ ℱ
τ : Ω → WithTop ι
f : ι → Ω → E
n : ι
inst_8 : Nonempty ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ (↑n : WithTop ι)
h_countable_range : (Set.range τ).Countable
inst_9 : SigmaFinite (μ.trim ⋯)
h₁ :
  ∀ (x : Ω),
    Membership.mem (γ := Set Ω) Set.univ x ↔ Membership.mem (γ := Set Ω) (⋃ i ∈ Set.range τ, {x : Ω | τ x = i}) x
⊢ Eq.{u_1 + 1} (α := Set Ω) Set.univ (⋃ i ∈ Set.range τ, {x : Ω | τ x = i})

Tactic:
ext1 x
-- Module: Mathlib.Probability.Martingale.OptionalSampling
Goal:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
inst_6 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_7 : SigmaFiniteFiltration μ ℱ
τ : Ω → WithTop ι
f : ι → Ω → E
n : ι
inst_8 : Nonempty ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ (↑n : WithTop ι)
h_countable_range : (Set.range τ).Countable
inst_9 : SigmaFinite (μ.trim ⋯)
x : Ω
⊢ Membership.mem (γ := Set Ω) Set.univ x ↔ Membership.mem (γ := Set Ω) (⋃ i ∈ Set.range τ, {x : Ω | τ x = i}) x

Tactic:
simp only [Set.mem_univ, Set.mem_range, Set.iUnion_exists, Set.iUnion_iUnion_eq',
      Set.mem_iUnion, Set.mem_setOf_eq, exists_apply_eq_apply']

Premises used: Set.mem_range, Set.mem_iUnion, Set.mem_setOf_eq, exists_apply_eq_apply', Set.mem_univ, Set.iUnion_exists, Set.iUnion_iUnion_eq'
-- Module: Mathlib.Probability.Martingale.OptionalSampling
Goal:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
inst_6 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_7 : SigmaFiniteFiltration μ ℱ
τ : Ω → WithTop ι
f : ι → Ω → E
n : ι
inst_8 : Nonempty ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ (↑n : WithTop ι)
h_countable_range : (Set.range τ).Countable
inst_9 : SigmaFinite (μ.trim ⋯)
⊢ Eq.{u_1 + 1} (α := Set Ω) Set.univ (⋃ i ∈ Set.range τ, {x : Ω | τ x = i})

Tactic:
have : Set.univ = ⋃ i ∈ Set.range τ, {x | τ x = i} := by
    ext1 x
    simp only [Set.mem_univ, Set.mem_range, Set.iUnion_exists, Set.iUnion_iUnion_eq',
      Set.mem_iUnion, Set.mem_setOf_eq, exists_apply_eq_apply']
-- Module: Mathlib.Probability.Martingale.OptionalSampling
Goal:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
inst_6 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_7 : SigmaFiniteFiltration μ ℱ
τ : Ω → WithTop ι
f : ι → Ω → E
n : ι
inst_8 : Nonempty ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ (↑n : WithTop ι)
h_countable_range : (Set.range τ).Countable
inst_9 : SigmaFinite (μ.trim ⋯)
this : Eq.{u_1 + 1} (α := Set Ω) Set.univ (⋃ i ∈ Set.range τ, {x : Ω | τ x = i})
nth_rw : stoppedValue f τ =ᶠ[ae (μ.restrict Set.univ)] μ[f n | hτ.measurableSpace]
⊢ stoppedValue f τ =ᶠ[ae μ] μ[f n | hτ.measurableSpace]

Tactic:
nth_rw 1 [← @Measure.restrict_univ Ω _ μ]

Premises used: MeasureTheory.Measure.restrict_univ
-- Module: Mathlib.Probability.Martingale.OptionalSampling
Goal:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
inst_6 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_7 : SigmaFiniteFiltration μ ℱ
τ : Ω → WithTop ι
f : ι → Ω → E
n : ι
inst_8 : Nonempty ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ (↑n : WithTop ι)
h_countable_range : (Set.range τ).Countable
inst_9 : SigmaFinite (μ.trim ⋯)
this : Eq.{u_1 + 1} (α := Set Ω) Set.univ (⋃ i ∈ Set.range τ, {x : Ω | τ x = i})
rw : ∀ i ∈ Set.range τ, stoppedValue f τ =ᶠ[ae (μ.restrict {x : Ω | τ x = i})] μ[f n | hτ.measurableSpace]
⊢ stoppedValue f τ =ᶠ[ae (μ.restrict Set.univ)] μ[f n | hτ.measurableSpace]

Tactic:
rw [this, ae_eq_restrict_biUnion_iff _ h_countable_range]

Premises used: MeasureTheory.ae_eq_restrict_biUnion_iff