awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
inst_6 : IsOrderedAddMonoid E
inst_7 : IsFiniteMeasure μ
R : ℝ
f : ℕ → Ω → E
ξ : ℕ → Ω → ℝ
hf : Submartingale f 𝒢 μ
hξ : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) 𝒢 ξ
hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R
hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω
C : (i : ℕ) → ℝ
hC : ∀ (i : ℕ) (ω : Ω), ‖ξ i ω‖ ≤ C i
hint : ∀ (m : ℕ), Integrable.{u_2, u_1} (ε := E) (∑ k ∈ Finset.range m, ξ k • (f (k + 1) - f k)) μ
hadp : StronglyAdapted (β := fun (n : ℕ) ↦ E) 𝒢 fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, ξ k • (f (k + 1) - f k)
i : ℕ
ω : Ω
hω1 : 0 ≤ μ[f (i + 1) - f i | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω
hω2 :
  μ[ξ i • (f (i + 1) - f i) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω =
    ξ i ω • μ[f (i + 1) - f i | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω
h₁ : 0 ≤ ξ i ω
⊢ 0 ≤ μ[ξ i • (f (i + 1) - f i) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω
have h₂ : LE.le.{u_2} (α := E) 0 0
Tactic: grw [← smul_zero (0 : ℝ), hnonneg i ω, hω1, hω2]
-- Lean 4 proof step from Mathlib.Probability.Martingale.BorelCantelli (goal)
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
i : ℕ
⊢ ∀ᵐ (ω : Ω) ∂μ, stoppedAbove f r i ω ≤ r + (↑R : ℝ)
have h : ∀ (ω : Ω) (hbddω : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)), stoppedAbove f r i ω ≤ r + (↑R : ℝ)
Tactic: filter_upwards [hbdd] with ω hbddω
-- Lean 4 proof step from Mathlib.Probability.Martingale.BorelCantelli (goal)
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
i : ℕ
ω : Ω
hbddω : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
⊢ stoppedAbove f r i ω ≤ r + (↑R : ℝ)
have h : f (min (↑i : WithTop ℕ) (leastGE f r ω)).untopA ω ≤ r + (↑R : ℝ)
Tactic: rw [stoppedAbove, stoppedProcess, ENat.some_eq_coe]
-- Lean 4 proof step from Mathlib.Probability.Martingale.BorelCantelli (goal)
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
i : ℕ
ω : Ω
hbddω : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
⊢ f (min (↑i : WithTop ℕ) (leastGE f r ω)).untopA ω ≤ r + (↑R : ℝ)
have pos : ∀ (h_zero : WithTop.untopA (min (↑i : ℕ∞) (leastGE f r ω)) = 0),
  f (min (↑i : WithTop ℕ) (leastGE f r ω)).untopA ω ≤ r + (↑R : ℝ)
Tactic: by_cases h_zero : (min (i : ℕ∞) (leastGE f r ω)).untopA = 0
-- Lean 4 proof step from Mathlib.Probability.Martingale.BorelCantelli (goal)
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
i : ℕ
ω : Ω
hbddω : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
pos :
  ∀ (h_zero : WithTop.untopA (min (↑i : ℕ∞) (leastGE f r ω)) = 0),
    f (min (↑i : WithTop ℕ) (leastGE f r ω)).untopA ω ≤ r + (↑R : ℝ)
⊢ f (min (↑i : WithTop ℕ) (leastGE f r ω)).untopA ω ≤ r + (↑R : ℝ)
have neg : ∀ (h_zero : ¬WithTop.untopA (min (↑i : ℕ∞) (leastGE f r ω)) = 0),
  f (min (↑i : WithTop ℕ) (leastGE f r ω)).untopA ω ≤ r + (↑R : ℝ)
Tactic: by_cases h_zero : (min (i : ℕ∞) (leastGE f r ω)).untopA = 0
-- Lean 4 proof step from Mathlib.Probability.Martingale.BorelCantelli (goal)
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
i : ℕ
ω : Ω
hbddω : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
h_zero : WithTop.untopA (min (↑i : ℕ∞) (leastGE f r ω)) = 0
⊢ f (min (↑i : WithTop ℕ) (leastGE f r ω)).untopA ω ≤ r + (↑R : ℝ)
have pos : 0 ≤ r + (↑R : ℝ)
Tactic: simp only [h_zero, hf0, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.Probability.Martingale.BorelCantelli (goal)
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
i : ℕ
ω : Ω
hbddω : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
h_zero : ¬WithTop.untopA (min (↑i : ℕ∞) (leastGE f r ω)) = 0
⊢ f (min (↑i : WithTop ℕ) (leastGE f r ω)).untopA ω ≤ r + (↑R : ℝ)
have neg : ∀ (k : ℕ) (hk : WithTop.untopA (min (↑i : ℕ∞) (leastGE f r ω)) = k + 1),
  f (min (↑i : WithTop ℕ) (leastGE f r ω)).untopA ω ≤ r + (↑R : ℝ)
Tactic: obtain ⟨k, hk⟩ := Nat.exists_eq_add_one_of_ne_zero h_zero
-- Lean 4 proof step from Mathlib.Probability.Martingale.BorelCantelli (goal)
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
i : ℕ
ω : Ω
hbddω : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
h_zero : ¬WithTop.untopA (min (↑i : ℕ∞) (leastGE f r ω)) = 0
k : ℕ
hk : WithTop.untopA (min (↑i : ℕ∞) (leastGE f r ω)) = k + 1
⊢ f (min (↑i : WithTop ℕ) (leastGE f r ω)).untopA ω ≤ r + (↑R : ℝ)
have neg : f (k + 1) ω - r ≤ (↑R : ℝ)
Tactic: rw [hk, add_comm r, ← sub_le_iff_le_add]
-- Lean 4 proof step from Mathlib.Probability.Martingale.BorelCantelli (goal)
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
i : ℕ
ω : Ω
hbddω : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
h_zero : ¬WithTop.untopA (min (↑i : ℕ∞) (leastGE f r ω)) = 0
k : ℕ
hk : WithTop.untopA (min (↑i : ℕ∞) (leastGE f r ω)) = k + 1
⊢ f (k + 1) ω - r ≤ (↑R : ℝ)
have neg : ∀ (this : ∀ (hk₂ : LE.le (α := ℕ) ⊥ (↑k : ℕ)), f (↑k : ℕ) ω ∉ Set.Ici r), f (k + 1) ω - r ≤ (↑R : ℝ)
Tactic: have := notMem_of_lt_hittingAfter (?_ : k < leastGE f r ω)
-- Lean 4 proof step from Mathlib.Probability.Martingale.BorelCantelli (goal)
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
i : ℕ
ω : Ω
hbddω : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
h_zero : ¬WithTop.untopA (min (↑i : ℕ∞) (leastGE f r ω)) = 0
k : ℕ
hk : WithTop.untopA (min (↑i : ℕ∞) (leastGE f r ω)) = k + 1
neg : ∀ (this : ∀ (hk₂ : LE.le (α := ℕ) ⊥ (↑k : ℕ)), f (↑k : ℕ) ω ∉ Set.Ici r), f (k + 1) ω - r ≤ (↑R : ℝ)
⊢ f (k + 1) ω - r ≤ (↑R : ℝ)
have neg₁ : (↑k : WithTop ℕ) < leastGE f r ω
Tactic: have := notMem_of_lt_hittingAfter (?_ : k < leastGE f r ω)
-- Lean 4 proof step from Mathlib.Probability.Martingale.BorelCantelli (hypothesis)
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
i : ℕ
ω : Ω
hbddω : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
h_zero : ¬WithTop.untopA (min (↑i : ℕ∞) (leastGE f r ω)) = 0
k : ℕ
hk : WithTop.untopA (min (↑i : ℕ∞) (leastGE f r ω)) = k + 1
this : ∀ (hk₂ : LE.le (α := ℕ) ⊥ (↑k : ℕ)), f (↑k : ℕ) ω ∉ Set.Ici r
⊢ f (k + 1) ω - r ≤ (↑R : ℝ)
have this₁ : f (↑k : ℕ) ω < r
Tactic: simp only [bot_eq_zero, zero_le, Set.mem_Ici, not_le, forall_const] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Probability.Martingale.BorelCantelli (goal)
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
i : ℕ
ω : Ω
hbddω : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
h_zero : ¬WithTop.untopA (min (↑i : ℕ∞) (leastGE f r ω)) = 0
k : ℕ
hk : WithTop.untopA (min (↑i : ℕ∞) (leastGE f r ω)) = k + 1
⊢ (↑k : WithTop ℕ) < leastGE f r ω
have neg : (↑k : ℕ∞) < min (↑i : ℕ∞) (leastGE f r ω)
Tactic: suffices (k : ℕ∞) < min (i : ℕ∞) (leastGE f r ω) from this.trans_le (min_le_right _ _)
-- Lean 4 proof step from Mathlib.Probability.Martingale.BorelCantelli (hypothesis)
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
i : ℕ
ω : Ω
hbddω : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
h_zero : ¬WithTop.untopA (min (↑i : ℕ∞) (leastGE f r ω)) = 0
k : ℕ
hk : WithTop.untopA (min (↑i : ℕ∞) (leastGE f r ω)) = k + 1
⊢ (↑k : ℕ∞) < min (↑i : ℕ∞) (leastGE f r ω)
have h_top : min (↑i : ℕ∞) (leastGE f r ω) ≠ ⊤
Tactic: have h_top : min (i : ℕ∞) (leastGE f r ω) ≠ ⊤ :=
      ne_top_of_le_ne_top (by simp) (min_le_left _ _)
-- Lean 4 proof step from Mathlib.Probability.Martingale.BorelCantelli (goal)
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
i : ℕ
ω : Ω
hbddω : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
h_zero : ¬WithTop.untopA (min (↑i : ℕ∞) (leastGE f r ω)) = 0
k : ℕ
hk : WithTop.untopA (min (↑i : ℕ∞) (leastGE f r ω)) = k + 1
h_top : min (↑i : ℕ∞) (leastGE f r ω) ≠ ⊤
⊢ (↑k : ℕ∞) < min (↑i : ℕ∞) (leastGE f r ω)
have neg : ∀ (p : ℕ) (h_zero : ¬Eq (α := ℕ) (WithTop.untopA (↑p : ℕ∞)) 0) (hk : WithTop.untopA (↑p : ℕ∞) = k + 1),
  LT.lt (α := ℕ∞) (↑k : ℕ∞) (↑p : ℕ∞)
Tactic: lift min (i : ℕ∞) (leastGE f r ω) to ℕ using h_top with p
Cleared hypotheses: h_zero, hk, h_top
-- Lean 4 proof step from Mathlib.Probability.Martingale.BorelCantelli (goal)
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
i : ℕ
ω : Ω
hbddω : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
k p : ℕ
h_zero : ¬Eq (α := ℕ) (WithTop.untopA (↑p : ℕ∞)) 0
hk : WithTop.untopA (↑p : ℕ∞) = k + 1
⊢ LT.lt (α := ℕ∞) (↑k : ℕ∞) (↑p : ℕ∞)
have neg : k < p
Tactic: simp only [untopD_coe_enat, Nat.cast_lt, gt_iff_lt] at *
-- Lean 4 proof step from Mathlib.Probability.Martingale.BorelCantelli (goal)
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
i : ℕ
⊢ eLpNorm (stoppedAbove f r i) 1 μ ≤
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞) *
      ENNReal.ofReal (r + (↑R : ℝ))
have refine : LE.le (α := ℝ) 0 (∫ (x : Ω), stoppedAbove f r i x ∂μ)
Tactic: refine eLpNorm_one_le_of_le' ((hf.stoppedAbove r).integrable _) ?_
    (stoppedAbove_le hr hf0 hbdd i)
-- Lean 4 proof step from Mathlib.Probability.Martingale.BorelCantelli (goal)
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
i : ℕ
⊢ LE.le (α := ℝ) 0 (∫ (x : Ω), stoppedAbove f r i x ∂μ)
have rw : LE.le (α := ℝ) 0 (∫ (x : Ω) in Set.univ, stoppedAbove f r i x ∂μ)
Tactic: rw [← setIntegral_univ]
-- Lean 4 proof step from Mathlib.Probability.Martingale.BorelCantelli (goal)
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
i : ℕ
⊢ LE.le (α := ℝ) 0 (∫ (x : Ω) in Set.univ, stoppedAbove f r i x ∂μ)
have refine : LE.le (α := ℝ) 0 (∫ (ω : Ω) in Set.univ, stoppedAbove f r 0 ω ∂μ)
Tactic: refine le_trans ?_ ((hf.stoppedAbove r).setIntegral_le zero_le MeasurableSet.univ)
-- Lean 4 proof step from Mathlib.Probability.Martingale.BorelCantelli (goal)
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
i : ℕ
⊢ eLpNorm (stoppedAbove f r i) 1 μ ≤
    (↑(HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞) *
            ENNReal.ofReal (r + (↑R : ℝ))).toNNReal :
      ℝ≥0∞)
have refine : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞) *
    ENNReal.ofReal (r + (↑R : ℝ)) ≤
  (↑(HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞) *
          ENNReal.ofReal (r + (↑R : ℝ))).toNNReal :
    ℝ≥0∞)
