awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
ℱ : Filtration ℕ m0
μ : Measure Ω
s : ℕ → Set Ω
n : ℕ
⊢ Eq.{u_2 + 1} (α := Ω → ℝ)
    (∑ i ∈ Finset.range n,
      (process s (i + 1) - process s i - μ[process s (i + 1) - process s i | (↑ℱ : ℕ → MeasurableSpace Ω) i]))
    (∑ k ∈ Finset.range n,
      HSub.hSub (α := (x : Ω) → ℝ) ((s (k + 1)).indicator 1)
        μ[(s (k + 1)).indicator 1 | (↑ℱ : ℕ → MeasurableSpace Ω) k])

Tactic:
Finset.sum_congr rfl fun k _ => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
ℱ : Filtration ℕ m0
μ : Measure Ω
s : ℕ → Set Ω
n : ℕ
refine :
  ∀ k ∈ Finset.range n,
    process s (k + 1) - process s k - μ[process s (k + 1) - process s k | (↑ℱ : ℕ → MeasurableSpace Ω) k] =
      HSub.hSub (α := (x : Ω) → ℝ) ((s (k + 1)).indicator 1) μ[(s (k + 1)).indicator 1 | (↑ℱ : ℕ → MeasurableSpace Ω) k]
⊢ Eq.{u_2 + 1} (α := Ω → ℝ)
    (∑ i ∈ Finset.range n,
      (process s (i + 1) - process s i - μ[process s (i + 1) - process s i | (↑ℱ : ℕ → MeasurableSpace Ω) i]))
    (∑ k ∈ Finset.range n,
      HSub.hSub (α := (x : Ω) → ℝ) ((s (k + 1)).indicator 1)
        μ[(s (k + 1)).indicator 1 | (↑ℱ : ℕ → MeasurableSpace Ω) k])

Tactic:
refine Finset.sum_congr rfl fun k _ => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
ℱ : Filtration ℕ m0
μ : Measure Ω
s : ℕ → Set Ω
n k : ℕ
h : k ∈ Finset.range n
⊢ process s (k + 1) - process s k - μ[process s (k + 1) - process s k | (↑ℱ : ℕ → MeasurableSpace Ω) k] =
    HSub.hSub (α := (x : Ω) → ℝ) ((s (k + 1)).indicator 1) μ[(s (k + 1)).indicator 1 | (↑ℱ : ℕ → MeasurableSpace Ω) k]

Tactic:
simp only [process, Finset.sum_range_succ_sub_sum]

Premises used: Finset.sum_range_succ_sub_sum, MeasureTheory.BorelCantelli.process
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
ℱ : Filtration ℕ m0
μ : Measure Ω
s : ℕ → Set Ω
n : ℕ
⊢ martingalePart (process s) ℱ μ n =
    ∑ k ∈ Finset.range n,
      HSub.hSub (α := (x : Ω) → ℝ) ((s (k + 1)).indicator 1) μ[(s (k + 1)).indicator 1 | (↑ℱ : ℕ → MeasurableSpace Ω) k]

Tactic:
have := martingalePart_process_ae_eq ℱ μ s n
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
ℱ : Filtration ℕ m0
μ : Measure Ω
s : ℕ → Set Ω
n : ℕ
this :
  martingalePart (process s) ℱ μ n =
    ∑ k ∈ Finset.range n,
      HSub.hSub (α := (x : Ω) → ℝ) ((s (k + 1)).indicator 1) μ[(s (k + 1)).indicator 1 | (↑ℱ : ℕ → MeasurableSpace Ω) k]
⊢ ∑ k ∈ Finset.range n, (s (k + 1)).indicator 1 - predictablePart (process s) ℱ μ n =
    HSub.hSub (α := Ω → ℝ) (∑ k ∈ Finset.range n, (s (k + 1)).indicator 1)
      (∑ x ∈ Finset.range n, μ[(s (x + 1)).indicator 1 | (↑ℱ : ℕ → MeasurableSpace Ω) x])

Tactic:
simp_rw [martingalePart, process, Finset.sum_sub_distrib] at this

Premises used: MeasureTheory.martingalePart, Finset.sum_sub_distrib, MeasureTheory.BorelCantelli.process
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
ℱ : Filtration ℕ m0
μ : Measure Ω
s : ℕ → Set Ω
n : ℕ
this :
  ∑ k ∈ Finset.range n, (s (k + 1)).indicator 1 - predictablePart (process s) ℱ μ n =
    HSub.hSub (α := Ω → ℝ) (∑ k ∈ Finset.range n, (s (k + 1)).indicator 1)
      (∑ x ∈ Finset.range n, μ[(s (x + 1)).indicator 1 | (↑ℱ : ℕ → MeasurableSpace Ω) x])
