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 : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
rw :
  ENNReal.ofReal
      (∫ (x : Ω) in
        {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} ∪
          {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)},
        stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) x ∂μ) =
    ENNReal.ofReal
      (∫ (ω : Ω), stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω ∂μ)
hst :
  Disjoint.{u_1} (α := Set Ω) {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω}
    {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)}
ht : MeasurableSet.{u_1} (α := Ω) {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)}
hfs :
  IntegrableOn (stoppedValue f fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ))
    {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} μ
hft :
  IntegrableOn (stoppedValue f fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ))
    {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)} μ
hp :
  LE.le (α := ℝ) 0
    (∫ (ω : Ω) in {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω},
      stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω ∂μ)
⊢ ENNReal.ofReal
        (∫ (ω : Ω) in {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω},
          stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω ∂μ) +
      ENNReal.ofReal
        (∫ (ω : Ω) in {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)},
          stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω ∂μ) =
    ENNReal.ofReal
      (∫ (ω : Ω), stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω ∂μ)
have hq : LE.le (α := ℝ) 0
  (∫ (ω : Ω) in {ω : Ω | ((range (n + 1)).sup' sorry fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)},
    stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω ∂μ)
Tactic: rw [← ENNReal.ofReal_add, ← setIntegral_union]
-- 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 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ ENNReal.ofReal
      (∫ (x : Ω) in
        {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} ∪
          {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)},
        stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) x ∂μ) =
    ENNReal.ofReal
      (∫ (ω : Ω), stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω ∂μ)
have rw : ENNReal.ofReal
    (∫ (x : Ω) in
      {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' sorry fun (k : ℕ) ↦ f k ω} ∪
        {ω : Ω | ((range (n + 1)).sup' sorry fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)},
      stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) x ∂μ) =
  ENNReal.ofReal
    (∫ (x : Ω) in Set.univ,
      stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) x ∂μ)
Tactic: rw [← setIntegral_univ (μ := μ)]
-- 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 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ ENNReal.ofReal
      (∫ (x : Ω) in
        {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} ∪
          {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)},
        stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) x ∂μ) =
    ENNReal.ofReal
      (∫ (x : Ω) in Set.univ,
        stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) x ∂μ)
