awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalStopping (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
τ π : Ω → ℕ∞
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : IsOrderedModule ℝ E
inst_6 : ClosedIciTopology E
inst_7 : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)
rw :
  LE.le.{u_2} (α := E) 0
    (∫ (a : Ω),
      (fun (ω : Ω) ↦
          ((∑ i ∈ Finset.range (N + 1), Set.indicator {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω} (f (i + 1) - f i)) ω :
            E))
        a ∂μ)
⊢ LE.le.{u_2} (α := E) (∫ (x : Ω), stoppedValue f τ x ∂μ) (∫ (x : Ω), stoppedValue f π x ∂μ)
have hf₁ : Integrable (stoppedValue f π) μ
Tactic: rw [← sub_nonneg, ← integral_sub', stoppedValue_sub_eq_sum' hle hbdd]
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalStopping (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
τ π : Ω → ℕ∞
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : IsOrderedModule ℝ E
inst_6 : ClosedIciTopology E
inst_7 : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)
rw :
  LE.le.{u_2} (α := E) 0
    (∫ (a : Ω),
      (fun (ω : Ω) ↦
          ((∑ i ∈ Finset.range (N + 1), Set.indicator {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω} (f (i + 1) - f i)) ω :
            E))
        a ∂μ)
hf₁ : Integrable (stoppedValue f π) μ
⊢ LE.le.{u_2} (α := E) (∫ (x : Ω), stoppedValue f τ x ∂μ) (∫ (x : Ω), stoppedValue f π x ∂μ)
have hg : Integrable (stoppedValue f τ) μ
Tactic: rw [← sub_nonneg, ← integral_sub', stoppedValue_sub_eq_sum' hle hbdd]
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalStopping (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
τ π : Ω → ℕ∞
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : IsOrderedModule ℝ E
inst_6 : ClosedIciTopology E
inst_7 : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)
⊢ LE.le.{u_2} (α := E) 0
    (∫ (a : Ω),
      (fun (ω : Ω) ↦
          ((∑ i ∈ Finset.range (N + 1), Set.indicator {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω} (f (i + 1) - f i)) ω :
            E))
        a ∂μ)
have simp : LE.le.{u_2} (α := E) 0
  (∫ (a : Ω),
    ∑ c ∈ Finset.range (N + 1), Set.indicator {ω : Ω | τ ω ≤ (↑c : ℕ∞) ∧ (↑c : ℕ∞) < π ω} (f (c + 1) - f c) a ∂μ)
Tactic: simp only [Finset.sum_apply]
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalStopping (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
τ π : Ω → ℕ∞
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : IsOrderedModule ℝ E
inst_6 : ClosedIciTopology E
inst_7 : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)
i : ℕ
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω}
have refine : MeasurableSet.{u_1} (α := Ω) fun (ω : Ω) ↦ WithBot.LT (π ω) (↑i : ℕ∞)
Tactic: refine (hτ i).inter ?_
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalStopping (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
τ π : Ω → ℕ∞
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : IsOrderedModule ℝ E
inst_6 : ClosedIciTopology E
inst_7 : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)
i : ℕ
⊢ MeasurableSet.{u_1} (α := Ω) fun (ω : Ω) ↦ WithBot.LT (π ω) (↑i : ℕ∞)
have h : Eq.{u_1 + 1} (α := Set Ω) (fun (ω : Ω) ↦ WithBot.LT (π ω) (↑i : ℕ∞)) {ω : Ω | π ω ≤ (↑i : WithTop ℕ)}ᶜ
Tactic: convert! (hπ i).compl using 1
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalStopping (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
τ π : Ω → ℕ∞
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : IsOrderedModule ℝ E
inst_6 : ClosedIciTopology E
inst_7 : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)
i : ℕ
⊢ Eq.{u_1 + 1} (α := Set Ω) (fun (ω : Ω) ↦ WithBot.LT (π ω) (↑i : ℕ∞)) {ω : Ω | π ω ≤ (↑i : WithTop ℕ)}ᶜ
have h : ∀ (x : Ω),
  Membership.mem (γ := Set Ω) (fun (ω : Ω) ↦ WithBot.LT (π ω) (↑i : ℕ∞)) x ↔
    Membership.mem (γ := Set Ω) {ω : Ω | π ω ≤ (↑i : WithTop ℕ)}ᶜ x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalStopping (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
τ π : Ω → ℕ∞
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : IsOrderedModule ℝ E
inst_6 : ClosedIciTopology E
inst_7 : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)
i : ℕ
x : Ω
⊢ Membership.mem (γ := Set Ω) (fun (ω : Ω) ↦ WithBot.LT (π ω) (↑i : ℕ∞)) x ↔
    Membership.mem (γ := Set Ω) {ω : Ω | π ω ≤ (↑i : WithTop ℕ)}ᶜ x