Tactic: refine (hf.eLpNorm_stoppedAbove_le hr hf0 hbdd i).trans ?_
-- Lean 4 proof step from Mathlib.Probability.Martingale.BorelCantelli (goal)
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
⊢ ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ stoppedAbove f (↑i : ℝ) n ω) atTop (𝓝 c)
have rw : ∀ (i : ℕ), ∀ᵐ (a : Ω) ∂μ, ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ stoppedAbove f (↑i : ℝ) n a) atTop (𝓝 c)
Tactic: rw [ae_all_iff]
-- Lean 4 proof step from Mathlib.Probability.Martingale.BorelCantelli (hypothesis)
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
⊢ ∀ᵐ (ω : Ω) ∂μ,
    BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω) → ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
have ht : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ stoppedAbove f (↑i : ℝ) n ω) atTop (𝓝 c)
Tactic: have ht : ∀ᵐ ω ∂μ, ∀ i : ℕ, ∃ c, Tendsto (fun n => stoppedAbove f i n ω) atTop (𝓝 c) := by
    rw [ae_all_iff]
    exact fun i ↦ Submartingale.exists_ae_tendsto_of_bdd (hf.stoppedAbove i)
      (hf.eLpNorm_stoppedAbove_le' i.cast_nonneg hf0 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 μ
hf : Submartingale f ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
ht : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ stoppedAbove f (↑i : ℝ) n ω) atTop (𝓝 c)
⊢ ∀ᵐ (ω : Ω) ∂μ,
    BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω) → ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
