awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Martingale.Upcrossing
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
⊢ upperCrossingTime a b f N j.succ ω ≤ lowerCrossingTime a b f N i ω

Tactic:
le_trans upperCrossingTime_le_lowerCrossingTime
      (lowerCrossingTime_mono (Nat.succ_le_of_lt hij'))

Premises used: Nat.succ_le_of_lt, MeasureTheory.upperCrossingTime_le_lowerCrossingTime, MeasureTheory.lowerCrossingTime_mono, le_trans
-- Module: Mathlib.Probability.Martingale.Upcrossing
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
⊢ upperCrossingTime a b f N j.succ ω ≤ lowerCrossingTime a b f N i ω

Tactic:
refine le_trans upperCrossingTime_le_lowerCrossingTime
      (lowerCrossingTime_mono (Nat.succ_le_of_lt hij'))

Premises used: Nat.succ_le_of_lt, MeasureTheory.upperCrossingTime_le_lowerCrossingTime, MeasureTheory.lowerCrossingTime_mono, le_trans
-- Module: Mathlib.Probability.Martingale.Upcrossing
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

Tactic:
Finset.stronglyMeasurable_fun_sum _ fun i _ =>
    stronglyMeasurable_const.indicator ?_

Premises used: MeasureTheory.stronglyMeasurable_const, Finset.stronglyMeasurable_fun_sum, MeasureTheory.StronglyMeasurable.indicator
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
n : ℕ
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
⊢ 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

Tactic:
refine Finset.stronglyMeasurable_fun_sum _ fun i _ =>
    stronglyMeasurable_const.indicator ?_

Premises used: MeasureTheory.stronglyMeasurable_const, Finset.stronglyMeasurable_fun_sum, MeasureTheory.StronglyMeasurable.indicator
-- Module: Mathlib.Probability.Martingale.Upcrossing
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 (ω : Ω) ↦ ((↑(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
-- Module: Mathlib.Probability.Martingale.Upcrossing
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 (ω : Ω) ↦ ((↑(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
-- Module: Mathlib.Probability.Martingale.Upcrossing
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} (α := Ω) {ω : Ω | lowerCrossingTime a b f N i ω ≤ n}

Tactic:
simp only [ENat.some_eq_coe, Nat.cast_le] at hl hu

Premises used: ENat.some_eq_coe, Nat.cast_le
-- Module: Mathlib.Probability.Martingale.Upcrossing
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} (α := Ω) {ω : Ω | upperCrossingTime a b f N (i + 1) ω ≤ n}

Tactic:
simp only [ENat.some_eq_coe, Nat.cast_le] at hl hu

Premises used: ENat.some_eq_coe, Nat.cast_le
-- Module: Mathlib.Probability.Martingale.Upcrossing
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}
simp_rw :
  MeasurableSet.{u_1} (α := Ω) fun (ω : Ω) ↦
    ({n : ℕ | lowerCrossingTime a b f N i ω ≤ n} ∩ {n : ℕ | ¬upperCrossingTime a b f N (i + 1) ω ≤ n}) n
⊢ MeasurableSet.{u_1} (α := Ω) fun (ω : Ω) ↦
    ({n : ℕ | lowerCrossingTime a b f N i ω ≤ n} ∩ {n : ℕ | n < upperCrossingTime a b f N (i + 1) ω}) n

Tactic:
simp_rw [← not_le]

Premises used: not_le
-- Module: Mathlib.Probability.Martingale.Upcrossing
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 : ℕ | ¬upperCrossingTime a b f N (i + 1) ω ≤ n}) n

Tactic:
hl.inter hu.compl

Premises used: Set.Mem, setOf, Set.inter, MeasurableSet.compl, MeasurableSet.inter
-- Module: Mathlib.Probability.Martingale.Upcrossing
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 : ℕ | ¬upperCrossingTime a b f N (i + 1) ω ≤ n}) n

Tactic:
exact hl.inter hu.compl

Premises used: MeasurableSet.compl, MeasurableSet.inter
-- Module: Mathlib.Probability.Martingale.Upcrossing
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, upcrossingStrat a b f N k * (f (k + 1) - f k)) ℱ μ

Tactic:
hf.sum_mul_sub hf.stronglyAdapted.upcrossingStrat (fun _ _ => upcrossingStrat_le_one) fun _ _ =>
    upcrossingStrat_nonneg

Premises used: MeasureTheory.upcrossingStrat_nonneg, MeasureTheory.upcrossingStrat_le_one, MeasureTheory.Submartingale.sum_mul_sub, MeasureTheory.StronglyAdapted.upcrossingStrat, MeasureTheory.Submartingale.stronglyAdapted
-- Module: Mathlib.Probability.Martingale.Upcrossing
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)) ℱ μ

Tactic:
hf.sum_mul_sub
    (fun n => (stronglyAdapted_const ℱ 1 n).sub (hf.stronglyAdapted.upcrossingStrat n))
    (?_ : ∀ n ω, (1 - upcrossingStrat a b f N n) ω ≤ 1) ?_

Premises used: MeasureTheory.stronglyAdapted_const, MeasureTheory.StronglyMeasurable.sub, MeasureTheory.Submartingale.sum_mul_sub, MeasureTheory.StronglyAdapted.upcrossingStrat, MeasureTheory.Submartingale.stronglyAdapted, OfNat.ofNat
-- Module: Mathlib.Probability.Martingale.Upcrossing
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
refine_2 : ∀ (n : ℕ) (ω : Ω), 0 ≤ HSub.hSub (α := (ω : Ω) → ℝ) 1 (upcrossingStrat a b f N n) ω
⊢ Submartingale (E := ℝ) (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) ℱ μ

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) ?_

