awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Martingale.Upcrossing
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
this : upperCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N (k + 1) = upperCrossingTime a b f N (k + 1)
ω : Ω
h₁ :
  ∃ j ∈ Set.Icc (upperCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N (k + 1) ω) N,
    Membership.mem (γ := Set ℝ) (Set.Iic 0) (f j ω - a)⁺
h₂ : ¬∃ j ∈ Set.Icc (upperCrossingTime a b f N (k + 1) ω) N, f j ω ∈ Set.Iic a
⊢ sInf (Set.Icc (upperCrossingTime a b f N (k + 1) ω) N ∩ {i : ℕ | (f i ω - a)⁺ ≤ 0}) = N

Tactic:
False.elim (h₂ ?_)

Premises used: False.elim
-- Module: Mathlib.Probability.Martingale.Upcrossing
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
this : upperCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N (k + 1) = upperCrossingTime a b f N (k + 1)
ω : Ω
h₁ :
  ∃ j ∈ Set.Icc (upperCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N (k + 1) ω) N,
    Membership.mem (γ := Set ℝ) (Set.Iic 0) (f j ω - a)⁺
h₂ : ¬∃ j ∈ Set.Icc (upperCrossingTime a b f N (k + 1) ω) N, f j ω ∈ Set.Iic a
neg : ∃ j ∈ Set.Icc (upperCrossingTime a b f N (k + 1) ω) N, f j ω ∈ Set.Iic a
⊢ sInf (Set.Icc (upperCrossingTime a b f N (k + 1) ω) N ∩ {i : ℕ | (f i ω - a)⁺ ≤ 0}) = N

Tactic:
refine False.elim (h₂ ?_)

Premises used: False.elim
-- Module: Mathlib.Probability.Martingale.Upcrossing
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
this : upperCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N (k + 1) = upperCrossingTime a b f N (k + 1)
ω : Ω
h₁ :
  ∃ j ∈ Set.Icc (upperCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N (k + 1) ω) N,
    Membership.mem (γ := Set ℝ) (Set.Iic 0) (f j ω - a)⁺
h₂ : ¬∃ j ∈ Set.Icc (upperCrossingTime a b f N (k + 1) ω) N, f j ω ∈ Set.Iic a
⊢ ∃ j ∈ Set.Icc (upperCrossingTime a b f N (k + 1) ω) N, f j ω ∈ Set.Iic a

Tactic:
simp_all only [Set.mem_Iic, not_true_eq_false]

Premises used: not_true_eq_false, Set.mem_Iic
-- Module: Mathlib.Probability.Martingale.Upcrossing
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
this : upperCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N (k + 1) = upperCrossingTime a b f N (k + 1)
ω : Ω
h₁ :
  ¬∃ j ∈ Set.Icc (upperCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N (k + 1) ω) N,
      Membership.mem (γ := Set ℝ) (Set.Iic 0) (f j ω - a)⁺
h₂ : ∃ j ∈ Set.Icc (upperCrossingTime a b f N (k + 1) ω) N, f j ω ∈ Set.Iic a
⊢ N = sInf (Set.Icc (upperCrossingTime a b f N (k + 1) ω) N ∩ {i : ℕ | f i ω ≤ a})

Tactic:
False.elim (h₁ ?_)

Premises used: False.elim
-- Module: Mathlib.Probability.Martingale.Upcrossing
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
this : upperCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N (k + 1) = upperCrossingTime a b f N (k + 1)
ω : Ω
h₁ :
  ¬∃ j ∈ Set.Icc (upperCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N (k + 1) ω) N,
      Membership.mem (γ := Set ℝ) (Set.Iic 0) (f j ω - a)⁺
h₂ : ∃ j ∈ Set.Icc (upperCrossingTime a b f N (k + 1) ω) N, f j ω ∈ Set.Iic a
pos :
  ∃ j ∈ Set.Icc (upperCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N (k + 1) ω) N,
    Membership.mem (γ := Set ℝ) (Set.Iic 0) (f j ω - a)⁺
⊢ N = sInf (Set.Icc (upperCrossingTime a b f N (k + 1) ω) N ∩ {i : ℕ | f i ω ≤ a})

Tactic:
refine False.elim (h₁ ?_)