have h : ∀ (ω : Ω) (hω : ∀ (i : ℕ), ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ stoppedAbove f (↑i : ℝ) n ω) atTop (𝓝 c))
  (hωb : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω)), ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
Tactic: filter_upwards [ht] with ω hω hωb
-- Lean 4 proof step from Mathlib.Probability.Martingale.BorelCantelli (hypothesis)
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
ht : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ stoppedAbove f (↑i : ℝ) n ω) atTop (𝓝 c)
ω : Ω
hω : ∀ (i : ℕ), ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ stoppedAbove f (↑i : ℝ) n ω) atTop (𝓝 c)
hωb : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω)
⊢ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
have hωb₁ : Set.Nonempty (α := ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ f n ω))
Tactic: rw [BddAbove] at hωb
Cleared hypotheses: hωb
-- Lean 4 proof step from Mathlib.Probability.Martingale.BorelCantelli (goal)
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
ht : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ stoppedAbove f (↑i : ℝ) n ω) atTop (𝓝 c)
ω : Ω
hω : ∀ (i : ℕ), ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ stoppedAbove f (↑i : ℝ) n ω) atTop (𝓝 c)
hωb : Set.Nonempty (α := ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ f n ω))
⊢ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
have h : ∀ (i : ℕ) (hi : hωb.some (s := upperBounds (Set.range fun (n : ℕ) ↦ f n ω)) < (↑i : ℝ)),
  ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
