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
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 ω ∂μ)
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 ω ∂μ)
⊢ LE.le (α := ℝ) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (ω : Ω) in s, f j ω ∂μ)
have rwa₃ : ∀ (hf : HAdd.hAdd (α := ℝ) (∫ (x : Ω) in s, f i x ∂μ) (∫ (x : Ω) in sᶜ, 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
-- 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 ω ∂μ)
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 ω ∂μ)
rwa₃ :
  ∀ (hf : HAdd.hAdd (α := ℝ) (∫ (x : Ω) in s, f i x ∂μ) (∫ (x : Ω) in sᶜ, f 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 :
    HAdd.hAdd (α := ℝ) (∫ (x : Ω) in s, f i x ∂μ) (∫ (x : Ω) in sᶜ, f j x ∂μ) ≤
      HAdd.hAdd (α := ℝ) (∫ (x : Ω) in s, f j x ∂μ) (∫ (x : Ω) in sᶜ, 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 ω ∂μ)
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 ω ∂μ)
rwa₃ :
  ∀ (hf : HAdd.hAdd (α := ℝ) (∫ (x : Ω) in s, f i x ∂μ) (∫ (x : Ω) in sᶜ, f j x ∂μ) ≤ ∫ (x : Ω), f j x ∂μ),
    LE.le (α := ℝ) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (ω : Ω) in s, f j ω ∂μ)
rwa₄ :
  ∀
    (hf :
      HAdd.hAdd (α := ℝ) (∫ (x : Ω) in s, f i x ∂μ) (∫ (x : Ω) in sᶜ, f j x ∂μ) ≤
        HAdd.hAdd (α := ℝ) (∫ (x : Ω) in s, f j x ∂μ) (∫ (x : Ω) in sᶜ, 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 : Ω) in s, f i x ∂μ) (∫ (x : Ω) in s, 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) μ
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: classical
  specialize hf (s.piecewise (fun _ => i) fun _ => j) _ (isStoppingTime_piecewise_const hij hs)
    (isStoppingTime_const 𝒢 j) ?_
    ⟨j, fun _ => le_rfl⟩
  · intro ω
    simp only [Set.piecewise, ENat.some_eq_coe]
    split_ifs with hω
    · exact mod_cast hij
    · norm_cast
  · 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
-- 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: classical
  specialize hf (s.piecewise (fun _ => i) fun _ => j) _ (isStoppingTime_piecewise_const hij hs)
    (isStoppingTime_const 𝒢 j) ?_
    ⟨j, fun _ => le_rfl⟩
  · intro ω
    simp only [Set.piecewise, ENat.some_eq_coe]
    split_ifs with hω
    · exact mod_cast hij
    · norm_cast
  · 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 μ 𝒢
h : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
⊢ Submartingale (stoppedProcess f τ) 𝒢 μ
have rw : ∀ (τ_1 π : Ω → ℕ∞),
  IsStoppingTime 𝒢 τ_1 →
    IsStoppingTime 𝒢 π →
      τ_1 ≤ π →
        (∃ (N : ℕ), ∀ (x : Ω), π x ≤ (↑N : ℕ∞)) →
          LE.le (α := ℝ) (∫ (x : Ω), stoppedValue (stoppedProcess f τ) τ_1 x ∂μ)
            (∫ (x : Ω), stoppedValue (stoppedProcess f τ) π x ∂μ)