Premises used: False.elim
-- Module: Mathlib.Probability.Martingale.Upcrossing
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
this : upperCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N (k + 1) = upperCrossingTime a b f N (k + 1)
ω : Ω
h₁ :
  ¬∃ j ∈ Set.Icc (upperCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N (k + 1) ω) N,
      Membership.mem (γ := Set ℝ) (Set.Iic 0) (f j ω - a)⁺
h₂ : ∃ j ∈ Set.Icc (upperCrossingTime a b f N (k + 1) ω) N, f j ω ∈ Set.Iic a
⊢ ∃ j ∈ Set.Icc (upperCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N (k + 1) ω) N,
    Membership.mem (γ := Set ℝ) (Set.Iic 0) (f j ω - a)⁺

Tactic:
simp_all only [Set.mem_Iic]

Premises used: Set.mem_Iic
-- Module: Mathlib.Probability.Martingale.Upcrossing
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
this : upperCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N (k + 1) = upperCrossingTime a b f N (k + 1)
ω : Ω
h₁ :
  ¬∃ j ∈ Set.Icc (upperCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N (k + 1) ω) N,
      Membership.mem (γ := Set ℝ) (Set.Iic 0) (f j ω - a)⁺
h₂ : ¬∃ j ∈ Set.Icc (upperCrossingTime a b f N (k + 1) ω) N, f j ω ∈ Set.Iic a
⊢ N = N

Tactic:
rfl
-- Module: Mathlib.Probability.Martingale.Upcrossing
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
zero :
  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
succ :
  ∀ (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) ∧
      lowerCrossingTime 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N (k + 1) = lowerCrossingTime a b f N (k + 1)
⊢ 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