have h : Eq.{u_1 + 1} (α := Set Ω) Set.univ
  ({ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' sorry fun (k : ℕ) ↦ f k ω} ∪
    {ω : Ω | ((range (n + 1)).sup' sorry fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)})
Tactic: convert! rfl
-- 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 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ Eq.{u_1 + 1} (α := Set Ω) Set.univ
    ({ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} ∪
      {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)})
have h : ∀ (ω : Ω),
  Membership.mem (γ := Set Ω) Set.univ ω ↔
    Membership.mem (γ := Set Ω)
      ({ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' sorry fun (k : ℕ) ↦ f k ω} ∪
        {ω : Ω | ((range (n + 1)).sup' sorry fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)})
      ω
Tactic: ext ω
-- 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 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ ENNReal.ofReal
      (∫ (ω : Ω), stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω ∂μ) ≤
    ENNReal.ofReal (∫ (x : Ω), f n x ∂μ)
have refine : LE.le (α := ℝ)
  (∫ (ω : Ω), stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω ∂μ)
  (∫ (x : Ω), f n x ∂μ)
Tactic: refine ENNReal.ofReal_le_ofReal ?_
-- 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 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ LE.le (α := ℝ)
    (∫ (ω : Ω), stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω ∂μ)
    (∫ (x : Ω), f n x ∂μ)
have rw : LE.le (α := ℝ)
  (∫ (ω : Ω), stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω ∂μ)
  (∫ (x : Ω), stoppedValue f (fun (x : Ω) ↦ (↑n : WithTop ℕ)) x ∂μ)
Tactic: rw [← stoppedValue_const f n]
-- 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 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ LE.le (α := ℝ)
    (∫ (ω : Ω), stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω ∂μ)
    (∫ (x : Ω), stoppedValue f (fun (x : Ω) ↦ (↑n : WithTop ℕ)) x ∂μ)
have refine : ∀ (ω : Ω), (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ) ≤ (↑n : WithTop ℕ)
Tactic: refine hsub.expected_stoppedValue_mono
        (hsub.stronglyAdapted.adapted.isStoppingTime_hittingBtwn measurableSet_Ici)
        (isStoppingTime_const _ _) (fun ω ↦ ?_) (fun _ => mod_cast le_rfl)
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
ι : Type u_2
inst : Preorder ι
inst_1 : OrderBot ι
inst_2 : InfSet ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
n : ℕ
ω : Ω
⊢ upperCrossingTime a b f N (n + 1) ω =
    hittingBtwn f (Set.Ici b) (lowerCrossingTimeAux a f (upperCrossingTime a b f N n ω) N ω) N ω
have rw : (fun (ω : Ω) ↦ hittingBtwn f (Set.Ici b) (lowerCrossingTimeAux a f (upperCrossingTime a b f N n ω) N ω) N ω) ω =
  hittingBtwn f (Set.Ici b) (lowerCrossingTimeAux a f (upperCrossingTime a b f N n ω) N ω) N ω
Tactic: rw [upperCrossingTime]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
ι : Type u_2
inst : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
n : ℕ
ω : Ω
⊢ upperCrossingTime a b f N n ω ≤ N
have zero : upperCrossingTime a b f N 0 ω ≤ N
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
ι : Type u_2
inst : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
n : ℕ
ω : Ω
zero : upperCrossingTime a b f N 0 ω ≤ N
⊢ upperCrossingTime a b f N n ω ≤ N
have succ : ∀ (n : ℕ), upperCrossingTime a b f N (n + 1) ω ≤ N
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
ι : Type u_2
inst : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
n : ℕ
ω : Ω
⊢ lowerCrossingTime a b f N n ω ≤ upperCrossingTime a b f N (n + 1) ω
have rw : lowerCrossingTime a b f N n ω ≤
  hittingBtwn f (Set.Ici b) (lowerCrossingTimeAux a f (upperCrossingTime a b f N n ω) N ω) N ω
Tactic: rw [upperCrossingTime_succ]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
ι : Type u_2
inst : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
n m : ℕ
ω : Ω
hnm : n ≤ m
⊢ lowerCrossingTime a b f N n ω ≤ lowerCrossingTime a b f N m ω
have suffices : Monotone.{0, u_2} (β := ι) fun (n : ℕ) ↦ lowerCrossingTime a b f N n ω
Tactic: suffices Monotone fun n => lowerCrossingTime a b f N n ω by exact this hnm
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
ι : Type u_2
inst : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
n m : ℕ
ω : Ω
hnm : n ≤ m
⊢ upperCrossingTime a b f N n ω ≤ upperCrossingTime a b f N m ω
have suffices : Monotone.{0, u_2} (β := ι) fun (n : ℕ) ↦ upperCrossingTime a b f N n ω
Tactic: suffices Monotone fun n => upperCrossingTime a b f N n ω by exact this hnm
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
h : lowerCrossingTime a b f N n ω ≠ N
⊢ stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N n ω) : WithTop ℕ)) ω ≤ a
have obtain : ∀ (j : ℕ) (hj₁ : j ∈ Set.Icc (upperCrossingTime a b f N n ω) (lowerCrossingTime a b f N n ω)) (hj₂ : f j ω ∈ Set.Iic a),
  stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N n ω) : WithTop ℕ)) ω ≤ a
Tactic: obtain ⟨j, hj₁, hj₂⟩ :=
    (hittingBtwn_le_iff_of_lt _ (lt_of_le_of_ne lowerCrossingTime_le h)).1 le_rfl
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
h : upperCrossingTime a b f N (n + 1) ω ≠ N
⊢ b ≤ stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (n + 1) ω) : WithTop ℕ)) ω
have obtain : ∀ (j : ℕ)
  (hj₁ :
    j ∈ Set.Icc (lowerCrossingTimeAux a f (upperCrossingTime a b f N n ω) N ω) (upperCrossingTime a b f N (n + 1) ω))
  (hj₂ : f j ω ∈ Set.Ici b), b ≤ stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (n + 1) ω) : WithTop ℕ)) ω
