awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
g : Ω → ℝ
ht :
  Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦
      eLpNorm
        (μ[μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n] | (↑ℱ : ℕ → MeasurableSpace Ω) n] -
          μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n])
        1 μ)
    atTop (𝓝 0)
heq :
  ∀ (n : ℕ),
    ∀ᵐ (x : Ω) ∂μ,
      μ[μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n] | (↑ℱ : ℕ → MeasurableSpace Ω) n] x =
        μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x
⊢ Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦
      eLpNorm (μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] - μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n]) 1 μ)
    atTop (𝓝 0)
have refine : ∀ (n : ℕ),
  μ[μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n] | (↑ℱ : ℕ → MeasurableSpace Ω) n] -
      μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n] =ᶠ[ae μ]
    μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] - μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n]
Tactic: refine ht.congr fun n => eLpNorm_congr_ae ?_
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
g : Ω → ℝ
ht :
  Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦
      eLpNorm
        (μ[μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n] | (↑ℱ : ℕ → MeasurableSpace Ω) n] -
          μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n])
        1 μ)
    atTop (𝓝 0)
heq :
  ∀ (n : ℕ),
    ∀ᵐ (x : Ω) ∂μ,
      μ[μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n] | (↑ℱ : ℕ → MeasurableSpace Ω) n] x =
        μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x
n : ℕ
⊢ μ[μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n] | (↑ℱ : ℕ → MeasurableSpace Ω) n] -
      μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n] =ᶠ[ae μ]
    μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] - μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n]
have h : ∀ (x : Ω)
  (hxeq :
    μ[μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n] | (↑ℱ : ℕ → MeasurableSpace Ω) n] x =
      μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x),
  (μ[μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n] | (↑ℱ : ℕ → MeasurableSpace Ω) n] -
        μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n])
      x =
    (μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] - μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n]) x
Tactic: filter_upwards [heq n] with x hxeq
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalSampling (goal)
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
⊢ μ[f n | hτ.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x = (↑i : WithTop ι)})] f i
have refine : μ[f n | hτ.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x = (↑i : WithTop ι)})] μ[f n | (↑ℱ : ι → MeasurableSpace Ω) i]
Tactic: refine Filter.EventuallyEq.trans ?_ (ae_restrict_of_ae (h.condExp_ae_eq hin))
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalSampling (goal)
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
⊢ μ[f n | hτ.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x = (↑i : WithTop ι)})]
    μ[f n | (↑ℱ : ι → MeasurableSpace Ω) i]
have refine : ∀ (t : Set Ω),
  MeasurableSet ({x : Ω | τ x = (↑i : WithTop ι)} ∩ t) ↔ MeasurableSet ({x : Ω | τ x = (↑i : WithTop ι)} ∩ t)