have h : Membership.mem (γ := Set Ω) (fun (ω : Ω) ↦ WithBot.LT (π ω) (↑i : ℕ∞)) x ↔ (↑i : WithTop ℕ) < π x
Tactic: simp
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalStopping (hypothesis)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
τ π : Ω → ℕ∞
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : IsOrderedModule ℝ E
inst_6 : ClosedIciTopology E
inst_7 : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)
⊢ LE.le.{u_2} (α := E) 0
    (∫ (a : Ω),
      ∑ c ∈ Finset.range (N + 1), Set.indicator {ω : Ω | τ ω ≤ (↑c : ℕ∞) ∧ (↑c : ℕ∞) < π ω} (f (c + 1) - f c) a ∂μ)
have this : ∀ (i : ℕ), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω}
Tactic: have : ∀ i, MeasurableSet[𝒢 i] {ω : Ω | τ ω ≤ i ∧ i < π ω} := by
      intro i
      refine (hτ i).inter ?_
      convert! (hπ i).compl using 1
      ext x
      simp; rfl
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalStopping (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
τ π : Ω → ℕ∞
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : IsOrderedModule ℝ E
inst_6 : ClosedIciTopology E
inst_7 : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)
this : ∀ (i : ℕ), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω}
⊢ LE.le.{u_2} (α := E) 0
    (∫ (a : Ω),
      ∑ c ∈ Finset.range (N + 1), Set.indicator {ω : Ω | τ ω ≤ (↑c : ℕ∞) ∧ (↑c : ℕ∞) < π ω} (f (c + 1) - f c) a ∂μ)
have rw : LE.le.{u_2} (α := E) 0
  (∑ i ∈ Finset.range (N + 1),
    ∫ (a : Ω), Set.indicator {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω} (f (i + 1) - f i) a ∂μ)
Tactic: rw [integral_finsetSum]
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalStopping (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
τ π : Ω → ℕ∞
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : IsOrderedModule ℝ E
inst_6 : ClosedIciTopology E
inst_7 : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)
this : ∀ (i : ℕ), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω}
rw :
  LE.le.{u_2} (α := E) 0
    (∑ i ∈ Finset.range (N + 1),
      ∫ (a : Ω), Set.indicator {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω} (f (i + 1) - f i) a ∂μ)
⊢ LE.le.{u_2} (α := E) 0
    (∫ (a : Ω),
      ∑ c ∈ Finset.range (N + 1), Set.indicator {ω : Ω | τ ω ≤ (↑c : ℕ∞) ∧ (↑c : ℕ∞) < π ω} (f (c + 1) - f c) a ∂μ)
have hf₁ : ∀ i ∈ Finset.range (N + 1), Integrable (Set.indicator {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω} (f (i + 1) - f i)) μ
Tactic: rw [integral_finsetSum]
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalStopping (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
τ π : Ω → ℕ∞
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : IsOrderedModule ℝ E
inst_6 : ClosedIciTopology E
inst_7 : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)
this : ∀ (i : ℕ), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω}
⊢ LE.le.{u_2} (α := E) 0
    (∑ i ∈ Finset.range (N + 1),
      ∫ (a : Ω), Set.indicator {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω} (f (i + 1) - f i) a ∂μ)
have refine : ∀ i ∈ Finset.range (N + 1),
  LE.le.{u_2} (α := E) 0 (∫ (a : Ω), Set.indicator {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω} (f (i + 1) - f i) a ∂μ)