Tactic: obtain ⟨j, hj₁, hj₂⟩ :=
    (hittingBtwn_le_iff_of_lt _ (lt_of_le_of_ne upperCrossingTime_le h)).1 le_rfl
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : lowerCrossingTime a b f N (n + 1) ω ≠ N
⊢ upperCrossingTime a b f N (n + 1) ω < lowerCrossingTime a b f N (n + 1) ω
have refine : ∀ (h : upperCrossingTime a b f N (n + 1) ω = lowerCrossingTime a b f N (n + 1) ω),
  b ≤ stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N (n + 1) ω) : WithTop ℕ)) ω
Tactic: refine lt_of_le_of_ne upperCrossingTime_le_lowerCrossingTime fun h =>
    not_le.2 hab <| le_trans ?_ (stoppedValue_lowerCrossingTime hn)
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : lowerCrossingTime a b f N (n + 1) ω ≠ N
h : upperCrossingTime a b f N (n + 1) ω = lowerCrossingTime a b f N (n + 1) ω
⊢ b ≤ stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N (n + 1) ω) : WithTop ℕ)) ω
have simp : b ≤ f (WithTop.untopA (↑(lowerCrossingTime a b f N (n + 1) ω) : WithTop ℕ)) ω
Tactic: simp only [stoppedValue]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : lowerCrossingTime a b f N (n + 1) ω ≠ N
h : upperCrossingTime a b f N (n + 1) ω = lowerCrossingTime a b f N (n + 1) ω
⊢ b ≤ f (WithTop.untopA (↑(lowerCrossingTime a b f N (n + 1) ω) : WithTop ℕ)) ω
have rw : b ≤ f (WithTop.untopA (↑(upperCrossingTime a b f N (n + 1) ω) : WithTop ℕ)) ω
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : upperCrossingTime a b f N (n + 1) ω ≠ N
⊢ lowerCrossingTime a b f N n ω < upperCrossingTime a b f N (n + 1) ω
have refine : ∀ (h : lowerCrossingTime a b f N n ω = upperCrossingTime a b f N (n + 1) ω),
  stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (n + 1) ω) : WithTop ℕ)) ω ≤ a
