awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 n ω) : WithTop ℕ)) ∧
    IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N n ω) : WithTop ℕ)
have zero : (IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N 0 ω) : WithTop ℕ)) ∧
  IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N 0 ω) : WithTop ℕ)
Tactic: induction n with
  | zero =>
    refine ⟨isStoppingTime_const _ 0, ?_⟩
    simp only [lowerCrossingTime_zero, Nat.bot_eq_zero]
    exact hf.adapted.isStoppingTime_hittingBtwn measurableSet_Iic
  | succ k ih =>
    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]
    refine ⟨this, fun n ↦ ?_⟩
    refine hf.adapted.isStoppingTime_hittingBtwn_isStoppingTime this ?_ measurableSet_Iic _
    simp [upperCrossingTime_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
zero :
  (IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N 0 ω) : WithTop ℕ)) ∧
    IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N 0 ω) : WithTop ℕ)
⊢ (IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N n ω) : WithTop ℕ)) ∧
    IsStoppingTime ℱ fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N n ω) : WithTop ℕ)
have succ : ∀ (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 ℕ)
Tactic: induction n with
  | zero =>
    refine ⟨isStoppingTime_const _ 0, ?_⟩
    simp only [lowerCrossingTime_zero, Nat.bot_eq_zero]
    exact hf.adapted.isStoppingTime_hittingBtwn measurableSet_Iic
  | succ k ih =>
    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]
    refine ⟨this, fun n ↦ ?_⟩
    refine hf.adapted.isStoppingTime_hittingBtwn_isStoppingTime this ?_ measurableSet_Iic _
    simp [upperCrossingTime_le]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
⊢ upcrossingStrat a b f N n ω ≤ 1
have rw : LE.le (α := ℝ)
  (Set.indicator (⋃ i ∈ Finset.range N, Set.Ico (lowerCrossingTime a b f N i ω) (upperCrossingTime a b f N (i + 1) ω)) 1
    n)
  1
Tactic: rw [upcrossingStrat, ← Finset.indicator_biUnion_apply]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
rw :
  LE.le (α := ℝ)
    (Set.indicator (⋃ i ∈ Finset.range N, Set.Ico (lowerCrossingTime a b f N i ω) (upperCrossingTime a b f N (i + 1) ω))
      1 n)
    1
⊢ upcrossingStrat a b f N n ω ≤ 1
have h : (↑(Finset.range N) : Set ℕ).PairwiseDisjoint (α := Set ℕ) fun (k : ℕ) ↦
  Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)
Tactic: rw [upcrossingStrat, ← Finset.indicator_biUnion_apply]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
i : ℕ
h : i ∈ (↑(Finset.range N) : Set ℕ)
j : ℕ
h_1 : j ∈ (↑(Finset.range N) : Set ℕ)
hij : i ≠ j
⊢ Function.onFun (β := Set ℕ) Disjoint
    (fun (k : ℕ) ↦ Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)) i j
have h : min (upperCrossingTime a b f N (i + 1) ω) (upperCrossingTime a b f N (j + 1) ω) ≤
  max (lowerCrossingTime a b f N i ω) (lowerCrossingTime a b f N j ω)
Tactic: simp only [Set.Ico_disjoint_Ico]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
i : ℕ
h : i ∈ (↑(Finset.range N) : Set ℕ)
j : ℕ
h_1 : j ∈ (↑(Finset.range N) : Set ℕ)
hij : i ≠ j
⊢ min (upperCrossingTime a b f N (i + 1) ω) (upperCrossingTime a b f N (j + 1) ω) ≤
    max (lowerCrossingTime a b f N i ω) (lowerCrossingTime a b f N j ω)
