awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    ∑ n ∈ Finset.range N,
        (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)).indicator
          (fun (m : ℕ) ↦ f (m + 1) ω - f m ω) n =
      stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)) ω -
        stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)) ω
h₂ :
  LE.le (α := ℝ) (∑ _k ∈ Finset.range (upcrossingsBefore a b f N ω), (b - a))
    (∑ k ∈ Finset.range N,
      (stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)) ω -
        stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)) ω))
⊢ (b - a) * (↑(upcrossingsBefore a b f N ω) : ℝ) ≤ ∑ _k ∈ Finset.range (upcrossingsBefore a b f N ω), (b - a)
have neg : (b - a) * (↑(upcrossingsBefore a b f N ω) : ℝ) ≤ (Finset.range (upcrossingsBefore a b f N ω)).card • (b - a)
Tactic: rw [Finset.sum_const, Finset.card_range, nsmul_eq_mul, mul_comm]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    ∑ n ∈ Finset.range N,
        (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)).indicator
          (fun (m : ℕ) ↦ f (m + 1) ω - f m ω) n =
      stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)) ω -
        stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)) ω
h₂ :
  LE.le (α := ℝ) (∑ _k ∈ Finset.range (upcrossingsBefore a b f N ω), (b - a))
    (∑ k ∈ Finset.range N,
      (stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)) ω -
        stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)) ω))
neg : (b - a) * (↑(upcrossingsBefore a b f N ω) : ℝ) ≤ (Finset.range (upcrossingsBefore a b f N ω)).card • (b - a)
⊢ (b - a) * (↑(upcrossingsBefore a b f N ω) : ℝ) ≤ ∑ _k ∈ Finset.range (upcrossingsBefore a b f N ω), (b - a)
have neg₁ : (b - a) * (↑(upcrossingsBefore a b f N ω) : ℝ) ≤ upcrossingsBefore a b f N ω • (b - a)
Tactic: rw [Finset.sum_const, Finset.card_range, nsmul_eq_mul, mul_comm]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    ∑ n ∈ Finset.range N,
        (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)).indicator
          (fun (m : ℕ) ↦ f (m + 1) ω - f m ω) n =
      stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)) ω -
        stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)) ω
h₂ :
  LE.le (α := ℝ) (∑ _k ∈ Finset.range (upcrossingsBefore a b f N ω), (b - a))
    (∑ k ∈ Finset.range N,
      (stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)) ω -
        stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)) ω))
neg : (b - a) * (↑(upcrossingsBefore a b f N ω) : ℝ) ≤ (Finset.range (upcrossingsBefore a b f N ω)).card • (b - a)
neg₁ : (b - a) * (↑(upcrossingsBefore a b f N ω) : ℝ) ≤ upcrossingsBefore a b f N ω • (b - a)
⊢ (b - a) * (↑(upcrossingsBefore a b f N ω) : ℝ) ≤ ∑ _k ∈ Finset.range (upcrossingsBefore a b f N ω), (b - a)
have neg₂ : (b - a) * (↑(upcrossingsBefore a b f N ω) : ℝ) ≤ (↑(upcrossingsBefore a b f N ω) : ℝ) * (b - a)
Tactic: rw [Finset.sum_const, Finset.card_range, nsmul_eq_mul, mul_comm]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    ∑ n ∈ Finset.range N,
        (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)).indicator
          (fun (m : ℕ) ↦ f (m + 1) ω - f m ω) n =
      stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)) ω -
        stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)) ω
h₂ :
  LE.le (α := ℝ) (∑ _k ∈ Finset.range (upcrossingsBefore a b f N ω), (b - a))
    (∑ k ∈ Finset.range N,
      (stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)) ω -
        stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)) ω))
