awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Martingale.BorelCantelli (goal)
Goal:
Ω : Type u_2
s : ℕ → Set Ω
ω : Ω
n : ℕ
x : Ω
h : x ∈ s (n + 1)
⊢ norm (E := ℝ) (1 x) ≤ 1
have rw : norm (E := ℝ) 1 ≤ 1
Tactic: rw [Pi.one_apply, norm_one]
-- Lean 4 proof step from Mathlib.Probability.Martingale.BorelCantelli (goal)
Goal:
Ω : Type u_2
s : ℕ → Set Ω
ω : Ω
n : ℕ
x : Ω
h : x ∈ s (n + 1)
rw : norm (E := ℝ) 1 ≤ 1
⊢ norm (E := ℝ) (1 x) ≤ 1
have rw₁ : LE.le (α := ℝ) 1 1
Tactic: rw [Pi.one_apply, norm_one]
-- Lean 4 proof step from Mathlib.Probability.Martingale.BorelCantelli (hypothesis)
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 : ℕ) ↦ f n ω) atTop atTop ↔
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ predictablePart f ℱ μ n ω) atTop atTop
have h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atTop
Tactic: have h₁ := (martingale_martingalePart hf hint).ae_not_tendsto_atTop_atTop
    (martingalePart_bdd_difference ℱ hbdd)
-- Lean 4 proof step from Mathlib.Probability.Martingale.BorelCantelli (hypothesis)
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 : ℕ) ↦ f n ω) atTop atTop ↔
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ predictablePart f ℱ μ n ω) atTop atTop
have h₂ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atBot
Tactic: have h₂ := (martingale_martingalePart hf hint).ae_not_tendsto_atTop_atBot
    (martingalePart_bdd_difference ℱ hbdd)
-- Lean 4 proof step from Mathlib.Probability.Martingale.BorelCantelli (goal)
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] ω
have refine : ∀ (n : ℕ), 0 ≤ᶠ[ae μ] f (n + 1) - f n
Tactic: refine ae_all_iff.2 fun n => condExp_nonneg ?_
-- Lean 4 proof step from Mathlib.Probability.Martingale.BorelCantelli (goal)
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 ≤ᶠ[ae μ] f (n + 1) - f n
have 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
Tactic: filter_upwards [ae_all_iff.1 hfmono n] with ω hω using sub_nonneg.2 hω
-- Lean 4 proof step from Mathlib.Probability.Martingale.BorelCantelli (goal)
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
⊢ 0 ≤ᶠ[ae μ] f (n + 1) - f n
have h₃ : ∀ (a : Ω), f n a ≤ f (n + 1) a → 0 a ≤ (f (n + 1) - f n) a
Tactic: filter_upwards [ae_all_iff.1 hfmono n] with ω hω using sub_nonneg.2 hω
-- Lean 4 proof step from Mathlib.Probability.Martingale.BorelCantelli (hypothesis)
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
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ f n ω) atTop atTop ↔
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ predictablePart f ℱ μ n ω) atTop atTop
have h₃ : ∀ᵐ (ω : Ω) ∂μ, ∀ (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ω
-- Lean 4 proof step from Mathlib.Probability.Martingale.BorelCantelli (goal)
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] ω
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ f n ω) atTop atTop ↔
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ predictablePart f ℱ μ n ω) atTop atTop
have 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
Tactic: filter_upwards [h₁, h₂, h₃, hfmono] with ω hω₁ hω₂ hω₃ hω₄
-- Lean 4 proof step from Mathlib.Probability.Martingale.BorelCantelli (goal)
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) ω
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ f n ω) atTop atTop ↔
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ predictablePart f ℱ μ n ω) atTop atTop
have h : Tendsto (β := ℝ) (fun (n : ℕ) ↦ f n ω) atTop atTop →
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ predictablePart f ℱ μ n ω) atTop atTop
Tactic: constructor
-- Lean 4 proof step from Mathlib.Probability.Martingale.BorelCantelli (goal)
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
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ f n ω) atTop atTop ↔
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ predictablePart f ℱ μ n ω) atTop atTop
have h₄ : Tendsto (β := ℝ) (fun (n : ℕ) ↦ predictablePart f ℱ μ n ω) atTop atTop →
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ f n ω) atTop atTop
Tactic: constructor
-- Lean 4 proof step from Mathlib.Probability.Martingale.BorelCantelli (goal)
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
have h : Monotone (β := ℝ) fun (n : ℕ) ↦ predictablePart f ℱ μ n ω
Tactic: refine tendsto_atTop_atTop_of_monotone' ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Martingale.BorelCantelli (goal)
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 ω
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ predictablePart f ℱ μ n ω) atTop atTop
have h₄ : ¬BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ predictablePart f ℱ μ n ω)
Tactic: refine tendsto_atTop_atTop_of_monotone' ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Martingale.BorelCantelli (goal)
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 (α := ℝ) ((fun (n : ℕ) ↦ predictablePart f ℱ μ n ω) n) ((fun (n : ℕ) ↦ predictablePart f ℱ μ n ω) m)
have 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] ω)
Tactic: simp only [predictablePart, Finset.sum_apply]
-- Lean 4 proof step from Mathlib.Probability.Martingale.BorelCantelli (goal)
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
⊢ False
have h : ∀ (ht : Tendsto (β := ℝ) (fun (x : ℕ) ↦ -f x ω) atTop atBot) (b : ℝ)
  (hbdd : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ predictablePart f ℱ μ n ω)) b), False