Premises used: MeasureTheory.stronglyAdapted_const, MeasureTheory.StronglyMeasurable.sub, MeasureTheory.Submartingale.sum_mul_sub, MeasureTheory.StronglyAdapted.upcrossingStrat, MeasureTheory.Submartingale.stronglyAdapted, OfNat.ofNat
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
a b : ℝ
N : ℕ
⊢ ∀ (n : ℕ) (ω : Ω), HSub.hSub (α := (ω : Ω) → ℝ) 1 (upcrossingStrat a b f N n) ω ≤ 1

Tactic:
fun n ω => sub_le_self _ upcrossingStrat_nonneg

Premises used: MeasureTheory.upcrossingStrat_nonneg, sub_le_self, OfNat.ofNat
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
a b : ℝ
N : ℕ
⊢ ∀ (n : ℕ) (ω : Ω), HSub.hSub (α := (ω : Ω) → ℝ) 1 (upcrossingStrat a b f N n) ω ≤ 1

Tactic:
exact fun n ω => sub_le_self _ upcrossingStrat_nonneg

Premises used: MeasureTheory.upcrossingStrat_nonneg, sub_le_self
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
a b : ℝ
N n : ℕ
ω : Ω
⊢ 0 ≤ HSub.hSub (α := (ω : Ω) → ℝ) 1 (upcrossingStrat a b f N n) ω

Tactic:
simp [upcrossingStrat_le_one]

Premises used: MeasureTheory.upcrossingStrat_le_one
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
⊢ 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
-- Module: Mathlib.Probability.Martingale.Upcrossing
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 (α := ℝ) (∫ (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

Premises used: MeasureTheory.setIntegral_univ
-- Module: Mathlib.Probability.Martingale.Upcrossing
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 ∂μ)

Tactic:
le_trans ?_ this

Premises used: le_trans
-- Module: Mathlib.Probability.Martingale.Upcrossing
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 ∂μ)
refine : LE.le (α := ℝ) 0 (∫ (x : Ω), (∑ k ∈ Finset.range 0, (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 ∂μ)

Tactic:
refine le_trans ?_ this

Premises used: le_trans
-- Module: Mathlib.Probability.Martingale.Upcrossing
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 0, (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) x ∂μ)

Tactic:
simp only [Finset.range_zero, Finset.sum_empty, integral_zero', le_refl]

Premises used: le_refl, MeasureTheory.integral_zero', Finset.sum_empty, Finset.range_zero
-- Module: Mathlib.Probability.Martingale.Upcrossing
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 ∂μ)

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]
-- Module: Mathlib.Probability.Martingale.Upcrossing
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 ∂μ)
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) ∂μ)
⊢ ∫ (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:
simp only [sub_mul, one_mul, Finset.sum_sub_distrib, Pi.sub_apply, Finset.sum_apply,
      Pi.mul_apply]

Premises used: Pi.mul_apply, Finset.sum_apply, sub_mul, Finset.sum_sub_distrib, one_mul, Pi.sub_apply
-- Module: Mathlib.Probability.Martingale.Upcrossing
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) ∂μ)

Tactic:
integral_sub (Integrable.sub (integrable_finsetSum _ fun i _ => hf.integrable _)
      (integrable_finsetSum _ fun i _ => hf.integrable _)) ?_

Premises used: MeasureTheory.Submartingale.integrable, MeasureTheory.Integrable.sub, MeasureTheory.integral_sub, MeasureTheory.integrable_finsetSum, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Probability.Martingale.Upcrossing
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 ∂μ)
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))
    μ
⊢ ∫ (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:
refine integral_sub (Integrable.sub (integrable_finsetSum _ fun i _ => hf.integrable _)
      (integrable_finsetSum _ fun i _ => hf.integrable _)) ?_

Premises used: MeasureTheory.Submartingale.integrable, MeasureTheory.Integrable.sub, MeasureTheory.integral_sub, MeasureTheory.integrable_finsetSum
-- Module: Mathlib.Probability.Martingale.Upcrossing
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 (ε := ℝ) (∑ k ∈ Finset.range n, upcrossingStrat a b f N k * (f (k + 1) - f k)) μ

Tactic:
(hf.sum_upcrossingStrat_mul a b N).integrable n

Premises used: MeasureTheory.Submartingale.sum_upcrossingStrat_mul, MeasureTheory.Submartingale.integrable
-- Module: Mathlib.Probability.Martingale.Upcrossing
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 :
  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))
⊢ 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:
convert! (hf.sum_upcrossingStrat_mul a b N).integrable n using 1

Premises used: MeasureTheory.Submartingale.sum_upcrossingStrat_mul, MeasureTheory.Submartingale.integrable
-- Module: Mathlib.Probability.Martingale.Upcrossing
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 : Ω),
    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)
⊢ 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:
ext
-- Module: Mathlib.Probability.Martingale.Upcrossing
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 : Ω
⊢ 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:
simp
-- Module: Mathlib.Probability.Martingale.Upcrossing
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 ∂μ)

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
-- Module: Mathlib.Probability.Martingale.Upcrossing
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 ∂μ)
⊢ 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₁

Premises used: sub_nonneg
-- Module: Mathlib.Probability.Martingale.Upcrossing
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 ∂μ)
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 ∂μ)
⊢ ∫ (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:
rw [h₂, sub_nonneg] at h₁

Premises used: sub_nonneg