Tactic: refine Finset.sum_nonneg fun i _ => ?_
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalStopping (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
τ π : Ω → ℕ∞
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : IsOrderedModule ℝ E
inst_6 : ClosedIciTopology E
inst_7 : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)
this : ∀ (i : ℕ), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω}
i : ℕ
h : i ∈ Finset.range (N + 1)
⊢ LE.le.{u_2} (α := E) 0 (∫ (a : Ω), Set.indicator {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω} (f (i + 1) - f i) a ∂μ)
have rw : LE.le.{u_2} (α := E) (∫ (a : Ω) in {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω}, f i a ∂μ)
  (∫ (a : Ω) in {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω}, f (i + 1) a ∂μ)
Tactic: rw [integral_indicator (𝒢.le _ _ (this _)), integral_sub', sub_nonneg]
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalStopping (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
τ π : Ω → ℕ∞
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : IsOrderedModule ℝ E
inst_6 : ClosedIciTopology E
inst_7 : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)
this : ∀ (i : ℕ), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω}
i : ℕ
h : i ∈ Finset.range (N + 1)
rw :
  LE.le.{u_2} (α := E) (∫ (a : Ω) in {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω}, f i a ∂μ)
    (∫ (a : Ω) in {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω}, f (i + 1) a ∂μ)
⊢ LE.le.{u_2} (α := E) 0 (∫ (a : Ω), Set.indicator {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω} (f (i + 1) - f i) a ∂μ)
have hf₁ : Integrable (f (i + 1)) (μ.restrict {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω})
Tactic: rw [integral_indicator (𝒢.le _ _ (this _)), integral_sub', sub_nonneg]
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalStopping (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
τ π : Ω → ℕ∞
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : IsOrderedModule ℝ E
inst_6 : ClosedIciTopology E
inst_7 : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)
this : ∀ (i : ℕ), MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω}
i : ℕ
h : i ∈ Finset.range (N + 1)
rw :
  LE.le.{u_2} (α := E) (∫ (a : Ω) in {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω}, f i a ∂μ)
    (∫ (a : Ω) in {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω}, f (i + 1) a ∂μ)
hf₁ : Integrable (f (i + 1)) (μ.restrict {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω})
⊢ LE.le.{u_2} (α := E) 0 (∫ (a : Ω), Set.indicator {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω} (f (i + 1) - f i) a ∂μ)
have hg : Integrable (f i) (μ.restrict {ω : Ω | τ ω ≤ (↑i : ℕ∞) ∧ (↑i : ℕ∞) < π ω})
Tactic: rw [integral_indicator (𝒢.le _ _ (this _)), integral_sub', sub_nonneg]
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalStopping (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : SigmaFiniteFiltration μ 𝒢
hadp : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf :
  ∀ (τ π : Ω → ℕ∞),
    IsStoppingTime 𝒢 τ →
      IsStoppingTime 𝒢 π →
        τ ≤ π →
          (∃ (N : ℕ), ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)) →
            LE.le (α := ℝ) (∫ (x : Ω), stoppedValue f τ x ∂μ) (∫ (x : Ω), stoppedValue f π x ∂μ)
⊢ Submartingale f 𝒢 μ
have refine : ∀ (i j : ℕ) (hij : i ≤ j) (s : Set Ω) (hs : MeasurableSet s),
  LE.le (α := ℝ) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (ω : Ω) in s, f j ω ∂μ)
Tactic: refine submartingale_of_setIntegral_le hadp hint fun i j hij s hs => ?_
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalStopping (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : SigmaFiniteFiltration μ 𝒢
hadp : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf :
  ∀ (τ π : Ω → ℕ∞),
    IsStoppingTime 𝒢 τ →
      IsStoppingTime 𝒢 π →
        τ ≤ π →
          (∃ (N : ℕ), ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)) →
            LE.le (α := ℝ) (∫ (x : Ω), stoppedValue f τ x ∂μ) (∫ (x : Ω), stoppedValue f π x ∂μ)