Tactic: rw [submartingale_iff_expected_stoppedValue_mono]
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalStopping (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ : Ω → ℕ∞
inst : SigmaFiniteFiltration μ 𝒢
h : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
rw :
  ∀ (τ_1 π : Ω → ℕ∞),
    IsStoppingTime 𝒢 τ_1 →
      IsStoppingTime 𝒢 π →
        τ_1 ≤ π →
          (∃ (N : ℕ), ∀ (x : Ω), π x ≤ (↑N : ℕ∞)) →
            LE.le (α := ℝ) (∫ (x : Ω), stoppedValue (stoppedProcess f τ) τ_1 x ∂μ)
              (∫ (x : Ω), stoppedValue (stoppedProcess f τ) π x ∂μ)
⊢ Submartingale (stoppedProcess f τ) 𝒢 μ
have hadp : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) 𝒢 (stoppedProcess f τ)
Tactic: rw [submartingale_iff_expected_stoppedValue_mono]
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalStopping (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ : Ω → ℕ∞
inst : SigmaFiniteFiltration μ 𝒢
h : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
rw :
  ∀ (τ_1 π : Ω → ℕ∞),
    IsStoppingTime 𝒢 τ_1 →
      IsStoppingTime 𝒢 π →
        τ_1 ≤ π →
          (∃ (N : ℕ), ∀ (x : Ω), π x ≤ (↑N : ℕ∞)) →
            LE.le (α := ℝ) (∫ (x : Ω), stoppedValue (stoppedProcess f τ) τ_1 x ∂μ)
              (∫ (x : Ω), stoppedValue (stoppedProcess f τ) π x ∂μ)
hadp : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) 𝒢 (stoppedProcess f τ)
⊢ Submartingale (stoppedProcess f τ) 𝒢 μ
have hint : ∀ (i : ℕ), Integrable (stoppedProcess f τ i) μ
Tactic: rw [submartingale_iff_expected_stoppedValue_mono]
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalStopping (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ : Ω → ℕ∞
inst : SigmaFiniteFiltration μ 𝒢
h : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
σ π : Ω → ℕ∞
hσ : IsStoppingTime 𝒢 σ
hπ : IsStoppingTime 𝒢 π
hσ_le_π : σ ≤ π
hπ_bdd : ∃ (N : ℕ), ∀ (x : Ω), π x ≤ (↑N : ℕ∞)
⊢ LE.le (α := ℝ) (∫ (x : Ω), stoppedValue (stoppedProcess f τ) σ x ∂μ)
    (∫ (x : Ω), stoppedValue (stoppedProcess f τ) π x ∂μ)
have simp_rw : LE.le (α := ℝ)
  (∫ (x : Ω),
    if σ x ≠ ⊤ then stoppedValue f (fun (ω : Ω) ↦ min (σ ω) (τ ω)) x
    else stoppedValue f (fun (ω : Ω) ↦ min (↑(Classical.arbitrary ℕ) : WithTop ℕ) (τ ω)) x ∂μ)
  (∫ (x : Ω),
    if π x ≠ ⊤ then stoppedValue f (fun (ω : Ω) ↦ min (π ω) (τ ω)) x
    else stoppedValue f (fun (ω : Ω) ↦ min (↑(Classical.arbitrary ℕ) : WithTop ℕ) (τ ω)) x ∂μ)
Tactic: simp_rw [stoppedValue_stoppedProcess]
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalStopping (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ : Ω → ℕ∞
inst : SigmaFiniteFiltration μ 𝒢
h : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
σ π : Ω → ℕ∞
hσ : IsStoppingTime 𝒢 σ
hπ : IsStoppingTime 𝒢 π
hσ_le_π : σ ≤ π
hπ_bdd : ∃ (N : ℕ), ∀ (x : Ω), π x ≤ (↑N : ℕ∞)
⊢ LE.le (α := ℝ)
    (∫ (x : Ω),
      if σ x ≠ ⊤ then stoppedValue f (fun (ω : Ω) ↦ min (σ ω) (τ ω)) x
      else stoppedValue f (fun (ω : Ω) ↦ min (↑(Classical.arbitrary ℕ) : WithTop ℕ) (τ ω)) x ∂μ)
    (∫ (x : Ω),
      if π x ≠ ⊤ then stoppedValue f (fun (ω : Ω) ↦ min (π ω) (τ ω)) x
      else stoppedValue f (fun (ω : Ω) ↦ min (↑(Classical.arbitrary ℕ) : WithTop ℕ) (τ ω)) x ∂μ)
have obtain : ∀ (n : ℕ) (hπ_le_n : ∀ (x : Ω), π x ≤ (↑n : ℕ∞)),
  LE.le (α := ℝ)
    (∫ (x : Ω),
      if σ x ≠ ⊤ then stoppedValue f (fun (ω : Ω) ↦ min (σ ω) (τ ω)) x
      else stoppedValue f (fun (ω : Ω) ↦ min (↑(Classical.arbitrary ℕ) : WithTop ℕ) (τ ω)) x ∂μ)
    (∫ (x : Ω),
      if π x ≠ ⊤ then stoppedValue f (fun (ω : Ω) ↦ min (π ω) (τ ω)) x
      else stoppedValue f (fun (ω : Ω) ↦ min (↑(Classical.arbitrary ℕ) : WithTop ℕ) (τ ω)) x ∂μ)
Tactic: obtain ⟨n, hπ_le_n⟩ := hπ_bdd
Cleared hypotheses: hπ_bdd
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalStopping (hypothesis)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ : Ω → ℕ∞
inst : SigmaFiniteFiltration μ 𝒢
h : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
σ π : Ω → ℕ∞
hσ : IsStoppingTime 𝒢 σ
hπ : IsStoppingTime 𝒢 π
hσ_le_π : σ ≤ π
n : ℕ
hπ_le_n : ∀ (x : Ω), π x ≤ (↑n : ℕ∞)
⊢ LE.le (α := ℝ)
    (∫ (x : Ω),
      if σ x ≠ ⊤ then stoppedValue f (fun (ω : Ω) ↦ min (σ ω) (τ ω)) x
      else stoppedValue f (fun (ω : Ω) ↦ min (↑(Classical.arbitrary ℕ) : WithTop ℕ) (τ ω)) x ∂μ)
    (∫ (x : Ω),
      if π x ≠ ⊤ then stoppedValue f (fun (ω : Ω) ↦ min (π ω) (τ ω)) x
      else stoppedValue f (fun (ω : Ω) ↦ min (↑(Classical.arbitrary ℕ) : WithTop ℕ) (τ ω)) x ∂μ)
have hπ_top : ∀ (ω : Ω), π ω ≠ ⊤
Tactic: have hπ_top ω : π ω ≠ ⊤ := ne_top_of_le_ne_top (by simp) (hπ_le_n ω)
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalStopping (hypothesis)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ : Ω → ℕ∞
inst : SigmaFiniteFiltration μ 𝒢
h : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
σ π : Ω → ℕ∞
hσ : IsStoppingTime 𝒢 σ
hπ : IsStoppingTime 𝒢 π
hσ_le_π : σ ≤ π
n : ℕ
hπ_le_n : ∀ (x : Ω), π x ≤ (↑n : ℕ∞)
hπ_top : ∀ (ω : Ω), π ω ≠ ⊤
⊢ LE.le (α := ℝ)
    (∫ (x : Ω),
      if σ x ≠ ⊤ then stoppedValue f (fun (ω : Ω) ↦ min (σ ω) (τ ω)) x
      else stoppedValue f (fun (ω : Ω) ↦ min (↑(Classical.arbitrary ℕ) : WithTop ℕ) (τ ω)) x ∂μ)
    (∫ (x : Ω),
      if π x ≠ ⊤ then stoppedValue f (fun (ω : Ω) ↦ min (π ω) (τ ω)) x
      else stoppedValue f (fun (ω : Ω) ↦ min (↑(Classical.arbitrary ℕ) : WithTop ℕ) (τ ω)) x ∂μ)
have hσ_top : ∀ (ω : Ω), σ ω ≠ ⊤
Tactic: have hσ_top ω : σ ω ≠ ⊤ := ne_top_of_le_ne_top (hπ_top ω) (hσ_le_π ω)
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalStopping (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ : Ω → ℕ∞
inst : SigmaFiniteFiltration μ 𝒢
h : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
σ π : Ω → ℕ∞
hσ : IsStoppingTime 𝒢 σ
hπ : IsStoppingTime 𝒢 π
hσ_le_π : σ ≤ π
n : ℕ
hπ_le_n : ∀ (x : Ω), π x ≤ (↑n : ℕ∞)
hπ_top : ∀ (ω : Ω), π ω ≠ ⊤
hσ_top : ∀ (ω : Ω), σ ω ≠ ⊤
⊢ LE.le (α := ℝ)
    (∫ (x : Ω),
      if σ x ≠ ⊤ then stoppedValue f (fun (ω : Ω) ↦ min (σ ω) (τ ω)) x
      else stoppedValue f (fun (ω : Ω) ↦ min (↑(Classical.arbitrary ℕ) : WithTop ℕ) (τ ω)) x ∂μ)
    (∫ (x : Ω),
      if π x ≠ ⊤ then stoppedValue f (fun (ω : Ω) ↦ min (π ω) (τ ω)) x
      else stoppedValue f (fun (ω : Ω) ↦ min (↑(Classical.arbitrary ℕ) : WithTop ℕ) (τ ω)) x ∂μ)
have simp : LE.le (α := ℝ) (∫ (x : Ω), stoppedValue f (fun (ω : Ω) ↦ min (σ ω) (τ ω)) x ∂μ)
  (∫ (x : Ω), stoppedValue f (fun (ω : Ω) ↦ min (π ω) (τ ω)) x ∂μ)
Tactic: simp only [ne_eq, hσ_top, not_false_eq_true, ↓reduceIte, hπ_top, ge_iff_le]
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalStopping (hypothesis)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
ε : ℝ≥0
n : ℕ
x : Ω
hx : (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k x
⊢ (↑ε : ℝ) ≤ stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) x
have hx₁ : ∃ b ≤ n, (↑ε : ℝ) ≤ f b x
Tactic: simp_rw [le_sup'_iff, mem_range, Nat.lt_succ_iff] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalStopping (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
ε : ℝ≥0
n : ℕ
x : Ω
hx : ∃ b ≤ n, (↑ε : ℝ) ≤ f b x
⊢ (↑ε : ℝ) ≤ stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) x
have refine : ∃ j ∈ Set.Icc 0 n, Membership.mem (γ := Set ℝ) {y : ℝ | (↑ε : ℝ) ≤ y} (f j x)
Tactic: refine stoppedValue_hittingBtwn_mem ?_
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalStopping (hypothesis)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
ε : ℝ≥0
n : ℕ
⊢ HSMul.hSMul (β := ℝ≥0∞) ε
      ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} : ℝ≥0∞) ≤
    ENNReal.ofReal
      (∫ (ω : Ω) in {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω},
        stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω ∂μ)
have this : ∀ (ω : Ω),
  ((↑ε : ℝ) ≤ (range (n + 1)).sup' sorry fun (k : ℕ) ↦ f k ω) →
    (↑ε : ℝ) ≤ stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω
Tactic: have : ∀ ω, ((ε : ℝ) ≤ (range (n + 1)).sup' nonempty_range_add_one fun k => f k ω) →
      (ε : ℝ) ≤ stoppedValue f (fun ω ↦ (hittingBtwn f {y : ℝ | ε ≤ y} 0 n ω : ℕ)) ω := by
    intro x hx
    simp_rw [le_sup'_iff, mem_range, Nat.lt_succ_iff] at hx
    refine stoppedValue_hittingBtwn_mem ?_
    simp only [Set.mem_Icc, zero_le, true_and, Set.mem_setOf_eq]
    exact
      let ⟨j, hj₁, hj₂⟩ := hx
      ⟨j, hj₁, hj₂⟩
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalStopping (hypothesis)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
ε : ℝ≥0
n : ℕ
this :
  ∀ (ω : Ω),
    ((↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) →
      (↑ε : ℝ) ≤ stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω
⊢ HSMul.hSMul (β := ℝ≥0∞) ε
      ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} : ℝ≥0∞) ≤
    ENNReal.ofReal
      (∫ (ω : Ω) in {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω},
        stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω ∂μ)
have h : (↑ε : ℝ) * μ.real {a : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' sorry fun (k : ℕ) ↦ f k a} ≤
  ∫ (x : Ω) in {a : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' sorry fun (k : ℕ) ↦ f k a},
    stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) x ∂μ
Tactic: have h := setIntegral_ge_of_const_le_real (measurableSet_le measurable_const
    (measurable_range_sup'' fun n _ => (hsub.stronglyMeasurable n).measurable.le (𝒢.le n)))
      (measure_ne_top _ _) this (Integrable.integrableOn (hsub.integrable_stoppedValue
        (hsub.stronglyAdapted.adapted.isStoppingTime_hittingBtwn measurableSet_Ici)
        (mod_cast hittingBtwn_le)))
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalStopping (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
ε : ℝ≥0
n : ℕ
this :
  ∀ (ω : Ω),
    ((↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) →
      (↑ε : ℝ) ≤ stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω
h :
  (↑ε : ℝ) * μ.real {a : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k a} ≤
    ∫ (x : Ω) in {a : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k a},
      stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) x ∂μ
⊢ HSMul.hSMul (β := ℝ≥0∞) ε
      ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} : ℝ≥0∞) ≤
    ENNReal.ofReal
      (∫ (ω : Ω) in {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω},
        stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω ∂μ)
have rw : ε • ENNReal.toReal ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' sorry fun (k : ℕ) ↦ f k ω}) ≤
  ∫ (ω : Ω) in {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' sorry fun (k : ℕ) ↦ f k ω},
    stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω ∂μ
Tactic: rw [ENNReal.le_ofReal_iff_toReal_le, ENNReal.toReal_smul]
-- Lean 4 proof step from Mathlib.Probability.Martingale.OptionalStopping (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
ε : ℝ≥0
n : ℕ
this :
  ∀ (ω : Ω),
    ((↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) →
      (↑ε : ℝ) ≤ stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω
h :
  (↑ε : ℝ) * μ.real {a : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k a} ≤
    ∫ (x : Ω) in {a : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k a},
      stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) x ∂μ
rw :
  ε • ENNReal.toReal ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω}) ≤
    ∫ (ω : Ω) in {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω},
      stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω ∂μ
⊢ HSMul.hSMul (β := ℝ≥0∞) ε
      ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} : ℝ≥0∞) ≤
    ENNReal.ofReal
      (∫ (ω : Ω) in {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω},
        stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω ∂μ)
have ha : HSMul.hSMul (β := ℝ≥0∞) ε
    ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' sorry fun (k : ℕ) ↦ f k ω} : ℝ≥0∞) ≠
  ∞
Tactic: rw [ENNReal.le_ofReal_iff_toReal_le, ENNReal.toReal_smul]