Tactic: obtain ⟨i, hi⟩ := exists_nat_gt hωb.some
-- Lean 4 proof step from Mathlib.Probability.Martingale.BorelCantelli (hypothesis)
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
ht : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ stoppedAbove f (↑i : ℝ) n ω) atTop (𝓝 c)
ω : Ω
hω : ∀ (i : ℕ), ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ stoppedAbove f (↑i : ℝ) n ω) atTop (𝓝 c)
hωb : Set.Nonempty (α := ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ f n ω))
i : ℕ
hi : hωb.some (s := upperBounds (Set.range fun (n : ℕ) ↦ f n ω)) < (↑i : ℝ)
⊢ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
have hib : ∀ (n : ℕ), f n ω < (↑i : ℝ)
Tactic: have hib : ∀ n, f n ω < i := by
    intro n
    exact lt_of_le_of_lt ((mem_upperBounds.1 hωb.some_mem) _ ⟨n, rfl⟩) hi
-- Lean 4 proof step from Mathlib.Probability.Martingale.BorelCantelli (goal)
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
ht : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ stoppedAbove f (↑i : ℝ) n ω) atTop (𝓝 c)
ω : Ω
hω : ∀ (i : ℕ), ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ stoppedAbove f (↑i : ℝ) n ω) atTop (𝓝 c)
hωb : Set.Nonempty (α := ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ f n ω))
i : ℕ
hi : hωb.some (s := upperBounds (Set.range fun (n : ℕ) ↦ f n ω)) < (↑i : ℝ)
hib : ∀ (n : ℕ), f n ω < (↑i : ℝ)
n : ℕ
⊢ stoppedAbove f (↑i : ℝ) n ω = f n ω
have rw : f (min (↑n : WithTop ℕ) ⊤).untopA ω = f n ω
Tactic: rw [stoppedAbove, stoppedProcess, leastGE, hittingAfter_eq_top_iff.mpr]
-- Lean 4 proof step from Mathlib.Probability.Martingale.BorelCantelli (goal)
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
ht : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ stoppedAbove f (↑i : ℝ) n ω) atTop (𝓝 c)
ω : Ω
hω : ∀ (i : ℕ), ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ stoppedAbove f (↑i : ℝ) n ω) atTop (𝓝 c)
hωb : Set.Nonempty (α := ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ f n ω))
i : ℕ
hi : hωb.some (s := upperBounds (Set.range fun (n : ℕ) ↦ f n ω)) < (↑i : ℝ)
hib : ∀ (n : ℕ), f n ω < (↑i : ℝ)
n : ℕ
rw : f (min (↑n : WithTop ℕ) ⊤).untopA ω = f n ω
⊢ stoppedAbove f (↑i : ℝ) n ω = f n ω
have rw₁ : ∀ (j : ℕ), ⊥ ≤ j → f j ω ∉ Set.Ici (↑i : ℝ)
Tactic: rw [stoppedAbove, stoppedProcess, leastGE, hittingAfter_eq_top_iff.mpr]
-- Lean 4 proof step from Mathlib.Probability.Martingale.BorelCantelli (goal)
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
ht : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ stoppedAbove f (↑i : ℝ) n ω) atTop (𝓝 c)
ω : Ω
hω : ∀ (i : ℕ), ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ stoppedAbove f (↑i : ℝ) n ω) atTop (𝓝 c)
hωb : Set.Nonempty (α := ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ f n ω))
i : ℕ
hi : hωb.some (s := upperBounds (Set.range fun (n : ℕ) ↦ f n ω)) < (↑i : ℝ)
hib : ∀ (n : ℕ), f n ω < (↑i : ℝ)
n : ℕ
⊢ f (min (↑n : WithTop ℕ) ⊤).untopA ω = f n ω
have simp : f (↑n : WithTop ℕ).untopA ω = f n ω
Tactic: simp only [le_top, inf_of_le_left]
-- Lean 4 proof step from Mathlib.Probability.Martingale.BorelCantelli (hypothesis)
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
ht : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ stoppedAbove f (↑i : ℝ) n ω) atTop (𝓝 c)
ω : Ω
hω : ∀ (i : ℕ), ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ stoppedAbove f (↑i : ℝ) n ω) atTop (𝓝 c)
hωb : Set.Nonempty (α := ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ f n ω))
i : ℕ
hi : hωb.some (s := upperBounds (Set.range fun (n : ℕ) ↦ f n ω)) < (↑i : ℝ)
hib : ∀ (n : ℕ), f n ω < (↑i : ℝ)
⊢ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
have heq : ∀ (n : ℕ), stoppedAbove f (↑i : ℝ) n ω = f n ω
Tactic: have heq : ∀ n, stoppedAbove f i n ω = f n ω := by
    intro n
    rw [stoppedAbove, stoppedProcess, leastGE, hittingAfter_eq_top_iff.mpr]
    · simp only [le_top, inf_of_le_left]
      congr
    · simp [hib]