i j : ℕ
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
⊢ LE.le (α := ℝ) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (ω : Ω) in s, f j ω ∂μ)
have specialize : LE.le (α := Ω → ℕ∞) (s.piecewise (β := fun (a : Ω) ↦ ℕ∞) (fun (x : Ω) ↦ (↑i : ℕ∞)) fun (x : Ω) ↦ (↑j : ℕ∞))
  fun (x : Ω) ↦ (↑j : WithTop ℕ)
Tactic: specialize hf (s.piecewise (fun _ => i) fun _ => j) _ (isStoppingTime_piecewise_const hij hs)
    (isStoppingTime_const 𝒢 j) ?_
    ⟨j, fun _ => le_rfl⟩
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalStopping (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : SigmaFiniteFiltration μ 𝒢
hadp : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf :
  ∀ (τ π : Ω → ℕ∞),
    IsStoppingTime 𝒢 τ →
      IsStoppingTime 𝒢 π →
        τ ≤ π →
          (∃ (N : ℕ), ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)) →
            LE.le (α := ℝ) (∫ (x : Ω), stoppedValue f τ x ∂μ) (∫ (x : Ω), stoppedValue f π x ∂μ)
i j : ℕ
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
specialize :
  LE.le (α := Ω → ℕ∞) (s.piecewise (β := fun (a : Ω) ↦ ℕ∞) (fun (x : Ω) ↦ (↑i : ℕ∞)) fun (x : Ω) ↦ (↑j : ℕ∞))
    fun (x : Ω) ↦ (↑j : WithTop ℕ)
⊢ LE.le (α := ℝ) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (ω : Ω) in s, f j ω ∂μ)
have specialize₁ : ∀
  (hf :
    LE.le (α := ℝ)
      (∫ (x : Ω),
        stoppedValue f (s.piecewise (β := fun (a : Ω) ↦ ℕ∞) (fun (x : Ω) ↦ (↑i : ℕ∞)) fun (x : Ω) ↦ (↑j : ℕ∞)) x ∂μ)
      (∫ (x : Ω), stoppedValue f (fun (x : Ω) ↦ (↑j : WithTop ℕ)) x ∂μ)),
  LE.le (α := ℝ) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (ω : Ω) in s, f j ω ∂μ)
Tactic: specialize hf (s.piecewise (fun _ => i) fun _ => j) _ (isStoppingTime_piecewise_const hij hs)
    (isStoppingTime_const 𝒢 j) ?_
    ⟨j, fun _ => le_rfl⟩
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalStopping (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : SigmaFiniteFiltration μ 𝒢
hadp : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf :
  ∀ (τ π : Ω → ℕ∞),
    IsStoppingTime 𝒢 τ →
      IsStoppingTime 𝒢 π →
        τ ≤ π →
          (∃ (N : ℕ), ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)) →
            LE.le (α := ℝ) (∫ (x : Ω), stoppedValue f τ x ∂μ) (∫ (x : Ω), stoppedValue f π x ∂μ)
i j : ℕ
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
ω : Ω
⊢ LE.le (α := (fun (a : Ω) ↦ ℕ∞) ω)
    (s.piecewise (β := fun (a : Ω) ↦ ℕ∞) (fun (x : Ω) ↦ (↑i : ℕ∞)) (fun (x : Ω) ↦ (↑j : ℕ∞)) ω : ℕ∞)
    ((fun (x : Ω) ↦ (↑j : WithTop ℕ)) ω : WithTop ℕ)
have simp : LE.le (α := ℕ∞) (if ω ∈ s then (↑i : ℕ∞) else (↑j : ℕ∞)) (↑j : WithTop ℕ)
Tactic: simp only [Set.piecewise, ENat.some_eq_coe]
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalStopping (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : SigmaFiniteFiltration μ 𝒢
hadp : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf :
  ∀ (τ π : Ω → ℕ∞),
    IsStoppingTime 𝒢 τ →
      IsStoppingTime 𝒢 π →
        τ ≤ π →
          (∃ (N : ℕ), ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)) →
            LE.le (α := ℝ) (∫ (x : Ω), stoppedValue f τ x ∂μ) (∫ (x : Ω), stoppedValue f π x ∂μ)