Tactic:
induction n with
  | zero =>
    refine ⟨rfl, ?_⟩
    simp +unfoldPartialApp only [lowerCrossingTime_zero, hittingBtwn,
      Set.mem_Icc, Set.mem_Iic]
    simp_all
  | succ k ih =>
    have : upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N (k + 1) =
        upperCrossingTime a b f N (k + 1) := by
      ext ω
      simp only [upperCrossingTime_succ_eq, ← ih.2, hittingBtwn, Set.mem_Ici, tsub_le_iff_right]
      split_ifs with h₁ h₂ h₂
      · simp_rw [← sub_le_iff_le_add, hf ω]
      · refine False.elim (h₂ ?_)
        simp_all only [Set.mem_Ici, not_true_eq_false]
      · refine False.elim (h₁ ?_)
        simp_all only [Set.mem_Ici]
      · rfl
    refine ⟨this, ?_⟩
    ext ω
    simp only [lowerCrossingTime, this, hittingBtwn, Set.mem_Iic]
    split_ifs with h₁ h₂ h₂
    · simp_rw [hf' ω]
    · refine False.elim (h₂ ?_)
      simp_all only [Set.mem_Iic, not_true_eq_false]
    · refine False.elim (h₁ ?_)
      simp_all only [Set.mem_Iic]
    · rfl

Premises used: MeasureTheory.lowerCrossingTime, MeasureTheory.lowerCrossingTime_zero, not_true_eq_false, MeasureTheory.hittingBtwn, Set.mem_Icc, Set.mem_Iic
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hab : a < b
⊢ (b - a) * ∫ (x : Ω), (↑(upcrossingsBefore a b f N x) : ℝ) ∂μ ≤ ∫ (x : Ω), (fun (ω : Ω) ↦ (f N ω - a)⁺) x ∂μ

Tactic:
le_trans (le_of_eq ?_)
    (integral_mul_upcrossingsBefore_le_integral (hf.sub_martingale (martingale_const _ _ _)).pos
      (fun ω => posPart_nonneg _)
      (fun ω => posPart_nonneg _) (sub_pos.2 hab))

Premises used: Iff.mpr, sub_pos, MeasureTheory.martingale_const, MeasureTheory.integral_mul_upcrossingsBefore_le_integral, posPart_nonneg, HSub.hSub, MeasureTheory.Submartingale.pos, le_of_eq, OfNat.ofNat, MeasureTheory.Submartingale.sub_martingale, le_trans
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hab : a < b
refine :
  (b - a) * ∫ (x : Ω), (↑(upcrossingsBefore a b f N x) : ℝ) ∂μ =
    (b - a - 0) * ∫ (x : Ω), (↑(upcrossingsBefore 0 (b - a) (f - fun (x : ℕ) (x_1 : Ω) ↦ a)⁺ N x) : ℝ) ∂μ
⊢ (b - a) * ∫ (x : Ω), (↑(upcrossingsBefore a b f N x) : ℝ) ∂μ ≤ ∫ (x : Ω), (fun (ω : Ω) ↦ (f N ω - a)⁺) x ∂μ

Tactic:
refine le_trans (le_of_eq ?_)
    (integral_mul_upcrossingsBefore_le_integral (hf.sub_martingale (martingale_const _ _ _)).pos
      (fun ω => posPart_nonneg _)
      (fun ω => posPart_nonneg _) (sub_pos.2 hab))

Premises used: Iff.mpr, sub_pos, MeasureTheory.martingale_const, MeasureTheory.integral_mul_upcrossingsBefore_le_integral, posPart_nonneg, HSub.hSub, MeasureTheory.Submartingale.pos, le_of_eq, OfNat.ofNat, MeasureTheory.Submartingale.sub_martingale, le_trans
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hab : a < b
simp_rw :
  (b - a) * ∫ (x : Ω), (↑(upcrossingsBefore 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N x) : ℝ) ∂μ =
    (b - a) * ∫ (x : Ω), (↑(upcrossingsBefore 0 (b - a) (f - fun (x : ℕ) (x_1 : Ω) ↦ a)⁺ N x) : ℝ) ∂μ
⊢ (b - a) * ∫ (x : Ω), (↑(upcrossingsBefore a b f N x) : ℝ) ∂μ =
    (b - a - 0) * ∫ (x : Ω), (↑(upcrossingsBefore 0 (b - a) (f - fun (x : ℕ) (x_1 : Ω) ↦ a)⁺ N x) : ℝ) ∂μ

Tactic:
simp_rw [sub_zero, ← upcrossingsBefore_pos_eq hab]

Premises used: sub_zero, MeasureTheory.upcrossingsBefore_pos_eq
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hab : a < b
⊢ (b - a) * ∫ (x : Ω), (↑(upcrossingsBefore 0 (b - a) (fun (n : ℕ) (ω : Ω) ↦ (f n ω - a)⁺) N x) : ℝ) ∂μ =
    (b - a) * ∫ (x : Ω), (↑(upcrossingsBefore 0 (b - a) (f - fun (x : ℕ) (x_1 : Ω) ↦ a)⁺ N x) : ℝ) ∂μ

Tactic:
rfl
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
N : ℕ
pos :
  ∀ (hab : a < b),
    (b - a) * ∫ (x : Ω), (↑(upcrossingsBefore a b f N x) : ℝ) ∂μ ≤ ∫ (x : Ω), (fun (ω : Ω) ↦ (f N ω - a)⁺) x ∂μ
neg :
  ∀ (hab : b ≤ a),
    (b - a) * ∫ (x : Ω), (↑(upcrossingsBefore a b f N x) : ℝ) ∂μ ≤ ∫ (x : Ω), (fun (ω : Ω) ↦ (f N ω - a)⁺) x ∂μ
⊢ (b - a) * ∫ (x : Ω), (↑(upcrossingsBefore a b f N x) : ℝ) ∂μ ≤ ∫ (x : Ω), (fun (ω : Ω) ↦ (f N ω - a)⁺) x ∂μ

Tactic:
by_cases! hab : a < b
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
N : ℕ
hab : a < b
⊢ (b - a) * ∫ (x : Ω), (↑(upcrossingsBefore a b f N x) : ℝ) ∂μ ≤ ∫ (x : Ω), (fun (ω : Ω) ↦ (f N ω - a)⁺) x ∂μ

Tactic:
mul_integral_upcrossingsBefore_le_integral_pos_part_aux hf hab

Premises used: MeasureTheory.mul_integral_upcrossingsBefore_le_integral_pos_part_aux
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
N : ℕ
hab : a < b
⊢ (b - a) * ∫ (x : Ω), (↑(upcrossingsBefore a b f N x) : ℝ) ∂μ ≤ ∫ (x : Ω), (fun (ω : Ω) ↦ (f N ω - a)⁺) x ∂μ

Tactic:
exact mul_integral_upcrossingsBefore_le_integral_pos_part_aux hf hab

Premises used: MeasureTheory.mul_integral_upcrossingsBefore_le_integral_pos_part_aux
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
N : ℕ
hab : b ≤ a
⊢ b - a ≤ 0

Tactic:
rw [← sub_nonpos] at hab

Premises used: sub_nonpos
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
N : ℕ
hab : b - a ≤ 0
⊢ LE.le (α := ℝ) 0 (∫ (x : Ω), (↑(upcrossingsBefore a b f N x) : ℝ) ∂μ)

Tactic:
positivity
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
N : ℕ
hab : b - a ≤ 0
⊢ (b - a) * ∫ (x : Ω), (↑(upcrossingsBefore a b f N x) : ℝ) ∂μ ≤ ∫ (x : Ω), (fun (ω : Ω) ↦ (f N ω - a)⁺) x ∂μ

Tactic:
exact le_trans (mul_nonpos_of_nonpos_of_nonneg hab (by positivity))
      (integral_nonneg fun ω => posPart_nonneg _)

Premises used: MeasureTheory.integral_nonneg, mul_nonpos_of_nonpos_of_nonneg, posPart_nonneg, le_trans
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
pos :
  ∀ (hN : N = 0),
    upcrossingsBefore a b f N ω =
      ∑ i ∈ Finset.Ico 1 (N + 1), Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 i
neg :
  ∀ (hN : ¬N = 0),
    upcrossingsBefore a b f N ω =
      ∑ i ∈ Finset.Ico 1 (N + 1), Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 i
⊢ upcrossingsBefore a b f N ω =
    ∑ i ∈ Finset.Ico 1 (N + 1), Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 i

Tactic:
by_cases hN : N = 0
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN : N = 0
⊢ upcrossingsBefore a b f N ω =
    ∑ i ∈ Finset.Ico 1 (N + 1), Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 i

Tactic:
simp [hN]
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN : ¬N = 0
neg :
  upcrossingsBefore a b f N ω =
    HAdd.hAdd (α := ℕ)
      (∑ i ∈ Finset.Ico (Nat.succ 0) (upcrossingsBefore a b f N ω).succ,
        Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 i)
      (∑ i ∈ Finset.Ico (upcrossingsBefore a b f N ω).succ N.succ,
        Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 i)
⊢ upcrossingsBefore a b f N ω =
    ∑ i ∈ Finset.Ico 1 (N + 1), Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 i

Tactic:
rw [← Finset.sum_Ico_consecutive _ (Nat.succ_le_succ zero_le')
    (Nat.succ_le_succ (upcrossingsBefore_le f ω hab))]

Premises used: MeasureTheory.upcrossingsBefore_le, Finset.sum_Ico_consecutive, zero_le', Nat.succ_le_succ
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN : ¬N = 0
k : ℕ
hk : k ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1)
⊢ 1 ≤ k ∧ k < upcrossingsBefore a b f N ω + 1

Tactic:
rw [Finset.mem_Ico] at hk

Premises used: Finset.mem_Ico
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN : ¬N = 0
k : ℕ
hk : 1 ≤ k ∧ k < upcrossingsBefore a b f N ω + 1
rw : Eq (α := ℕ) (1 k) 1
h : Membership.mem (γ := Set ℕ) {n : ℕ | upperCrossingTime a b f N n ω < N} k
⊢ Eq (α := ℕ) (Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 k) 1

Tactic:
rw [Set.indicator_of_mem]

Premises used: Set.indicator_of_mem
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN : ¬N = 0
k : ℕ
hk : 1 ≤ k ∧ k < upcrossingsBefore a b f N ω + 1
⊢ Eq (α := ℕ) (1 k) 1

Tactic:
rfl
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN : ¬N = 0
k : ℕ
hk : 1 ≤ k ∧ k < upcrossingsBefore a b f N ω + 1
⊢ Membership.mem (γ := Set ℕ) {n : ℕ | upperCrossingTime a b f N n ω < N} k

Tactic:
upperCrossingTime_lt_of_le_upcrossingsBefore (zero_lt_iff.2 hN) hab
        (Nat.lt_succ_iff.1 hk.2)

Premises used: Iff.mpr, Set.Mem, MeasureTheory.upperCrossingTime_lt_of_le_upcrossingsBefore, setOf, And.right, Nat.lt_succ_iff, Iff.mp, zero_lt_iff, Nat.lt
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN : ¬N = 0
k : ℕ
hk : 1 ≤ k ∧ k < upcrossingsBefore a b f N ω + 1
⊢ Membership.mem (γ := Set ℕ) {n : ℕ | upperCrossingTime a b f N n ω < N} k

Tactic:
exact upperCrossingTime_lt_of_le_upcrossingsBefore (zero_lt_iff.2 hN) hab
        (Nat.lt_succ_iff.1 hk.2)

Premises used: Iff.mpr, MeasureTheory.upperCrossingTime_lt_of_le_upcrossingsBefore, And.right, Nat.lt_succ_iff, Iff.mp, zero_lt_iff
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN : ¬N = 0
⊢ ∀ k ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1),
    Eq (α := ℕ) (Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 k) 1