have h : ∀ (hij' : i < j),
  min (upperCrossingTime a b f N (i + 1) ω) (upperCrossingTime a b f N (j + 1) ω) ≤
    max (lowerCrossingTime a b f N i ω) (lowerCrossingTime a b f N j ω)
Tactic: obtain hij' | hij' := lt_or_gt_of_ne hij
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
i : ℕ
h_1 : i ∈ (↑(Finset.range N) : Set ℕ)
j : ℕ
h_2 : j ∈ (↑(Finset.range N) : Set ℕ)
hij : i ≠ j
h :
  ∀ (hij' : i < j),
    min (upperCrossingTime a b f N (i + 1) ω) (upperCrossingTime a b f N (j + 1) ω) ≤
      max (lowerCrossingTime a b f N i ω) (lowerCrossingTime a b f N j ω)
⊢ min (upperCrossingTime a b f N (i + 1) ω) (upperCrossingTime a b f N (j + 1) ω) ≤
    max (lowerCrossingTime a b f N i ω) (lowerCrossingTime a b f N j ω)
have h₁ : ∀ (hij' : j < i),
  min (upperCrossingTime a b f N (i + 1) ω) (upperCrossingTime a b f N (j + 1) ω) ≤
    max (lowerCrossingTime a b f N i ω) (lowerCrossingTime a b f N j ω)
Tactic: obtain hij' | hij' := lt_or_gt_of_ne hij
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
i : ℕ
h : i ∈ (↑(Finset.range N) : Set ℕ)
j : ℕ
h_1 : j ∈ (↑(Finset.range N) : Set ℕ)
hij : i ≠ j
hij' : i < j
⊢ min (upperCrossingTime a b f N (i + 1) ω) (upperCrossingTime a b f N (j + 1) ω) ≤
    max (lowerCrossingTime a b f N i ω) (lowerCrossingTime a b f N j ω)
have h : upperCrossingTime a b f N i.succ ω ≤ lowerCrossingTime a b f N j ω
Tactic: rw [min_eq_left (upperCrossingTime_mono (Nat.succ_le_succ hij'.le) :
      upperCrossingTime a b f N _ ω ≤ upperCrossingTime a b f N _ ω),
      max_eq_right (lowerCrossingTime_mono hij'.le :
        lowerCrossingTime a b f N _ _ ≤ lowerCrossingTime _ _ _ _ _ _)]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
i : ℕ
h : i ∈ (↑(Finset.range N) : Set ℕ)
j : ℕ
h_1 : j ∈ (↑(Finset.range N) : Set ℕ)
hij : i ≠ j
hij' : j < i
⊢ min (upperCrossingTime a b f N (i + 1) ω) (upperCrossingTime a b f N (j + 1) ω) ≤
    max (lowerCrossingTime a b f N i ω) (lowerCrossingTime a b f N j ω)
have h : upperCrossingTime a b f N j.succ ω ≤ lowerCrossingTime a b f N i ω
Tactic: rw [min_eq_right (upperCrossingTime_mono (Nat.succ_le_succ hij'.le) :
      upperCrossingTime a b f N _ ω ≤ upperCrossingTime a b f N _ ω),
      max_eq_left (lowerCrossingTime_mono hij'.le :
        lowerCrossingTime a b f N _ _ ≤ lowerCrossingTime _ _ _ _ _ _)]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
n : ℕ
⊢ StronglyMeasurable (β := (fun (i : ℕ) ↦ ℝ) n) fun (ω : Ω) ↦
    ∑ k ∈ Finset.range N,
      Set.indicator ({n : ℕ | lowerCrossingTime a b f N k ω ≤ n} ∩ {n : ℕ | n < upperCrossingTime a b f N (k + 1) ω}) 1
        n
have refine : ∀ i ∈ Finset.range N,
  MeasurableSet.{u_1} (α := Ω) fun (ω : Ω) ↦
    ({n : ℕ | lowerCrossingTime a b f N i ω ≤ n} ∩ {n : ℕ | n < upperCrossingTime a b f N (i + 1) ω}) n
Tactic: refine Finset.stronglyMeasurable_fun_sum _ fun i _ =>
    stronglyMeasurable_const.indicator ?_
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (hypothesis)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
n i : ℕ
h : i ∈ Finset.range N
⊢ MeasurableSet.{u_1} (α := Ω) fun (ω : Ω) ↦
    ({n : ℕ | lowerCrossingTime a b f N i ω ≤ n} ∩ {n : ℕ | n < upperCrossingTime a b f N (i + 1) ω}) n
have hl : MeasurableSet.{u_1} (α := Ω)
  {ω : Ω | (fun (ω : Ω) ↦ ((↑(lowerCrossingTime a b f N i ω) : WithTop ℕ) : WithTop ℕ)) ω ≤ (↑n : WithTop ℕ)}
Tactic: have hl := hf.isStoppingTime_lowerCrossingTime (a := a) (b := b) (N := N) (n := i) n
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (hypothesis)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
n i : ℕ
h : i ∈ Finset.range N
hl :
  MeasurableSet.{u_1} (α := Ω)
    {ω : Ω | (fun (ω : Ω) ↦ ((↑(lowerCrossingTime a b f N i ω) : WithTop ℕ) : WithTop ℕ)) ω ≤ (↑n : WithTop ℕ)}
⊢ MeasurableSet.{u_1} (α := Ω) fun (ω : Ω) ↦
    ({n : ℕ | lowerCrossingTime a b f N i ω ≤ n} ∩ {n : ℕ | n < upperCrossingTime a b f N (i + 1) ω}) n
have hu : MeasurableSet.{u_1} (α := Ω)
  {ω : Ω | (fun (ω : Ω) ↦ ((↑(upperCrossingTime a b f N (i + 1) ω) : WithTop ℕ) : WithTop ℕ)) ω ≤ (↑n : WithTop ℕ)}
Tactic: have hu := hf.isStoppingTime_upperCrossingTime (a := a) (b := b) (N := N) (n := i + 1) n
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (hypothesis)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
n i : ℕ
h : i ∈ Finset.range N
hl :
  MeasurableSet.{u_1} (α := Ω)
    {ω : Ω | (fun (ω : Ω) ↦ ((↑(lowerCrossingTime a b f N i ω) : WithTop ℕ) : WithTop ℕ)) ω ≤ (↑n : WithTop ℕ)}
hu :
  MeasurableSet.{u_1} (α := Ω)
    {ω : Ω | (fun (ω : Ω) ↦ ((↑(upperCrossingTime a b f N (i + 1) ω) : WithTop ℕ) : WithTop ℕ)) ω ≤ (↑n : WithTop ℕ)}
⊢ MeasurableSet.{u_1} (α := Ω) fun (ω : Ω) ↦
    ({n : ℕ | lowerCrossingTime a b f N i ω ≤ n} ∩ {n : ℕ | n < upperCrossingTime a b f N (i + 1) ω}) n
have hl₁ : MeasurableSet.{u_1} (α := Ω) {ω : Ω | lowerCrossingTime a b f N i ω ≤ n}
Tactic: simp only [ENat.some_eq_coe, Nat.cast_le] at hl hu
Cleared hypotheses: hl, hu
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (hypothesis)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
n i : ℕ
h : i ∈ Finset.range N
hl :
  MeasurableSet.{u_1} (α := Ω)
    {ω : Ω | (fun (ω : Ω) ↦ ((↑(lowerCrossingTime a b f N i ω) : WithTop ℕ) : WithTop ℕ)) ω ≤ (↑n : WithTop ℕ)}
hu :
  MeasurableSet.{u_1} (α := Ω)
    {ω : Ω | (fun (ω : Ω) ↦ ((↑(upperCrossingTime a b f N (i + 1) ω) : WithTop ℕ) : WithTop ℕ)) ω ≤ (↑n : WithTop ℕ)}
hl₁ : MeasurableSet.{u_1} (α := Ω) {ω : Ω | lowerCrossingTime a b f N i ω ≤ n}
⊢ MeasurableSet.{u_1} (α := Ω) fun (ω : Ω) ↦
    ({n : ℕ | lowerCrossingTime a b f N i ω ≤ n} ∩ {n : ℕ | n < upperCrossingTime a b f N (i + 1) ω}) n
have hu₁ : MeasurableSet.{u_1} (α := Ω) {ω : Ω | upperCrossingTime a b f N (i + 1) ω ≤ n}
Tactic: simp only [ENat.some_eq_coe, Nat.cast_le] at hl hu
Cleared hypotheses: hl, hu
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
n i : ℕ
h : i ∈ Finset.range N
hl : MeasurableSet.{u_1} (α := Ω) {ω : Ω | lowerCrossingTime a b f N i ω ≤ n}
hu : MeasurableSet.{u_1} (α := Ω) {ω : Ω | upperCrossingTime a b f N (i + 1) ω ≤ n}
⊢ MeasurableSet.{u_1} (α := Ω) fun (ω : Ω) ↦
    ({n : ℕ | lowerCrossingTime a b f N i ω ≤ n} ∩ {n : ℕ | n < upperCrossingTime a b f N (i + 1) ω}) n
have simp_rw : MeasurableSet.{u_1} (α := Ω) fun (ω : Ω) ↦
  ({n : ℕ | lowerCrossingTime a b f N i ω ≤ n} ∩ {n : ℕ | ¬upperCrossingTime a b f N (i + 1) ω ≤ n}) n
Tactic: simp_rw [← not_le]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
a b : ℝ
N : ℕ
⊢ Submartingale (E := ℝ) (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) ℱ μ
have refine_1 : ∀ (n : ℕ) (ω : Ω), HSub.hSub (α := (ω : Ω) → ℝ) 1 (upcrossingStrat a b f N n) ω ≤ 1
Tactic: refine hf.sum_mul_sub
    (fun n => (stronglyAdapted_const ℱ 1 n).sub (hf.stronglyAdapted.upcrossingStrat n))
    (?_ : ∀ n ω, (1 - upcrossingStrat a b f N n) ω ≤ 1) ?_
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
a b : ℝ
N : ℕ
refine_1 : ∀ (n : ℕ) (ω : Ω), HSub.hSub (α := (ω : Ω) → ℝ) 1 (upcrossingStrat a b f N n) ω ≤ 1
⊢ Submartingale (E := ℝ) (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) ℱ μ
have refine_2 : ∀ (n : ℕ) (ω : Ω), 0 ≤ HSub.hSub (α := (ω : Ω) → ℝ) 1 (upcrossingStrat a b f N n) ω
Tactic: refine hf.sum_mul_sub
    (fun n => (stronglyAdapted_const ℱ 1 n).sub (hf.stronglyAdapted.upcrossingStrat n))
    (?_ : ∀ n ω, (1 - upcrossingStrat a b f N n) ω ≤ 1) ?_
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (hypothesis)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
⊢ LE.le (α := ℝ) 0 (∫ (x : Ω), (∑ k ∈ Finset.range n, (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) x ∂μ)
have this : LE.le (α := ℝ) (∫ (ω : Ω) in Set.univ, (∑ k ∈ Finset.range 0, (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) ω ∂μ)
  (∫ (ω : Ω) in Set.univ, (∑ k ∈ Finset.range n, (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) ω ∂μ)
Tactic: have := (hf.sum_sub_upcrossingStrat_mul a b N).setIntegral_le (zero_le (a := n)) .univ
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (hypothesis)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
this :
  LE.le (α := ℝ)
    (∫ (ω : Ω) in Set.univ, (∑ k ∈ Finset.range 0, (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) ω ∂μ)
    (∫ (ω : Ω) in Set.univ, (∑ k ∈ Finset.range n, (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) ω ∂μ)
⊢ LE.le (α := ℝ) 0 (∫ (x : Ω), (∑ k ∈ Finset.range n, (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) x ∂μ)
have this₁ : LE.le (α := ℝ) (∫ (x : Ω), (∑ k ∈ Finset.range 0, (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) x ∂μ)
  (∫ (x : Ω), (∑ k ∈ Finset.range n, (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) x ∂μ)
Tactic: rw [setIntegral_univ, setIntegral_univ] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
this :
  LE.le (α := ℝ) (∫ (x : Ω), (∑ k ∈ Finset.range 0, (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) x ∂μ)
    (∫ (x : Ω), (∑ k ∈ Finset.range n, (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) x ∂μ)
⊢ LE.le (α := ℝ) 0 (∫ (x : Ω), (∑ k ∈ Finset.range n, (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) x ∂μ)
have refine : LE.le (α := ℝ) 0 (∫ (x : Ω), (∑ k ∈ Finset.range 0, (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) x ∂μ)
Tactic: refine le_trans ?_ this
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (hypothesis)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
⊢ ∫ (x : Ω), (∑ k ∈ Finset.range n, upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ ≤
    HSub.hSub (α := ℝ) (∫ (x : Ω), f n x ∂μ) (∫ (x : Ω), f 0 x ∂μ)
have h₁ : LE.le (α := ℝ) 0 (∫ (x : Ω), (∑ k ∈ Finset.range n, (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) x ∂μ)
Tactic: have h₁ : (0 : ℝ) ≤
      μ[∑ k ∈ Finset.range n, (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)] := by
    have := (hf.sum_sub_upcrossingStrat_mul a b N).setIntegral_le (zero_le (a := n)) .univ
    rw [setIntegral_univ, setIntegral_univ] at this
    refine le_trans ?_ this
    simp only [Finset.range_zero, Finset.sum_empty, integral_zero', le_refl]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
h₁ : LE.le (α := ℝ) 0 (∫ (x : Ω), (∑ k ∈ Finset.range n, (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) x ∂μ)
⊢ ∫ (x : Ω), (∑ k ∈ Finset.range n, (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) x ∂μ =
    HSub.hSub (α := ℝ) (∫ (x : Ω), (∑ k ∈ Finset.range n, (f (k + 1) - f k)) x ∂μ)
      (∫ (x : Ω), (∑ k ∈ Finset.range n, upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ)
have simp : ∫ (x : Ω),
    HSub.hSub (α := ℝ) (∑ x_1 ∈ Finset.range n, f (x_1 + 1) x) (∑ x_1 ∈ Finset.range n, f x_1 x) -
      ∑ x_1 ∈ Finset.range n, upcrossingStrat a b f N x_1 x * (f (x_1 + 1) x - f x_1 x) ∂μ =
  HSub.hSub (α := ℝ)
    (∫ (x : Ω), HSub.hSub (α := ℝ) (∑ x_1 ∈ Finset.range n, f (x_1 + 1) x) (∑ x_1 ∈ Finset.range n, f x_1 x) ∂μ)
    (∫ (x : Ω), ∑ x_1 ∈ Finset.range n, upcrossingStrat a b f N x_1 x * (f (x_1 + 1) x - f x_1 x) ∂μ)
Tactic: simp only [sub_mul, one_mul, Finset.sum_sub_distrib, Pi.sub_apply, Finset.sum_apply,
      Pi.mul_apply]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
h₁ : LE.le (α := ℝ) 0 (∫ (x : Ω), (∑ k ∈ Finset.range n, (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) x ∂μ)
⊢ ∫ (x : Ω),
      HSub.hSub (α := ℝ) (∑ x_1 ∈ Finset.range n, f (x_1 + 1) x) (∑ x_1 ∈ Finset.range n, f x_1 x) -
        ∑ x_1 ∈ Finset.range n, upcrossingStrat a b f N x_1 x * (f (x_1 + 1) x - f x_1 x) ∂μ =
    HSub.hSub (α := ℝ)
      (∫ (x : Ω), HSub.hSub (α := ℝ) (∑ x_1 ∈ Finset.range n, f (x_1 + 1) x) (∑ x_1 ∈ Finset.range n, f x_1 x) ∂μ)
      (∫ (x : Ω), ∑ x_1 ∈ Finset.range n, upcrossingStrat a b f N x_1 x * (f (x_1 + 1) x - f x_1 x) ∂μ)
have refine : Integrable (ε := ℝ) (fun (x : Ω) ↦ ∑ x_1 ∈ Finset.range n, upcrossingStrat a b f N x_1 x * (f (x_1 + 1) x - f x_1 x)) μ
Tactic: refine integral_sub (Integrable.sub (integrable_finsetSum _ fun i _ => hf.integrable _)
      (integrable_finsetSum _ fun i _ => hf.integrable _)) ?_
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
h₁ : LE.le (α := ℝ) 0 (∫ (x : Ω), (∑ k ∈ Finset.range n, (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) x ∂μ)
⊢ Integrable (ε := ℝ) (fun (x : Ω) ↦ ∑ x_1 ∈ Finset.range n, upcrossingStrat a b f N x_1 x * (f (x_1 + 1) x - f x_1 x))
    μ
have h : Eq.{u_1 + 1} (α := Ω → ℝ)
  (fun (x : Ω) ↦ ∑ x_1 ∈ Finset.range n, upcrossingStrat a b f N x_1 x * (f (x_1 + 1) x - f x_1 x))
  (∑ k ∈ Finset.range n, upcrossingStrat a b f N k * (f (k + 1) - f k))
Tactic: convert! (hf.sum_upcrossingStrat_mul a b N).integrable n using 1
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
h₁ : LE.le (α := ℝ) 0 (∫ (x : Ω), (∑ k ∈ Finset.range n, (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) x ∂μ)
⊢ Eq.{u_1 + 1} (α := Ω → ℝ)
    (fun (x : Ω) ↦ ∑ x_1 ∈ Finset.range n, upcrossingStrat a b f N x_1 x * (f (x_1 + 1) x - f x_1 x))
    (∑ k ∈ Finset.range n, upcrossingStrat a b f N k * (f (k + 1) - f k))
have h : ∀ (x : Ω),
  Eq (α := ℝ) (∑ x_1 ∈ Finset.range n, upcrossingStrat a b f N x_1 x * (f (x_1 + 1) x - f x_1 x))
    ((∑ k ∈ Finset.range n, upcrossingStrat a b f N k * (f (k + 1) - f k)) x)
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (hypothesis)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
h₁ : LE.le (α := ℝ) 0 (∫ (x : Ω), (∑ k ∈ Finset.range n, (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) x ∂μ)
⊢ ∫ (x : Ω), (∑ k ∈ Finset.range n, upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ ≤
    HSub.hSub (α := ℝ) (∫ (x : Ω), f n x ∂μ) (∫ (x : Ω), f 0 x ∂μ)
have h₂ : ∫ (x : Ω), (∑ k ∈ Finset.range n, (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) x ∂μ =
  HSub.hSub (α := ℝ) (∫ (x : Ω), (∑ k ∈ Finset.range n, (f (k + 1) - f k)) x ∂μ)
    (∫ (x : Ω), (∑ k ∈ Finset.range n, upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ)
Tactic: have h₂ : μ[∑ k ∈ Finset.range n, (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)] =
    μ[∑ k ∈ Finset.range n, (f (k + 1) - f k)] -
      μ[∑ k ∈ Finset.range n, upcrossingStrat a b f N k * (f (k + 1) - f k)] := by
    simp only [sub_mul, one_mul, Finset.sum_sub_distrib, Pi.sub_apply, Finset.sum_apply,
      Pi.mul_apply]
    refine integral_sub (Integrable.sub (integrable_finsetSum _ fun i _ => hf.integrable _)
      (integrable_finsetSum _ fun i _ => hf.integrable _)) ?_
    convert! (hf.sum_upcrossingStrat_mul a b N).integrable n using 1
    ext; simp
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (hypothesis)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
h₁ : LE.le (α := ℝ) 0 (∫ (x : Ω), (∑ k ∈ Finset.range n, (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) x ∂μ)
h₂ :
  ∫ (x : Ω), (∑ k ∈ Finset.range n, (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) x ∂μ =
    HSub.hSub (α := ℝ) (∫ (x : Ω), (∑ k ∈ Finset.range n, (f (k + 1) - f k)) x ∂μ)
      (∫ (x : Ω), (∑ k ∈ Finset.range n, upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ)
⊢ ∫ (x : Ω), (∑ k ∈ Finset.range n, upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ ≤
    HSub.hSub (α := ℝ) (∫ (x : Ω), f n x ∂μ) (∫ (x : Ω), f 0 x ∂μ)
have h₃ : LE.le (α := ℝ) (∫ (x : Ω), (∑ k ∈ Finset.range n, upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ)
  (∫ (x : Ω), (∑ k ∈ Finset.range n, (f (k + 1) - f k)) x ∂μ)
Tactic: rw [h₂, sub_nonneg] at h₁
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
h₁ :
  LE.le (α := ℝ) (∫ (x : Ω), (∑ k ∈ Finset.range n, upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ)
    (∫ (x : Ω), (∑ k ∈ Finset.range n, (f (k + 1) - f k)) x ∂μ)
h₂ :
  ∫ (x : Ω), (∑ k ∈ Finset.range n, (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) x ∂μ =
    HSub.hSub (α := ℝ) (∫ (x : Ω), (∑ k ∈ Finset.range n, (f (k + 1) - f k)) x ∂μ)
      (∫ (x : Ω), (∑ k ∈ Finset.range n, upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ)
⊢ ∫ (x : Ω), (∑ k ∈ Finset.range n, upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ ≤
    HSub.hSub (α := ℝ) (∫ (x : Ω), f n x ∂μ) (∫ (x : Ω), f 0 x ∂μ)
have refine : ∫ (x : Ω), (∑ k ∈ Finset.range n, (f (k + 1) - f k)) x ∂μ ≤
  HSub.hSub (α := ℝ) (∫ (x : Ω), f n x ∂μ) (∫ (x : Ω), f 0 x ∂μ)
Tactic: refine le_trans h₁ ?_