neg : (b - a) * (↑(upcrossingsBefore a b f N ω) : ℝ) ≤ (Finset.range (upcrossingsBefore a b f N ω)).card • (b - a)
neg₁ : (b - a) * (↑(upcrossingsBefore a b f N ω) : ℝ) ≤ upcrossingsBefore a b f N ω • (b - a)
neg₂ : (b - a) * (↑(upcrossingsBefore a b f N ω) : ℝ) ≤ (↑(upcrossingsBefore a b f N ω) : ℝ) * (b - a)
⊢ (b - a) * (↑(upcrossingsBefore a b f N ω) : ℝ) ≤ ∑ _k ∈ Finset.range (upcrossingsBefore a b f N ω), (b - a)
have neg₃ : (↑(upcrossingsBefore a b f N ω) : ℝ) * (b - a) ≤ (↑(upcrossingsBefore a b f N ω) : ℝ) * (b - a)
Tactic: rw [Finset.sum_const, Finset.card_range, nsmul_eq_mul, mul_comm]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hfN : ∀ (ω : Ω), a ≤ f N ω
hfzero : 0 ≤ f 0
hab : a < b
⊢ (b - a) * ∫ (x : Ω), (↑(upcrossingsBefore a b f N x) : ℝ) ∂μ ≤
    ∫ (x : Ω), (∑ k ∈ Finset.range N, upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ
have rw : LE.le (α := ℝ) (∫ (a_1 : Ω), (b - a) * (↑(upcrossingsBefore a b f N a_1) : ℝ) ∂μ)
  (∫ (x : Ω), (∑ k ∈ Finset.range N, upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ)
Tactic: rw [← integral_const_mul]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hfN : ∀ (ω : Ω), a ≤ f N ω
hfzero : 0 ≤ f 0
hab : a < b
⊢ LE.le (α := ℝ) (∫ (a_1 : Ω), (b - a) * (↑(upcrossingsBefore a b f N a_1) : ℝ) ∂μ)
    (∫ (x : Ω), (∑ k ∈ Finset.range N, upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ)
have refine_1 : (ae μ).EventuallyLE (β := ℝ) 0 fun (a_1 : Ω) ↦ (b - a) * (↑(upcrossingsBefore a b f N a_1) : ℝ)
Tactic: refine integral_mono_of_nonneg ?_ ((hf.sum_upcrossingStrat_mul a b N).integrable N) ?_
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hfN : ∀ (ω : Ω), a ≤ f N ω
hfzero : 0 ≤ f 0
hab : a < b
refine_1 : (ae μ).EventuallyLE (β := ℝ) 0 fun (a_1 : Ω) ↦ (b - a) * (↑(upcrossingsBefore a b f N a_1) : ℝ)
⊢ LE.le (α := ℝ) (∫ (a_1 : Ω), (b - a) * (↑(upcrossingsBefore a b f N a_1) : ℝ) ∂μ)
    (∫ (x : Ω), (∑ k ∈ Finset.range N, upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ)
have refine_2 : (ae μ).EventuallyLE (β := ℝ) (fun (a_1 : Ω) ↦ (b - a) * (↑(upcrossingsBefore a b f N a_1) : ℝ))
  (∑ k ∈ Finset.range N, upcrossingStrat a b f N k * (f (k + 1) - f k))
Tactic: refine integral_mono_of_nonneg ?_ ((hf.sum_upcrossingStrat_mul a b N).integrable N) ?_
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hfN : ∀ (ω : Ω), a ≤ f N ω
hfzero : 0 ≤ f 0
hab : a < b
⊢ (ae μ).EventuallyLE (β := ℝ) (fun (a_1 : Ω) ↦ (b - a) * (↑(upcrossingsBefore a b f N a_1) : ℝ))
    (∑ k ∈ Finset.range N, upcrossingStrat a b f N k * (f (k + 1) - f k))
have refine_2 : ∀ (ω : Ω),
  (b - a) * (↑(upcrossingsBefore a b f N ω) : ℝ) ≤
    (∑ k ∈ Finset.range N, upcrossingStrat a b f N k * (f (k + 1) - f k)) ω
Tactic: filter_upwards with ω
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (hypothesis)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
hab : a < b
⊢ upperCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N n = upperCrossingTime a b f N n ∧
    lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N n = lowerCrossingTime a b f N n
have hab' : 0 < b - a
Tactic: have hab' : 0 < b - a := sub_pos.2 hab
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
hab : a < b
hab' : 0 < b - a
i : Ω
ω : ℕ
⊢ b - a ≤ (f ω i - a)⁺ ↔ b ≤ f ω i
have refine_1 : ∀ (h : b - a ≤ (f ω i - a)⁺), b ≤ f ω i
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
hab : a < b
hab' : 0 < b - a
i : Ω
ω : ℕ
refine_1 : ∀ (h : b - a ≤ (f ω i - a)⁺), b ≤ f ω i
⊢ b - a ≤ (f ω i - a)⁺ ↔ b ≤ f ω i
have refine_2 : ∀ (h : b ≤ f ω i), b - a ≤ (f ω i - a)⁺
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
hab : a < b
hab' : 0 < b - a
i : Ω
ω : ℕ
h : b - a ≤ (f ω i - a)⁺
⊢ b ≤ f ω i
have refine_1 : b - a ≤ f ω i - a
Tactic: rwa [← sub_le_sub_iff_right a, ←
        posPart_eq_of_posPart_pos (lt_of_lt_of_le hab' h)]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (hypothesis)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
hab : a < b
hab' : 0 < b - a
i : Ω
ω : ℕ
h : b ≤ f ω i
⊢ b - a ≤ (f ω i - a)⁺
have h₁ : b - a ≤ f ω i - a
Tactic: rw [← sub_le_sub_iff_right a] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (hypothesis)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
hab : a < b
hab' : 0 < b - a
⊢ upperCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N n = upperCrossingTime a b f N n ∧
    lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N n = lowerCrossingTime a b f N n
have hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
Tactic: have hf : ∀ ω i, b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω := by
    intro i ω
    refine ⟨fun h => ?_, fun h => ?_⟩
    · rwa [← sub_le_sub_iff_right a, ←
        posPart_eq_of_posPart_pos (lt_of_lt_of_le hab' h)]
    · rw [← sub_le_sub_iff_right a] at h
      rwa [posPart_eq_self.2 (le_trans hab'.le h)]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
ω : Ω
i : ℕ
⊢ (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
have rw : f i ω - a ≤ 0 ↔ f i ω ≤ a
Tactic: rw [posPart_nonpos, sub_nonpos]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
ω : Ω
i : ℕ
rw : f i ω - a ≤ 0 ↔ f i ω ≤ a
⊢ (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
have rw₁ : f i ω ≤ a ↔ f i ω ≤ a
Tactic: rw [posPart_nonpos, sub_nonpos]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (hypothesis)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
⊢ upperCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N n = upperCrossingTime a b f N n ∧
    lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N n = lowerCrossingTime a b f N n
have hf' : ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
Tactic: have hf' (ω i) : (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a := by rw [posPart_nonpos, sub_nonpos]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
hf' : ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
⊢ upperCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N 0 = upperCrossingTime a b f N 0 ∧
    lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N 0 = lowerCrossingTime a b f N 0
have zero : lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N 0 = lowerCrossingTime a b f N 0
Tactic: refine ⟨rfl, ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
hf' : ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
k : ℕ
ih :
  upperCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N k = upperCrossingTime a b f N k ∧
    lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N k = lowerCrossingTime a b f N k
⊢ upperCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N (k + 1) = upperCrossingTime a b f N (k + 1)
have h : ∀ (ω : Ω),
  upperCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N (k + 1) ω = upperCrossingTime a b f N (k + 1) ω
Tactic: ext ω
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
hf' : ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
k : ℕ
ih :
  upperCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N k = upperCrossingTime a b f N k ∧
    lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N k = lowerCrossingTime a b f N k
ω : Ω
⊢ upperCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N (k + 1) ω = upperCrossingTime a b f N (k + 1) ω
have h : (if
      ∃ j ∈ Set.Icc (lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N k ω) N,
        (f j ω - a)⁺ ∈ Set.Ici (b - a) then
    sInf
      (Set.Icc (lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N k ω) N ∩
        {i : ℕ | b ≤ (f i ω - a)⁺ + a})
  else N) =
  if ∃ j ∈ Set.Icc (lowerCrossingTime a b f N k ω) N, f j ω ∈ Set.Ici b then
    sInf (Set.Icc (lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N k ω) N ∩ {i : ℕ | b ≤ f i ω})
  else N
Tactic: simp only [upperCrossingTime_succ_eq, ← ih.2, hittingBtwn, Set.mem_Ici, tsub_le_iff_right]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
hf' : ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
k : ℕ
ih :
  upperCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N k = upperCrossingTime a b f N k ∧
    lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N k = lowerCrossingTime a b f N k
ω : Ω
⊢ (if
        ∃ j ∈ Set.Icc (lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N k ω) N,
          (f j ω - a)⁺ ∈ Set.Ici (b - a) then
      sInf
        (Set.Icc (lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N k ω) N ∩
          {i : ℕ | b ≤ (f i ω - a)⁺ + a})
    else N) =
    if ∃ j ∈ Set.Icc (lowerCrossingTime a b f N k ω) N, f j ω ∈ Set.Ici b then
      sInf (Set.Icc (lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N k ω) N ∩ {i : ℕ | b ≤ f i ω})
    else N
have pos : ∀
  (h₁ :
    ∃ j ∈ Set.Icc (lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N k ω) N,
      (f j ω - a)⁺ ∈ Set.Ici (b - a))
  (h₂ : ∃ j ∈ Set.Icc (lowerCrossingTime a b f N k ω) N, f j ω ∈ Set.Ici b),
  sInf
      (Set.Icc (lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N k ω) N ∩
        {i : ℕ | b ≤ (f i ω - a)⁺ + a}) =
    sInf (Set.Icc (lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N k ω) N ∩ {i : ℕ | b ≤ f i ω})
Tactic: split_ifs with h₁ h₂ h₂
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
hf' : ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
k : ℕ
ih :
  upperCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N k = upperCrossingTime a b f N k ∧
    lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N k = lowerCrossingTime a b f N k
ω : Ω
pos :
  ∀
    (h₁ :
      ∃ j ∈ Set.Icc (lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N k ω) N,
        (f j ω - a)⁺ ∈ Set.Ici (b - a))
    (h₂ : ∃ j ∈ Set.Icc (lowerCrossingTime a b f N k ω) N, f j ω ∈ Set.Ici b),
    sInf
        (Set.Icc (lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N k ω) N ∩
          {i : ℕ | b ≤ (f i ω - a)⁺ + a}) =
      sInf (Set.Icc (lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N k ω) N ∩ {i : ℕ | b ≤ f i ω})
⊢ (if
        ∃ j ∈ Set.Icc (lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N k ω) N,
          (f j ω - a)⁺ ∈ Set.Ici (b - a) then
      sInf
        (Set.Icc (lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N k ω) N ∩
          {i : ℕ | b ≤ (f i ω - a)⁺ + a})
    else N) =
    if ∃ j ∈ Set.Icc (lowerCrossingTime a b f N k ω) N, f j ω ∈ Set.Ici b then
      sInf (Set.Icc (lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N k ω) N ∩ {i : ℕ | b ≤ f i ω})
    else N
have neg : ∀
  (h₁ :
    ∃ j ∈ Set.Icc (lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N k ω) N,
      (f j ω - a)⁺ ∈ Set.Ici (b - a))
  (h₂ : ¬∃ j ∈ Set.Icc (lowerCrossingTime a b f N k ω) N, f j ω ∈ Set.Ici b),
  sInf
      (Set.Icc (lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N k ω) N ∩
        {i : ℕ | b ≤ (f i ω - a)⁺ + a}) =
    N
Tactic: split_ifs with h₁ h₂ h₂
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
hf' : ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
k : ℕ
ih :
  upperCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N k = upperCrossingTime a b f N k ∧
    lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N k = lowerCrossingTime a b f N k
ω : Ω
pos :
  ∀
    (h₁ :
      ∃ j ∈ Set.Icc (lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N k ω) N,
        (f j ω - a)⁺ ∈ Set.Ici (b - a))
    (h₂ : ∃ j ∈ Set.Icc (lowerCrossingTime a b f N k ω) N, f j ω ∈ Set.Ici b),
    sInf
        (Set.Icc (lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N k ω) N ∩
          {i : ℕ | b ≤ (f i ω - a)⁺ + a}) =
      sInf (Set.Icc (lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N k ω) N ∩ {i : ℕ | b ≤ f i ω})
neg :
  ∀
    (h₁ :
      ∃ j ∈ Set.Icc (lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N k ω) N,
        (f j ω - a)⁺ ∈ Set.Ici (b - a))
    (h₂ : ¬∃ j ∈ Set.Icc (lowerCrossingTime a b f N k ω) N, f j ω ∈ Set.Ici b),
    sInf
        (Set.Icc (lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N k ω) N ∩
          {i : ℕ | b ≤ (f i ω - a)⁺ + a}) =
      N
⊢ (if
        ∃ j ∈ Set.Icc (lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N k ω) N,
          (f j ω - a)⁺ ∈ Set.Ici (b - a) then
      sInf
        (Set.Icc (lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N k ω) N ∩
          {i : ℕ | b ≤ (f i ω - a)⁺ + a})
    else N) =
    if ∃ j ∈ Set.Icc (lowerCrossingTime a b f N k ω) N, f j ω ∈ Set.Ici b then
      sInf (Set.Icc (lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N k ω) N ∩ {i : ℕ | b ≤ f i ω})
    else N
have pos₁ : ∀
  (h₁ :
    ¬∃ j ∈ Set.Icc (lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N k ω) N,
        (f j ω - a)⁺ ∈ Set.Ici (b - a))
  (h₂ : ∃ j ∈ Set.Icc (lowerCrossingTime a b f N k ω) N, f j ω ∈ Set.Ici b),
  N = sInf (Set.Icc (lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N k ω) N ∩ {i : ℕ | b ≤ f i ω})
Tactic: split_ifs with h₁ h₂ h₂
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
hf' : ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
k : ℕ
ih :
  upperCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N k = upperCrossingTime a b f N k ∧
    lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N k = lowerCrossingTime a b f N k
ω : Ω
pos :
  ∀
    (h₁ :
      ∃ j ∈ Set.Icc (lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N k ω) N,
        (f j ω - a)⁺ ∈ Set.Ici (b - a))
    (h₂ : ∃ j ∈ Set.Icc (lowerCrossingTime a b f N k ω) N, f j ω ∈ Set.Ici b),
    sInf
        (Set.Icc (lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N k ω) N ∩
          {i : ℕ | b ≤ (f i ω - a)⁺ + a}) =
      sInf (Set.Icc (lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N k ω) N ∩ {i : ℕ | b ≤ f i ω})
neg :
  ∀
    (h₁ :
      ∃ j ∈ Set.Icc (lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N k ω) N,
        (f j ω - a)⁺ ∈ Set.Ici (b - a))
    (h₂ : ¬∃ j ∈ Set.Icc (lowerCrossingTime a b f N k ω) N, f j ω ∈ Set.Ici b),
    sInf
        (Set.Icc (lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N k ω) N ∩
          {i : ℕ | b ≤ (f i ω - a)⁺ + a}) =
      N
pos₁ :
  ∀
    (h₁ :
      ¬∃ j ∈ Set.Icc (lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N k ω) N,
          (f j ω - a)⁺ ∈ Set.Ici (b - a))
    (h₂ : ∃ j ∈ Set.Icc (lowerCrossingTime a b f N k ω) N, f j ω ∈ Set.Ici b),
    N = sInf (Set.Icc (lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N k ω) N ∩ {i : ℕ | b ≤ f i ω})
⊢ (if
        ∃ j ∈ Set.Icc (lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N k ω) N,
          (f j ω - a)⁺ ∈ Set.Ici (b - a) then
      sInf
        (Set.Icc (lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N k ω) N ∩
          {i : ℕ | b ≤ (f i ω - a)⁺ + a})
    else N) =
    if ∃ j ∈ Set.Icc (lowerCrossingTime a b f N k ω) N, f j ω ∈ Set.Ici b then
      sInf (Set.Icc (lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N k ω) N ∩ {i : ℕ | b ≤ f i ω})
    else N
have neg₁ : ∀
  (h₁ :
    ¬∃ j ∈ Set.Icc (lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N k ω) N,
        (f j ω - a)⁺ ∈ Set.Ici (b - a))
  (h₂ : ¬∃ j ∈ Set.Icc (lowerCrossingTime a b f N k ω) N, f j ω ∈ Set.Ici b), N = N
Tactic: split_ifs with h₁ h₂ h₂
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
hf' : ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
k : ℕ
ih :
  upperCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N k = upperCrossingTime a b f N k ∧
    lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N k = lowerCrossingTime a b f N k
ω : Ω
h₁ :
  ∃ j ∈ Set.Icc (lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N k ω) N,
    (f j ω - a)⁺ ∈ Set.Ici (b - a)
h₂ : ∃ j ∈ Set.Icc (lowerCrossingTime a b f N k ω) N, f j ω ∈ Set.Ici b
⊢ sInf
      (Set.Icc (lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N k ω) N ∩
        {i : ℕ | b ≤ (f i ω - a)⁺ + a}) =
    sInf (Set.Icc (lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N k ω) N ∩ {i : ℕ | b ≤ f i ω})
have pos : sInf
    (Set.Icc (lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N k ω) N ∩
      {i : ℕ | b - a ≤ (f i ω - a)⁺}) =
  sInf (Set.Icc (lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N k ω) N ∩ {i : ℕ | b ≤ f i ω})
Tactic: simp_rw [← sub_le_iff_le_add, hf ω]