-- Lean 4 proof step from Mathlib.Probability.Martingale.BorelCantelli (goal)
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
⊢ ∀ᵐ (ω : Ω) ∂μ,
    BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
have h : ∀ (a : Ω),
  Membership.mem (γ := Set Ω)
    {x : Ω |
      Membership.mem (γ := Set Ω)
          {x : Ω |
            (fun (ω : Ω) ↦
                BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω) →
                  ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c))
              x}
          x →
        Membership.mem (γ := Set Ω)
          {x : Ω |
            (fun (ω : Ω) ↦
                BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω) ↔
                  ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c))
              x}
          x}
    a
Tactic: filter_upwards [hf.exists_tendsto_of_abs_bddAbove_aux hf0 hbdd] with ω hω using
    ⟨hω, fun ⟨c, hc⟩ => hc.bddAbove_range⟩
-- Lean 4 proof step from Mathlib.Probability.Martingale.BorelCantelli (goal)
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
h :
  ∀ (a : Ω),
    Membership.mem (γ := Set Ω)
      {x : Ω |
        Membership.mem (γ := Set Ω)
            {x : Ω |
              (fun (ω : Ω) ↦
                  BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω) →
                    ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c))
                x}
            x →
          Membership.mem (γ := Set Ω)
            {x : Ω |
              (fun (ω : Ω) ↦
                  BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω) ↔
                    ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c))
                x}
            x}
      a
⊢ ∀ᵐ (ω : Ω) ∂μ,
    BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
have h₁ : ∀ (a : Ω),
  (BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n a) → ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n a) atTop (𝓝 c)) →
    (BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n a) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n a) atTop (𝓝 c))
Tactic: filter_upwards [hf.exists_tendsto_of_abs_bddAbove_aux hf0 hbdd] with ω hω using
    ⟨hω, fun ⟨c, hc⟩ => hc.bddAbove_range⟩
-- Lean 4 proof step from Mathlib.Probability.Martingale.BorelCantelli (hypothesis)
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
g : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ f n ω - f 0 ω
⊢ ∀ᵐ (ω : Ω) ∂μ,
    BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
have hg : Submartingale g ℱ μ
Tactic: have hg : Submartingale g ℱ μ :=
    hf.sub_martingale (martingale_const_fun _ _ (hf.stronglyAdapted 0) (hf.integrable 0))