⊢ predictablePart (process s) ℱ μ n = ∑ k ∈ Finset.range n, μ[(s (k + 1)).indicator 1 | (↑ℱ : ℕ → MeasurableSpace Ω) k]

Tactic:
sub_right_injective this

Premises used: sub_right_injective
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
ℱ : Filtration ℕ m0
μ : Measure Ω
s : ℕ → Set Ω
n : ℕ
this :
  ∑ k ∈ Finset.range n, (s (k + 1)).indicator 1 - predictablePart (process s) ℱ μ n =
    HSub.hSub (α := Ω → ℝ) (∑ k ∈ Finset.range n, (s (k + 1)).indicator 1)
      (∑ x ∈ Finset.range n, μ[(s (x + 1)).indicator 1 | (↑ℱ : ℕ → MeasurableSpace Ω) x])
⊢ predictablePart (process s) ℱ μ n = ∑ k ∈ Finset.range n, μ[(s (k + 1)).indicator 1 | (↑ℱ : ℕ → MeasurableSpace Ω) k]

Tactic:
exact sub_right_injective this

Premises used: sub_right_injective
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
s : ℕ → Set Ω
ω : Ω
n : ℕ
rw : LE.le (α := ℝ) ((s (n + 1)).indicator (fun (a : Ω) ↦ norm (E := ℝ) (1 a)) ω) 1
⊢ |process s (n + 1) ω - process s n ω| ≤ 1

Tactic:
rw [process, process, Finset.sum_apply, Finset.sum_apply,
    Finset.sum_range_succ_sub_sum, ← Real.norm_eq_abs, norm_indicator_eq_indicator_norm]

Premises used: norm_indicator_eq_indicator_norm, Finset.sum_apply, Finset.sum_range_succ_sub_sum, MeasureTheory.BorelCantelli.process, Real.norm_eq_abs
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
s : ℕ → Set Ω
ω : Ω
n : ℕ
⊢ LE.le (α := ℝ) ((s (n + 1)).indicator (fun (a : Ω) ↦ norm (E := ℝ) (1 a)) ω) 1

Tactic:
Set.indicator_le' (fun _ _ => ?_) (fun _ _ => zero_le_one) _

Premises used: zero_le_one, Set.indicator_le'
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
s : ℕ → Set Ω
ω : Ω
n : ℕ
refine : ∀ x ∈ s (n + 1), norm (E := ℝ) (1 x) ≤ 1
⊢ LE.le (α := ℝ) ((s (n + 1)).indicator (fun (a : Ω) ↦ norm (E := ℝ) (1 a)) ω) 1

Tactic:
refine Set.indicator_le' (fun _ _ => ?_) (fun _ _ => zero_le_one) _

Premises used: zero_le_one, Set.indicator_le'
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
s : ℕ → Set Ω
ω : Ω
n : ℕ
x : Ω
h : x ∈ s (n + 1)
rw : norm (E := ℝ) 1 ≤ 1
rw₁ rw₂ : LE.le (α := ℝ) 1 1
⊢ norm (E := ℝ) (1 x) ≤ 1

Tactic:
rw [Pi.one_apply, norm_one]

Premises used: Pi.one_apply, NormOneClass.norm_one
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
ℱ : Filtration ℕ m0
s : ℕ → Set Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
hs : ∀ (n : ℕ), MeasurableSet (s n)
n : ℕ
⊢ Integrable (process s n) μ

Tactic:
integrable_finsetSum' _ fun _ _ =>
    IntegrableOn.integrable_indicator (integrable_const 1) <| ℱ.le _ _ <| hs _

Premises used: MeasureTheory.IntegrableOn.integrable_indicator, MeasureTheory.integrable_finsetSum', HAdd.hAdd, MeasureTheory.Filtration.le, OfNat.ofNat, MeasureTheory.BorelCantelli.process, MeasureTheory.integrable_const
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
hint : ∀ (n : ℕ), Integrable (f n) μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), |f (n + 1) ω - f n ω| ≤ (↑R : ℝ)
⊢ ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atTop

Tactic:
have h₁ := (martingale_martingalePart hf hint).ae_not_tendsto_atTop_atTop
    (martingalePart_bdd_difference ℱ hbdd)
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
hint : ∀ (n : ℕ), Integrable (f n) μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), |f (n + 1) ω - f n ω| ≤ (↑R : ℝ)
h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atTop
⊢ ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atBot