Tactic:
have h₁ : ∀ k ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1),
      {n : ℕ | upperCrossingTime a b f N n ω < N}.indicator 1 k = 1 := by
    rintro k hk
    rw [Finset.mem_Ico] at hk
    rw [Set.indicator_of_mem]
    · rfl
    · exact upperCrossingTime_lt_of_le_upcrossingsBefore (zero_lt_iff.2 hN) hab
        (Nat.lt_succ_iff.1 hk.2)
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ k ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1),
    Eq (α := ℕ) (Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 k) 1
k : ℕ
hk : k ∈ Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1)
⊢ upcrossingsBefore a b f N ω < k ∧ k < N + 1

Tactic:
rw [Finset.mem_Ico, Nat.succ_le_iff] at hk

Premises used: Nat.succ_le_iff, Finset.mem_Ico
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ k ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1),
    Eq (α := ℕ) (Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 k) 1
k : ℕ
hk : upcrossingsBefore a b f N ω < k ∧ k < N + 1
h : k ∉ {n : ℕ | upperCrossingTime a b f N n ω < N}
⊢ Eq (α := ℕ) (Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 k) 0

Tactic:
rw [Set.indicator_of_notMem]

Premises used: Set.indicator_of_notMem
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ k ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1),
    Eq (α := ℕ) (Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 k) 1