Tactic: rw [← tendsto_neg_atBot_iff] at ht
Cleared hypotheses: ht, b, hbdd
-- Lean 4 proof step from Mathlib.Probability.Martingale.BorelCantelli (hypothesis)
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
⊢ False
have hω₅ : ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ (f n + -predictablePart f ℱ μ n) ω) atTop atTop
Tactic: simp only [martingalePart, sub_eq_add_neg] at hω₁
Cleared hypotheses: hω₁
-- Lean 4 proof step from Mathlib.Probability.Martingale.BorelCantelli (goal)
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 : ℕ) ↦ predictablePart f ℱ μ n ω) atTop atTop
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ f n ω) atTop atTop
have h : ¬BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω)
Tactic: refine tendsto_atTop_atTop_of_monotone' (monotone_nat_of_le_succ hω₄) ?_
-- Lean 4 proof step from Mathlib.Probability.Martingale.BorelCantelli (goal)
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
s : ℕ → Set Ω
hs : ∀ (n : ℕ), MeasurableSet (s n)
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, (s (k + 1)).indicator 1 ω) atTop atTop ↔
      Tendsto (β := ℝ)
        (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, μ[(s (k + 1)).indicator 1 | (↑ℱ : ℕ → MeasurableSpace Ω) k] ω) atTop atTop
have refine_2 : ∀
  (this :
    ∀ᵐ (ω : Ω) ∂μ,
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ process s n ω) atTop atTop ↔
        Tendsto (β := ℝ) (fun (n : ℕ) ↦ predictablePart (process s) ℱ μ n ω) atTop atTop),
  ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, (s (k + 1)).indicator 1 ω) atTop atTop ↔
      Tendsto (β := ℝ)
        (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, μ[(s (k + 1)).indicator 1 | (↑ℱ : ℕ → MeasurableSpace Ω) k] ω) atTop atTop
Tactic: have := tendsto_sum_indicator_atTop_iff (Eventually.of_forall fun ω n => ?_)
    (stronglyAdapted_process hs) (integrable_process μ hs)
    (Eventually.of_forall <| process_difference_le s)
-- Lean 4 proof step from Mathlib.Probability.Martingale.BorelCantelli (goal)
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
s : ℕ → Set Ω
hs : ∀ (n : ℕ), MeasurableSet (s n)
refine_2 :
  ∀
    (this :
      ∀ᵐ (ω : Ω) ∂μ,
        Tendsto (β := ℝ) (fun (n : ℕ) ↦ process s n ω) atTop atTop ↔
          Tendsto (β := ℝ) (fun (n : ℕ) ↦ predictablePart (process s) ℱ μ n ω) atTop atTop),
    ∀ᵐ (ω : Ω) ∂μ,
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, (s (k + 1)).indicator 1 ω) atTop atTop ↔
        Tendsto (β := ℝ)
          (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, μ[(s (k + 1)).indicator 1 | (↑ℱ : ℕ → MeasurableSpace Ω) k] ω) atTop
          atTop
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, (s (k + 1)).indicator 1 ω) atTop atTop ↔
      Tendsto (β := ℝ)
        (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, μ[(s (k + 1)).indicator 1 | (↑ℱ : ℕ → MeasurableSpace Ω) k] ω) atTop atTop
have refine_1 : ∀ (ω : Ω) (n : ℕ), process s n ω ≤ process s (n + 1) ω
Tactic: have := tendsto_sum_indicator_atTop_iff (Eventually.of_forall fun ω n => ?_)
    (stronglyAdapted_process hs) (integrable_process μ hs)
    (Eventually.of_forall <| process_difference_le s)