Tactic:
have h₂ := (martingale_martingalePart hf hint).ae_not_tendsto_atTop_atBot
    (martingalePart_bdd_difference ℱ hbdd)
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
hint : ∀ (n : ℕ), Integrable (f n) μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), |f (n + 1) ω - f n ω| ≤ (↑R : ℝ)
h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atTop
h₂ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atBot
⊢ ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), 0 ≤ μ[f (n + 1) - f n | (↑ℱ : ℕ → MeasurableSpace Ω) n] ω

Tactic:
ae_all_iff.2 fun n => condExp_nonneg ?_

Premises used: Iff.mpr, MeasureTheory.condExp_nonneg, MeasureTheory.ae_all_iff
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
hint : ∀ (n : ℕ), Integrable (f n) μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), |f (n + 1) ω - f n ω| ≤ (↑R : ℝ)
h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atTop
h₂ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atBot
refine : ∀ (n : ℕ), 0 ≤ᶠ[ae μ] f (n + 1) - f n
⊢ ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), 0 ≤ μ[f (n + 1) - f n | (↑ℱ : ℕ → MeasurableSpace Ω) n] ω

Tactic:
refine ae_all_iff.2 fun n => condExp_nonneg ?_

Premises used: Iff.mpr, MeasureTheory.condExp_nonneg, MeasureTheory.ae_all_iff
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
hint : ∀ (n : ℕ), Integrable (f n) μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), |f (n + 1) ω - f n ω| ≤ (↑R : ℝ)
h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atTop
h₂ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atBot
n : ℕ
ω : Ω
hω : f n ω ≤ f (n + 1) ω
⊢ 0 ω ≤ (f (n + 1) - f n) ω

Tactic:
sub_nonneg.2 hω

Premises used: Iff.mpr, sub_nonneg
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
hint : ∀ (n : ℕ), Integrable (f n) μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), |f (n + 1) ω - f n ω| ≤ (↑R : ℝ)
h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atTop
h₂ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atBot
n : ℕ
h :
  ∀ (a : Ω),
    Membership.mem (γ := Set Ω)
      {x : Ω |
        Membership.mem (γ := Set Ω) {x : Ω | (fun (a : Ω) ↦ f n a ≤ f (n + 1) a) x} x →
          Membership.mem (γ := Set Ω) {x : Ω | (fun (x : Ω) ↦ 0 x ≤ (f (n + 1) - f n) x) x} x}
      a
h₃ h₄ : ∀ (ω : Ω) (hω : f n ω ≤ f (n + 1) ω), 0 ω ≤ (f (n + 1) - f n) ω
⊢ 0 ≤ᶠ[ae μ] f (n + 1) - f n

Tactic:
filter_upwards [ae_all_iff.1 hfmono n] with ω hω using sub_nonneg.2 hω

Premises used: Iff.mp, MeasureTheory.ae_all_iff
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
hint : ∀ (n : ℕ), Integrable (f n) μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), |f (n + 1) ω - f n ω| ≤ (↑R : ℝ)
h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atTop
h₂ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atBot
⊢ ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), 0 ≤ μ[f (n + 1) - f n | (↑ℱ : ℕ → MeasurableSpace Ω) n] ω

Tactic:
have h₃ : ∀ᵐ ω ∂μ, ∀ n, 0 ≤ (μ[f (n + 1) - f n | ℱ n]) ω := by
    refine ae_all_iff.2 fun n => condExp_nonneg ?_
    filter_upwards [ae_all_iff.1 hfmono n] with ω hω using sub_nonneg.2 hω
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
hint : ∀ (n : ℕ), Integrable (f n) μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), |f (n + 1) ω - f n ω| ≤ (↑R : ℝ)
h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atTop
h₂ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atBot
h₃ : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), 0 ≤ μ[f (n + 1) - f n | (↑ℱ : ℕ → MeasurableSpace Ω) n] ω
h :
  ∀ (ω : Ω) (hω₁ : ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atTop)
    (hω₂ : ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atBot)
    (hω₃ : ∀ (n : ℕ), 0 ≤ μ[f (n + 1) - f n | (↑ℱ : ℕ → MeasurableSpace Ω) n] ω) (hω₄ : ∀ (n : ℕ), f n ω ≤ f (n + 1) ω),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ f n ω) atTop atTop ↔
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ predictablePart f ℱ μ n ω) atTop atTop
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ f n ω) atTop atTop ↔
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ predictablePart f ℱ μ n ω) atTop atTop