i j : ℕ
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
ω : Ω
⊢ LE.le (α := ℕ∞) (if ω ∈ s then (↑i : ℕ∞) else (↑j : ℕ∞)) (↑j : WithTop ℕ)
have pos : ∀ (hω : ω ∈ s), LE.le (α := ℕ∞) (↑i : ℕ∞) (↑j : WithTop ℕ)
Tactic: split_ifs with hω
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalStopping (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : SigmaFiniteFiltration μ 𝒢
hadp : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf :
  ∀ (τ π : Ω → ℕ∞),
    IsStoppingTime 𝒢 τ →
      IsStoppingTime 𝒢 π →
        τ ≤ π →
          (∃ (N : ℕ), ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)) →
            LE.le (α := ℝ) (∫ (x : Ω), stoppedValue f τ x ∂μ) (∫ (x : Ω), stoppedValue f π x ∂μ)
i j : ℕ
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
ω : Ω
pos : ∀ (hω : ω ∈ s), LE.le (α := ℕ∞) (↑i : ℕ∞) (↑j : WithTop ℕ)
⊢ LE.le (α := ℕ∞) (if ω ∈ s then (↑i : ℕ∞) else (↑j : ℕ∞)) (↑j : WithTop ℕ)
have neg : ∀ (hω : ω ∉ s), LE.le (α := ℕ∞) (↑j : ℕ∞) (↑j : WithTop ℕ)
Tactic: split_ifs with hω
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalStopping (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : SigmaFiniteFiltration μ 𝒢
hadp : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf :
  ∀ (τ π : Ω → ℕ∞),
    IsStoppingTime 𝒢 τ →
      IsStoppingTime 𝒢 π →
        τ ≤ π →
          (∃ (N : ℕ), ∀ (ω : Ω), π ω ≤ (↑N : ℕ∞)) →
            LE.le (α := ℝ) (∫ (x : Ω), stoppedValue f τ x ∂μ) (∫ (x : Ω), stoppedValue f π x ∂μ)
i j : ℕ
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
ω : Ω
hω : ω ∉ s
⊢ LE.le (α := ℕ∞) (↑j : ℕ∞) (↑j : WithTop ℕ)
have neg : j ≤ j
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalStopping (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : SigmaFiniteFiltration μ 𝒢
hadp : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
i j : ℕ
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
hf :
  LE.le (α := ℝ)
    (∫ (x : Ω),
      stoppedValue f (s.piecewise (β := fun (a : Ω) ↦ ℕ∞) (fun (x : Ω) ↦ (↑i : ℕ∞)) fun (x : Ω) ↦ (↑j : ℕ∞)) x ∂μ)
    (∫ (x : Ω), stoppedValue f (fun (x : Ω) ↦ (↑j : WithTop ℕ)) x ∂μ)
⊢ LE.le (α := ℝ) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (ω : Ω) in s, f j ω ∂μ)
have rwa : ∀
  (hf :
    LE.le (α := ℝ)
      (∫ (x : Ω),
        stoppedValue f (s.piecewise (β := fun (a : Ω) ↦ ℕ∞) (fun (x : Ω) ↦ (↑i : ℕ∞)) fun (x : Ω) ↦ (↑j : ℕ∞)) x ∂μ)
      (∫ (x : Ω), f j x ∂μ)),
  LE.le (α := ℝ) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (ω : Ω) in s, f j ω ∂μ)