-- Lean 4 proof step from Mathlib.Probability.Martingale.BorelCantelli (goal)
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
s : ℕ → Set Ω
hs : ∀ (n : ℕ), MeasurableSet (s n)
ω : Ω
n : ℕ
⊢ process s n ω ≤ process s (n + 1) ω
have refine_1 : LE.le (α := ℝ) 0 ((s (n + 1)).indicator 1 ω)
Tactic: rw [process, process, ← sub_nonneg, Finset.sum_apply, Finset.sum_apply,
      Finset.sum_range_succ_sub_sum]
-- Lean 4 proof step from Mathlib.Probability.Martingale.BorelCantelli (hypothesis)
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
s : ℕ → Set Ω
hs : ∀ (n : ℕ), MeasurableSet (s n)
this :
  ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ process s n ω) atTop atTop ↔
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ predictablePart (process s) ℱ μ n ω) atTop atTop
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, (s (k + 1)).indicator 1 ω) atTop atTop ↔
      Tendsto (β := ℝ)
        (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, μ[(s (k + 1)).indicator 1 | (↑ℱ : ℕ → MeasurableSpace Ω) k] ω) atTop atTop
have this₁ : ∀ᵐ (ω : Ω) ∂μ,
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ (∑ k ∈ Finset.range n, (s (k + 1)).indicator 1) ω) atTop atTop ↔
    Tendsto (β := ℝ)
      (fun (n : ℕ) ↦ (∑ k ∈ Finset.range n, μ[(s (k + 1)).indicator 1 | (↑ℱ : ℕ → MeasurableSpace Ω) k]) ω) atTop atTop
Tactic: simp_rw [process, predictablePart_process_ae_eq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Probability.Martingale.BorelCantelli (goal)
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
ℱ : Filtration ℕ m0
μ : Measure Ω
inst : IsFiniteMeasure μ
s : ℕ → Set Ω
hs : ∀ (n : ℕ), MeasurableSet (s n)
⊢ ∀ᵐ (ω : Ω) ∂μ,
    ω ∈ limsup s atTop ↔
      Tendsto (β := ℝ)
        (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, μ[(s (k + 1)).indicator 1 | (↑ℱ : ℕ → MeasurableSpace Ω) k] ω) atTop atTop
have rw : ∀ᵐ (ω : Ω) ∂μ,
  Membership.mem (γ := Set Ω)
      {ω : Ω |
        Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, (s (k + 1)).indicator (fun (x : Ω) ↦ 1) ω) atTop atTop}
      ω ↔
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, μ[(s (k + 1)).indicator 1 | (↑ℱ : ℕ → MeasurableSpace Ω) k] ω)
      atTop atTop
Tactic: rw [← limsup_nat_add s 1,
    Set.limsup_eq_tendsto_sum_indicator_atTop (zero_lt_one (α := ℝ)) (fun n ↦ s (n + 1))]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Centering (goal)
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
⊢ predictablePart f ℱ μ 0 = 0
have simp_rw : Eq (α := Ω → E) (∑ i ∈ Finset.range 0, μ[f (i + 1) - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i]) 0
Tactic: simp_rw [predictablePart, Finset.range_zero, Finset.sum_empty]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Centering (goal)
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
simp_rw : Eq (α := Ω → E) (∑ i ∈ Finset.range 0, μ[f (i + 1) - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i]) 0
⊢ predictablePart f ℱ μ 0 = 0
have simp_rw₁ : Eq (α := Ω → E) (∑ i ∈ ∅, μ[f (i + 1) - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i]) 0
Tactic: simp_rw [predictablePart, Finset.range_zero, Finset.sum_empty]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Centering (goal)
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst_2 : CompleteSpace E
c : ℝ
n : ℕ
⊢ predictablePart (c • f) ℱ μ n =ᶠ[ae μ] c • predictablePart f ℱ μ n
have simp : EventuallyEq.{u_1, u_2} (β := E) (ae μ)
  (∑ i ∈ Finset.range n, μ[(c • f) (i + 1) - (c • f) i | (↑ℱ : ℕ → MeasurableSpace Ω) i])
  (∑ x ∈ Finset.range n, c • μ[f (x + 1) - f x | (↑ℱ : ℕ → MeasurableSpace Ω) x])
Tactic: simp only [predictablePart, Finset.smul_sum]