Tactic: refine lt_of_le_of_ne lowerCrossingTime_le_upperCrossingTime_succ fun h =>
    not_le.2 hab <| le_trans (stoppedValue_upperCrossingTime hn) ?_
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : upperCrossingTime a b f N (n + 1) ω ≠ N
h : lowerCrossingTime a b f N n ω = upperCrossingTime a b f N (n + 1) ω
⊢ stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (n + 1) ω) : WithTop ℕ)) ω ≤ a
have simp : f (WithTop.untopA (↑(upperCrossingTime a b f N (n + 1) ω) : WithTop ℕ)) ω ≤ a
Tactic: simp only [stoppedValue]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : upperCrossingTime a b f N (n + 1) ω ≠ N
h : lowerCrossingTime a b f N n ω = upperCrossingTime a b f N (n + 1) ω
⊢ f (WithTop.untopA (↑(upperCrossingTime a b f N (n + 1) ω) : WithTop ℕ)) ω ≤ a
have rw : f (WithTop.untopA (↑(lowerCrossingTime a b f N n ω) : WithTop ℕ)) ω ≤ a
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
⊢ ∃ (n : ℕ), upperCrossingTime a b f N n ω = N
have by_contra! : ∀ (h : ∀ (n : ℕ), upperCrossingTime a b f N n ω ≠ N), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (hypothesis)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
h : ∀ (n : ℕ), upperCrossingTime a b f N n ω ≠ N
⊢ False
have this : StrictMono (β := ℕ) fun (n : ℕ) ↦ upperCrossingTime a b f N n ω
Tactic: have : StrictMono fun n => upperCrossingTime a b f N n ω :=
    strictMono_nat_of_lt_succ fun n => upperCrossingTime_lt_succ hab (h _)
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
h : ∀ (n : ℕ), upperCrossingTime a b f N n ω ≠ N
this : StrictMono (β := ℕ) fun (n : ℕ) ↦ upperCrossingTime a b f N n ω
⊢ False
have obtain : ∀ (k : ℕ) (hk : N < (fun (n : ℕ) ↦ upperCrossingTime a b f N n ω) k), False
Tactic: obtain ⟨_, ⟨k, rfl⟩, hk⟩ :
      ∃ (m : _) (_ : m ∈ Set.range fun n => upperCrossingTime a b f N n ω), N < m :=
    ⟨upperCrossingTime a b f N (N + 1) ω, ⟨N + 1, rfl⟩,
      lt_of_lt_of_le N.lt_succ_self (StrictMono.id_le this (N + 1))⟩
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
⊢ BddAbove (α := ℕ) {n : ℕ | upperCrossingTime a b f N n ω < N}
have obtain : ∀ (k : ℕ) (hk : upperCrossingTime a b f N k ω = N), BddAbove (α := ℕ) {n : ℕ | upperCrossingTime a b f N n ω < N}
Tactic: obtain ⟨k, hk⟩ := exists_upperCrossingTime_eq f N ω hab
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
k : ℕ
hk : upperCrossingTime a b f N k ω = N
⊢ BddAbove (α := ℕ) {n : ℕ | upperCrossingTime a b f N n ω < N}
have refine : ∀ (n : ℕ) (hn : upperCrossingTime a b f N n ω < N), n ≤ k
Tactic: refine ⟨k, fun n (hn : upperCrossingTime a b f N n ω < N) => ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
k : ℕ
hk : upperCrossingTime a b f N k ω = N
n : ℕ
hn : upperCrossingTime a b f N n ω < N
⊢ n ≤ k
have by_contra : ∀ (hn' : ¬n ≤ k), False
Tactic: by_contra hn'
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
⊢ upperCrossingTime a b f N N ω = N
have pos : ∀ (hN' : N < Nat.find (p := fun (n : ℕ) ↦ upperCrossingTime a b f N n ω = N) sorry), upperCrossingTime a b f N N ω = N
Tactic: by_cases hN' : N < Nat.find (exists_upperCrossingTime_eq f N ω hab)
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
pos : ∀ (hN' : N < Nat.find (p := fun (n : ℕ) ↦ upperCrossingTime a b f N n ω = N) ⋯), upperCrossingTime a b f N N ω = N
⊢ upperCrossingTime a b f N N ω = N
have neg : ∀ (hN' : ¬N < Nat.find (p := fun (n : ℕ) ↦ upperCrossingTime a b f N n ω = N) sorry), upperCrossingTime a b f N N ω = N
Tactic: by_cases hN' : N < Nat.find (exists_upperCrossingTime_eq f N ω hab)
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN' : N < Nat.find (p := fun (n : ℕ) ↦ upperCrossingTime a b f N n ω = N) ⋯
⊢ upperCrossingTime a b f N N ω = N
have pos : N ≤ upperCrossingTime a b f N N ω
Tactic: refine le_antisymm upperCrossingTime_le ?_
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN' : N < Nat.find (p := fun (n : ℕ) ↦ upperCrossingTime a b f N n ω = N) ⋯
⊢ StrictMonoOn (β := ℕ) (fun (n : ℕ) ↦ upperCrossingTime a b f N n ω)
    (Set.Iic (Nat.find (p := fun (n : ℕ) ↦ upperCrossingTime a b f N n ω = N) ⋯).pred)
have refine : ∀ (m : ℕ) (hm : m < (Nat.find (p := fun (n : ℕ) ↦ upperCrossingTime a b f N n ω = N) sorry).pred),
  upperCrossingTime a b f N (m + 1) ω ≠ N
Tactic: refine strictMonoOn_Iic_of_lt_succ fun m hm => upperCrossingTime_lt_succ hab ?_
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (hypothesis)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN' : N < Nat.find (p := fun (n : ℕ) ↦ upperCrossingTime a b f N n ω = N) ⋯
m : ℕ
hm : m < (Nat.find (p := fun (n : ℕ) ↦ upperCrossingTime a b f N n ω = N) ⋯).pred
⊢ upperCrossingTime a b f N (m + 1) ω ≠ N
have hm₁ : m.succ < Nat.find (p := fun (n : ℕ) ↦ upperCrossingTime a b f N n ω = N) sorry
Tactic: rw [Nat.lt_pred_iff] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (hypothesis)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN' : N < Nat.find (p := fun (n : ℕ) ↦ upperCrossingTime a b f N n ω = N) ⋯
⊢ N ≤ upperCrossingTime a b f N N ω
have hmono : StrictMonoOn (β := ℕ) (fun (n : ℕ) ↦ upperCrossingTime a b f N n ω)
  (Set.Iic (Nat.find (p := fun (n : ℕ) ↦ upperCrossingTime a b f N n ω = N) sorry).pred)
Tactic: have hmono : StrictMonoOn (fun n => upperCrossingTime a b f N n ω)
        (Set.Iic (Nat.find (exists_upperCrossingTime_eq f N ω hab)).pred) := by
      refine strictMonoOn_Iic_of_lt_succ fun m hm => upperCrossingTime_lt_succ hab ?_
      rw [Nat.lt_pred_iff] at hm
      convert! Nat.find_min _ hm
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (hypothesis)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN' : ¬N < Nat.find (p := fun (n : ℕ) ↦ upperCrossingTime a b f N n ω = N) ⋯
⊢ upperCrossingTime a b f N N ω = N
have hN'₁ : Nat.find (p := fun (n : ℕ) ↦ upperCrossingTime a b f N n ω = N) sorry ≤ N
Tactic: rw [not_lt] at hN'
Cleared hypotheses: hN'
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ℱ : Filtration ℕ m0
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
⊢ (IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N 0 ω) : WithTop ℕ)) ∧
    IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N 0 ω) : WithTop ℕ)