Tactic: rwa [stoppedValue_const, ← ENat.some_eq_coe, stoppedValue_piecewise_const,
      integral_piecewise (𝒢.le _ _ hs) (hint _).integrableOn (hint _).integrableOn, ←
      integral_add_compl (𝒢.le _ _ hs) (hint j), add_le_add_iff_right] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalStopping (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : SigmaFiniteFiltration μ 𝒢
hadp : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
i j : ℕ
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
hf :
  LE.le (α := ℝ)
    (∫ (x : Ω),
      stoppedValue f (s.piecewise (β := fun (a : Ω) ↦ ℕ∞) (fun (x : Ω) ↦ (↑i : ℕ∞)) fun (x : Ω) ↦ (↑j : ℕ∞)) x ∂μ)
    (∫ (x : Ω), stoppedValue f (fun (x : Ω) ↦ (↑j : WithTop ℕ)) x ∂μ)
rwa :
  ∀
    (hf :
      LE.le (α := ℝ)
        (∫ (x : Ω),
          stoppedValue f (s.piecewise (β := fun (a : Ω) ↦ ℕ∞) (fun (x : Ω) ↦ (↑i : ℕ∞)) fun (x : Ω) ↦ (↑j : ℕ∞)) x ∂μ)
        (∫ (x : Ω), f j x ∂μ)),
    LE.le (α := ℝ) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (ω : Ω) in s, f j ω ∂μ)
⊢ LE.le (α := ℝ) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (ω : Ω) in s, f j ω ∂μ)
have rwa₁ : ∀
  (hf :
    LE.le (α := ℝ)
      (∫ (x : Ω),
        stoppedValue f
          (s.piecewise (β := fun (a : Ω) ↦ ℕ∞) (fun (x : Ω) ↦ (↑i : WithTop ℕ)) fun (x : Ω) ↦ (↑j : WithTop ℕ)) x ∂μ)
      (∫ (x : Ω), f j x ∂μ)),
  LE.le (α := ℝ) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (ω : Ω) in s, f j ω ∂μ)
Tactic: rwa [stoppedValue_const, ← ENat.some_eq_coe, stoppedValue_piecewise_const,
      integral_piecewise (𝒢.le _ _ hs) (hint _).integrableOn (hint _).integrableOn, ←
      integral_add_compl (𝒢.le _ _ hs) (hint j), add_le_add_iff_right] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalStopping (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : SigmaFiniteFiltration μ 𝒢
hadp : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
i j : ℕ
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
hf :
  LE.le (α := ℝ)
    (∫ (x : Ω),
      stoppedValue f (s.piecewise (β := fun (a : Ω) ↦ ℕ∞) (fun (x : Ω) ↦ (↑i : ℕ∞)) fun (x : Ω) ↦ (↑j : ℕ∞)) x ∂μ)
    (∫ (x : Ω), stoppedValue f (fun (x : Ω) ↦ (↑j : WithTop ℕ)) x ∂μ)
rwa :
  ∀
    (hf :
      LE.le (α := ℝ)
        (∫ (x : Ω),
          stoppedValue f (s.piecewise (β := fun (a : Ω) ↦ ℕ∞) (fun (x : Ω) ↦ (↑i : ℕ∞)) fun (x : Ω) ↦ (↑j : ℕ∞)) x ∂μ)
        (∫ (x : Ω), f j x ∂μ)),
    LE.le (α := ℝ) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (ω : Ω) in s, f j ω ∂μ)
rwa₁ :
  ∀
    (hf :
      LE.le (α := ℝ)
        (∫ (x : Ω),
          stoppedValue f
            (s.piecewise (β := fun (a : Ω) ↦ ℕ∞) (fun (x : Ω) ↦ (↑i : WithTop ℕ)) fun (x : Ω) ↦ (↑j : WithTop ℕ)) x ∂μ)
        (∫ (x : Ω), f j x ∂μ)),
    LE.le (α := ℝ) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (ω : Ω) in s, f j ω ∂μ)
⊢ LE.le (α := ℝ) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (ω : Ω) in s, f j ω ∂μ)
have rwa₂ : ∀ (hf : LE.le (α := ℝ) (∫ (x : Ω), s.piecewise (β := fun (i : Ω) ↦ ℝ) (f i) (f j) x ∂μ) (∫ (x : Ω), f j x ∂μ)),
  LE.le (α := ℝ) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (ω : Ω) in s, f j ω ∂μ)
Tactic: rwa [stoppedValue_const, ← ENat.some_eq_coe, stoppedValue_piecewise_const,
      integral_piecewise (𝒢.le _ _ hs) (hint _).integrableOn (hint _).integrableOn, ←
      integral_add_compl (𝒢.le _ _ hs) (hint j), add_le_add_iff_right] at hf
Cleared hypotheses: hf