Tactic:
filter_upwards [h₁, h₂, h₃, hfmono] with ω hω₁ hω₂ hω₃ hω₄
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
hint : ∀ (n : ℕ), Integrable (f n) μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), |f (n + 1) ω - f n ω| ≤ (↑R : ℝ)
h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atTop
h₂ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atBot
h₃ : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), 0 ≤ μ[f (n + 1) - f n | (↑ℱ : ℕ → MeasurableSpace Ω) n] ω
ω : Ω
hω₁ : ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atTop
hω₂ : ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atBot
hω₃ : ∀ (n : ℕ), 0 ≤ μ[f (n + 1) - f n | (↑ℱ : ℕ → MeasurableSpace Ω) n] ω
hω₄ : ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
h :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ f n ω) atTop atTop →
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ predictablePart f ℱ μ n ω) atTop atTop
h₄ :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ predictablePart f ℱ μ n ω) atTop atTop →
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ f n ω) atTop atTop
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ f n ω) atTop atTop ↔
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ predictablePart f ℱ μ n ω) atTop atTop

Tactic:
constructor
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
hint : ∀ (n : ℕ), Integrable (f n) μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), |f (n + 1) ω - f n ω| ≤ (↑R : ℝ)
h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atTop
h₂ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atBot
h₃ : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), 0 ≤ μ[f (n + 1) - f n | (↑ℱ : ℕ → MeasurableSpace Ω) n] ω
ω : Ω
hω₁ : ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atTop
hω₂ : ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atBot
hω₃ : ∀ (n : ℕ), 0 ≤ μ[f (n + 1) - f n | (↑ℱ : ℕ → MeasurableSpace Ω) n] ω
hω₄ : ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
ht : Tendsto (β := ℝ) (fun (n : ℕ) ↦ f n ω) atTop atTop
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ predictablePart f ℱ μ n ω) atTop atTop

Tactic:
tendsto_atTop_atTop_of_monotone' ?_ ?_

Premises used: Filter.tendsto_atTop_atTop_of_monotone'
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
hint : ∀ (n : ℕ), Integrable (f n) μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), |f (n + 1) ω - f n ω| ≤ (↑R : ℝ)
h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atTop
h₂ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atBot
h₃ : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), 0 ≤ μ[f (n + 1) - f n | (↑ℱ : ℕ → MeasurableSpace Ω) n] ω
ω : Ω
hω₁ : ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atTop
hω₂ : ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atBot
hω₃ : ∀ (n : ℕ), 0 ≤ μ[f (n + 1) - f n | (↑ℱ : ℕ → MeasurableSpace Ω) n] ω
hω₄ : ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
ht : Tendsto (β := ℝ) (fun (n : ℕ) ↦ f n ω) atTop atTop
h : Monotone (β := ℝ) fun (n : ℕ) ↦ predictablePart f ℱ μ n ω
h₄ : ¬BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ predictablePart f ℱ μ n ω)
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ predictablePart f ℱ μ n ω) atTop atTop

Tactic:
refine tendsto_atTop_atTop_of_monotone' ?_ ?_

Premises used: Filter.tendsto_atTop_atTop_of_monotone'
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
hint : ∀ (n : ℕ), Integrable (f n) μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), |f (n + 1) ω - f n ω| ≤ (↑R : ℝ)
h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atTop
h₂ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atBot
h₃ : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), 0 ≤ μ[f (n + 1) - f n | (↑ℱ : ℕ → MeasurableSpace Ω) n] ω
ω : Ω
hω₁ : ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atTop
hω₂ : ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atBot
hω₃ : ∀ (n : ℕ), 0 ≤ μ[f (n + 1) - f n | (↑ℱ : ℕ → MeasurableSpace Ω) n] ω
hω₄ : ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
ht : Tendsto (β := ℝ) (fun (n : ℕ) ↦ f n ω) atTop atTop
n m : ℕ
hnm : n ≤ m
h :
  LE.le (α := ℝ) (∑ c ∈ Finset.range n, μ[f (c + 1) - f c | (↑ℱ : ℕ → MeasurableSpace Ω) c] ω)
    (∑ c ∈ Finset.range m, μ[f (c + 1) - f c | (↑ℱ : ℕ → MeasurableSpace Ω) c] ω)
⊢ LE.le (α := ℝ) ((fun (n : ℕ) ↦ predictablePart f ℱ μ n ω) n) ((fun (n : ℕ) ↦ predictablePart f ℱ μ n ω) m)

Tactic:
simp only [predictablePart, Finset.sum_apply]