k : ℕ
hk : upcrossingsBefore a b f N ω < k ∧ k < N + 1
h : N ≤ upperCrossingTime a b f N k ω
⊢ k ∉ {n : ℕ | upperCrossingTime a b f N n ω < N}

Tactic:
simp only [Set.mem_setOf_eq, not_lt]

Premises used: Set.mem_setOf_eq, not_lt
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ k ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1),
    Eq (α := ℕ) (Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 k) 1
k : ℕ
hk : upcrossingsBefore a b f N ω < k ∧ k < N + 1
⊢ N ≤ upperCrossingTime a b f N k ω

Tactic:
(upperCrossingTime_eq_of_upcrossingsBefore_lt hab hk.1).symm.le

Premises used: Eq.le, And.left, Eq.symm, MeasureTheory.upperCrossingTime_eq_of_upcrossingsBefore_lt
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ k ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1),
    Eq (α := ℕ) (Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 k) 1
k : ℕ
hk : upcrossingsBefore a b f N ω < k ∧ k < N + 1
⊢ N ≤ upperCrossingTime a b f N k ω

Tactic:
exact (upperCrossingTime_eq_of_upcrossingsBefore_lt hab hk.1).symm.le

Premises used: Eq.le, And.left, Eq.symm, MeasureTheory.upperCrossingTime_eq_of_upcrossingsBefore_lt
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ k ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1),
    Eq (α := ℕ) (Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 k) 1
⊢ ∀ k ∈ Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1),
    Eq (α := ℕ) (Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 k) 0

Tactic:
have h₂ : ∀ k ∈ Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1),
      {n : ℕ | upperCrossingTime a b f N n ω < N}.indicator 1 k = 0 := by
    rintro k hk
    rw [Finset.mem_Ico, Nat.succ_le_iff] at hk
    rw [Set.indicator_of_notMem]
    simp only [Set.mem_setOf_eq, not_lt]
    exact (upperCrossingTime_eq_of_upcrossingsBefore_lt hab hk.1).symm.le