Tactic: refine condExp_ae_eq_restrict_of_measurableSpace_eq_on hτ.measurableSpace_le (ℱ.le i)
    (hτ.measurableSet_eq' i) fun t => ?_
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalSampling (goal)
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 Ω
⊢ MeasurableSet ({x : Ω | τ x = (↑i : WithTop ι)} ∩ t) ↔ MeasurableSet ({x : Ω | τ x = (↑i : WithTop ι)} ∩ t)
have rw : MeasurableSet (t ∩ {x : Ω | τ x = (↑i : WithTop ι)}) ↔ MeasurableSet (t ∩ {x : Ω | τ x = (↑i : WithTop ι)})
Tactic: rw [Set.inter_comm _ t, IsStoppingTime.measurableSet_inter_eq_iff]
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalSampling (goal)
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 ι)})
⊢ MeasurableSet ({x : Ω | τ x = (↑i : WithTop ι)} ∩ t) ↔ MeasurableSet ({x : Ω | τ x = (↑i : WithTop ι)} ∩ t)
have rw₁ : MeasurableSet (t ∩ {ω : Ω | τ ω = (↑i : WithTop ι)}) ↔ MeasurableSet (t ∩ {x : Ω | τ x = (↑i : WithTop ι)})
Tactic: rw [Set.inter_comm _ t, IsStoppingTime.measurableSet_inter_eq_iff]
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalSampling (goal)
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 : ι
⊢ μ[f n | hτ.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x = (↑i : WithTop ι)})] f i
have pos : ∀ (hin : i ≤ n), μ[f n | hτ.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x = (↑i : WithTop ι)})] f i
Tactic: by_cases hin : i ≤ n
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalSampling (goal)
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
⊢ μ[f n | hτ.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x = (↑i : WithTop ι)})] f i
have neg : ∀ (hin : ¬i ≤ n), μ[f n | hτ.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x = (↑i : WithTop ι)})] f i
Tactic: by_cases hin : i ≤ n
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalSampling (goal)
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
have pos : μ[f n | hτ.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x = (↑i : WithTop ι)})] μ[f n | (↑ℱ : ι → MeasurableSpace Ω) i]
Tactic: refine Filter.EventuallyEq.trans ?_ (ae_restrict_of_ae (h.condExp_ae_eq hin))
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalSampling (goal)
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]
have pos : ∀ (t : Set Ω),
  MeasurableSet ({x : Ω | τ x = (↑i : WithTop ι)} ∩ t) ↔ MeasurableSet ({x : Ω | τ x = (↑i : WithTop ι)} ∩ t)
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 => ?_
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalSampling (goal)
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 Ω
⊢ MeasurableSet ({x : Ω | τ x = (↑i : WithTop ι)} ∩ t) ↔ MeasurableSet ({x : Ω | τ x = (↑i : WithTop ι)} ∩ t)
have pos : MeasurableSet (t ∩ {x : Ω | τ x = (↑i : WithTop ι)}) ↔ MeasurableSet (t ∩ {x : Ω | τ x = (↑i : WithTop ι)})
Tactic: rw [Set.inter_comm _ t, IsStoppingTime.measurableSet_inter_eq_iff]
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalSampling (goal)
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 ι)})
⊢ MeasurableSet ({x : Ω | τ x = (↑i : WithTop ι)} ∩ t) ↔ MeasurableSet ({x : Ω | τ x = (↑i : WithTop ι)} ∩ t)
have pos₁ : MeasurableSet (t ∩ {ω : Ω | τ ω = (↑i : WithTop ι)}) ↔ MeasurableSet (t ∩ {x : Ω | τ x = (↑i : WithTop ι)})
Tactic: rw [Set.inter_comm _ t, IsStoppingTime.measurableSet_inter_eq_iff]
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalSampling (goal)
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] =ᶠ[ae (μ.restrict {x : Ω | τ x = (↑i : WithTop ι)})] f i
have simp : μ[f n | hτ.measurableSpace] =ᶠ[⊥] f i
Tactic: simp [this]
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalSampling (goal)
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
have neg : Eq.{u_1 + 1} (α := Set Ω) {x : Ω | τ x = (↑i : WithTop ι)} ∅
Tactic: suffices {x : Ω | τ x = i} = ∅ by simp [this]; norm_cast
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalSampling (goal)
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
⊢ Eq.{u_1 + 1} (α := Set Ω) {x : Ω | τ x = (↑i : WithTop ι)} ∅
have neg : ∀ (x : Ω), Membership.mem (γ := Set Ω) {x : Ω | τ x = (↑i : WithTop ι)} x ↔ Membership.mem (γ := Set Ω) ∅ x
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalSampling (goal)
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 : Ω
⊢ Membership.mem (γ := Set Ω) {x : Ω | τ x = (↑i : WithTop ι)} x ↔ Membership.mem (γ := Set Ω) ∅ x
have neg : ¬τ x = (↑i : WithTop ι)
Tactic: simp only [Set.mem_setOf_eq, Set.mem_empty_iff_false, iff_false]
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalSampling (goal)
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 : Ω
⊢ ¬τ x = (↑i : WithTop ι)
have neg : ∀ (hin : τ x = (↑i : WithTop ι)), i ≤ n
Tactic: contrapose hin
Cleared hypotheses: hin
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalSampling (goal)
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]
have refine : stoppedValue f τ =ᶠ[ae (μ.restrict {x : Ω | τ x = (↑i : WithTop ι)})] f i
Tactic: refine Filter.EventuallyEq.trans ?_
    (condExp_stopping_time_ae_eq_restrict_eq_const_of_le_const h hτ hτ_le i).symm
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalSampling (goal)
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 i
have rw : ∀ᵐ (x : Ω) ∂μ, Membership.mem (γ := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)} x → stoppedValue f τ x = f i x
Tactic: rw [Filter.EventuallyEq, ae_restrict_iff' (ℱ.le _ _ (hτ.measurableSet_eq i))]
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalSampling (goal)
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
have refine : ∀ (x : Ω) (hx : Membership.mem (γ := Set Ω) {ω : Ω | τ ω = (↑i : WithTop ι)} x), stoppedValue f τ x = f i x
Tactic: refine Filter.Eventually.of_forall fun x hx => ?_
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalSampling (hypothesis)
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
⊢ stoppedValue f τ x = f i x
have hx₁ : τ x = (↑i : WithTop ι)
Tactic: rw [Set.mem_setOf_eq] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalSampling (goal)
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})
have h₁ : ∀ (x : Ω), Membership.mem (γ := Set Ω) Set.univ x ↔ Membership.mem (γ := Set Ω) (⋃ i ∈ Set.range τ, {x : Ω | τ x = i}) x
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalSampling (hypothesis)
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 ⋯)
⊢ stoppedValue f τ =ᶠ[ae μ] μ[f n | hτ.measurableSpace]
have this : 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']
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalSampling (goal)
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})
⊢ stoppedValue f τ =ᶠ[ae μ] μ[f n | hτ.measurableSpace]
have nth_rw : stoppedValue f τ =ᶠ[ae (μ.restrict Set.univ)] μ[f n | hτ.measurableSpace]
Tactic: nth_rw 1 [← @Measure.restrict_univ Ω _ μ]
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalSampling (goal)
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})
⊢ stoppedValue f τ =ᶠ[ae (μ.restrict Set.univ)] μ[f n | hτ.measurableSpace]
have rw : ∀ i ∈ Set.range τ, stoppedValue f τ =ᶠ[ae (μ.restrict {x : Ω | τ x = i})] μ[f n | hτ.measurableSpace]
Tactic: rw [this, ae_eq_restrict_biUnion_iff _ h_countable_range]
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalSampling (hypothesis)
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_1 : 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})
i : WithTop ι
hi : i ∈ Set.range τ
h : i = ⊤
⊢ False
have hi₁ : ∃ (y : Ω), τ y = ⊤
Tactic: simp only [h, Set.mem_range] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalSampling (goal)
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_1 : 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})
i : WithTop ι
h : i = ⊤
hi : ∃ (y : Ω), τ y = ⊤
⊢ False
have obtain : ∀ (ω : Ω) (hω : τ ω = ⊤), False
Tactic: obtain ⟨ω, hω⟩ := hi
Cleared hypotheses: hi