Premises used: Finset.sum_apply, MeasureTheory.predictablePart
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
hint : ∀ (n : ℕ), Integrable (f n) μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), |f (n + 1) ω - f n ω| ≤ (↑R : ℝ)
h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atTop
h₂ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atBot
h₃ : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), 0 ≤ μ[f (n + 1) - f n | (↑ℱ : ℕ → MeasurableSpace Ω) n] ω
ω : Ω
hω₁ : ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atTop
hω₂ : ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atBot
hω₃ : ∀ (n : ℕ), 0 ≤ μ[f (n + 1) - f n | (↑ℱ : ℕ → MeasurableSpace Ω) n] ω
hω₄ : ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
ht : Tendsto (β := ℝ) (fun (n : ℕ) ↦ f n ω) atTop atTop
n m : ℕ
hnm : n ≤ m
⊢ LE.le (α := ℝ) (∑ c ∈ Finset.range n, μ[f (c + 1) - f c | (↑ℱ : ℕ → MeasurableSpace Ω) c] ω)
    (∑ c ∈ Finset.range m, μ[f (c + 1) - f c | (↑ℱ : ℕ → MeasurableSpace Ω) c] ω)

Tactic:
Finset.sum_mono_set_of_nonneg hω₃ (Finset.range_mono hnm)

Premises used: Finset.range_mono, Finset.sum_mono_set_of_nonneg
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
hint : ∀ (n : ℕ), Integrable (f n) μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), |f (n + 1) ω - f n ω| ≤ (↑R : ℝ)
h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atTop
h₂ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atBot
h₃ : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), 0 ≤ μ[f (n + 1) - f n | (↑ℱ : ℕ → MeasurableSpace Ω) n] ω
ω : Ω
hω₁ : ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atTop
hω₂ : ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atBot
hω₃ : ∀ (n : ℕ), 0 ≤ μ[f (n + 1) - f n | (↑ℱ : ℕ → MeasurableSpace Ω) n] ω
hω₄ : ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
ht : Tendsto (β := ℝ) (fun (n : ℕ) ↦ f n ω) atTop atTop
n m : ℕ
hnm : n ≤ m
⊢ LE.le (α := ℝ) (∑ c ∈ Finset.range n, μ[f (c + 1) - f c | (↑ℱ : ℕ → MeasurableSpace Ω) c] ω)
    (∑ c ∈ Finset.range m, μ[f (c + 1) - f c | (↑ℱ : ℕ → MeasurableSpace Ω) c] ω)

Tactic:
exact Finset.sum_mono_set_of_nonneg hω₃ (Finset.range_mono hnm)

Premises used: Finset.range_mono, Finset.sum_mono_set_of_nonneg
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
hint : ∀ (n : ℕ), Integrable (f n) μ
hbdd_1 : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), |f (n + 1) ω - f n ω| ≤ (↑R : ℝ)
h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atTop
h₂ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atBot
h₃ : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), 0 ≤ μ[f (n + 1) - f n | (↑ℱ : ℕ → MeasurableSpace Ω) n] ω
ω : Ω
hω₁ : ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atTop
hω₂ : ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atBot
hω₃ : ∀ (n : ℕ), 0 ≤ μ[f (n + 1) - f n | (↑ℱ : ℕ → MeasurableSpace Ω) n] ω
hω₄ : ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
ht : Tendsto (β := ℝ) (fun (n : ℕ) ↦ f n ω) atTop atTop
b : ℝ
hbdd : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ predictablePart f ℱ μ n ω)) b
h :
  ∀ (ht : Tendsto (β := ℝ) (fun (x : ℕ) ↦ -f x ω) atTop atBot) (b : ℝ)
    (hbdd : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ predictablePart f ℱ μ n ω)) b), False
⊢ False

Tactic:
rw [← tendsto_neg_atBot_iff] at ht

Premises used: Filter.tendsto_neg_atBot_iff
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
hint : ∀ (n : ℕ), Integrable (f n) μ
hbdd_1 : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), |f (n + 1) ω - f n ω| ≤ (↑R : ℝ)
h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atTop
h₂ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atBot
h₃ : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), 0 ≤ μ[f (n + 1) - f n | (↑ℱ : ℕ → MeasurableSpace Ω) n] ω
ω : Ω
hω₁ : ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atTop
hω₂ : ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atBot
hω₃ : ∀ (n : ℕ), 0 ≤ μ[f (n + 1) - f n | (↑ℱ : ℕ → MeasurableSpace Ω) n] ω
hω₄ : ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
ht : Tendsto (β := ℝ) (fun (x : ℕ) ↦ -f x ω) atTop atBot
b : ℝ
hbdd : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ predictablePart f ℱ μ n ω)) b
⊢ ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ (f n + -predictablePart f ℱ μ n) ω) atTop atTop

Tactic:
simp only [martingalePart, sub_eq_add_neg] at hω₁

Premises used: MeasureTheory.martingalePart, sub_eq_add_neg