have zero : IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N 0 ω) : WithTop ℕ)
Tactic: refine ⟨isStoppingTime_const _ 0, ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n_1 : ℕ
ℱ : Filtration ℕ m0
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
k : ℕ
ih :
  (IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N k ω) : WithTop ℕ)) ∧
    IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)
n : ℕ
⊢ MeasurableSet.{u_1} (α := Ω)
    {ω : Ω | (↑(hittingBtwn f (Set.Ici b) (lowerCrossingTime a b f N k ω) N ω) : WithTop ℕ) ≤ (↑n : WithTop ℕ)}
have refine : ∀ (x : Ω), (↑(lowerCrossingTime a b f N k x) : WithTop ℕ) ≤ (↑N : WithTop ℕ)
Tactic: refine hf.adapted.isStoppingTime_hittingBtwn_isStoppingTime ih.2 ?_ measurableSet_Ici _
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (hypothesis)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ℱ : Filtration ℕ m0
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
k : ℕ
ih :
  (IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N k ω) : WithTop ℕ)) ∧
    IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)
⊢ (IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)) ∧
    IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N (k + 1) ω) : WithTop ℕ)
have this : IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)
Tactic: have : IsStoppingTime ℱ (fun ω ↦ (upperCrossingTime a b f N (k + 1) ω : ℕ)) := by
      intro n
      simp_rw [upperCrossingTime_succ_eq]
      refine hf.adapted.isStoppingTime_hittingBtwn_isStoppingTime ih.2 ?_ measurableSet_Ici _
      simp [lowerCrossingTime_le]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ℱ : Filtration ℕ m0
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
k : ℕ
ih :
  (IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N k ω) : WithTop ℕ)) ∧
    IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)
this : IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)
⊢ (IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)) ∧
    IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N (k + 1) ω) : WithTop ℕ)
have succ : ∀ (n : ℕ),
  MeasurableSet.{u_1} (α := Ω)
    {ω : Ω | (fun (ω : Ω) ↦ ((↑(lowerCrossingTime a b f N (k + 1) ω) : WithTop ℕ) : WithTop ℕ)) ω ≤ (↑n : WithTop ℕ)}
Tactic: refine ⟨this, fun n ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n_1 : ℕ
ℱ : Filtration ℕ m0
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
k : ℕ
ih :
  (IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N k ω) : WithTop ℕ)) ∧
    IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)
this : IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)
n : ℕ
⊢ MeasurableSet.{u_1} (α := Ω)
    {ω : Ω | (fun (ω : Ω) ↦ ((↑(lowerCrossingTime a b f N (k + 1) ω) : WithTop ℕ) : WithTop ℕ)) ω ≤ (↑n : WithTop ℕ)}
have succ : ∀ (x : Ω), (↑(upperCrossingTime a b f N (k + 1) x) : WithTop ℕ) ≤ (↑N : WithTop ℕ)
Tactic: refine hf.adapted.isStoppingTime_hittingBtwn_isStoppingTime this ?_ measurableSet_Iic _