awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
hbdd' : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ (↑R : ℝ)
hup :
  ∀ᵐ (ω : Ω) ∂μ,
    BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
hdown :
  ∀ᵐ (ω : Ω) ∂μ,
    BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ (-f) n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ (-f) n ω) atTop (𝓝 c)
ω : Ω
hω₁ : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
hω₂ : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ (-f) n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ (-f) n ω) atTop (𝓝 c)
c : ℝ
hc : Tendsto (fun (n : ℕ) ↦ (-f) n ω) atTop (𝓝 c)
⊢ Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (-c))
have h : ∀ (x : ℕ), f x ω = -(-f) x ω
Tactic: convert! hc.neg
-- 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 : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
hbdd' : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ (↑R : ℝ)
hup :
  ∀ᵐ (ω : Ω) ∂μ,
    BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
hdown :
  ∀ᵐ (ω : Ω) ∂μ,
    BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ (-f) n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ (-f) n ω) atTop (𝓝 c)
ω : Ω
hω₁ : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
hω₂ : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ (-f) n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ (-f) n ω) atTop (𝓝 c)
⊢ BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω) ↔ BddBelow (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω)
have this : (∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ (-f) n ω) atTop (𝓝 c)
Tactic: have : (∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)) ↔
      ∃ c, Tendsto (fun n => (-f) n ω) atTop (𝓝 c) := by
    constructor <;> rintro ⟨c, hc⟩
    · exact ⟨-c, hc.neg⟩
    · refine ⟨-c, ?_⟩
      convert! hc.neg
      simp only [neg_neg, Pi.neg_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 μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
hbdd' : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ (↑R : ℝ)
hup :
  ∀ᵐ (ω : Ω) ∂μ,
    BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
hdown :
  ∀ᵐ (ω : Ω) ∂μ,
    BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ (-f) n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ (-f) n ω) atTop (𝓝 c)
ω : Ω
hω₁ : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
hω₂ : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ (-f) n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ (-f) n ω) atTop (𝓝 c)
this : (∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ (-f) n ω) atTop (𝓝 c)
⊢ BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω) ↔ BddBelow (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω)
have h : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ (-f) n ω) ↔ BddBelow (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω)
Tactic: rw [hω₁, this, ← 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 μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
hbdd' : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ (↑R : ℝ)
hup :
  ∀ᵐ (ω : Ω) ∂μ,
    BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
hdown :
  ∀ᵐ (ω : Ω) ∂μ,
    BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ (-f) n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ (-f) n ω) atTop (𝓝 c)
ω : Ω
hω₁ : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
hω₂ : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ (-f) n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ (-f) n ω) atTop (𝓝 c)
this : (∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ (-f) n ω) atTop (𝓝 c)
⊢ BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ (-f) n ω) ↔ BddBelow (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω)
have h : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ (-f) n ω) → BddBelow (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω)
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 μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
hbdd' : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ (↑R : ℝ)
hup :
  ∀ᵐ (ω : Ω) ∂μ,
    BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
hdown :
  ∀ᵐ (ω : Ω) ∂μ,
    BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ (-f) n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ (-f) n ω) atTop (𝓝 c)
ω : Ω
hω₁ : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
hω₂ : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ (-f) n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ (-f) n ω) atTop (𝓝 c)
this : (∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ (-f) n ω) atTop (𝓝 c)
h : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ (-f) n ω) → BddBelow (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω)
⊢ BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ (-f) n ω) ↔ BddBelow (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω)
have h₁ : BddBelow (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω) → BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ (-f) n ω)
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 μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
hbdd' : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ (↑R : ℝ)
hup :
  ∀ᵐ (ω : Ω) ∂μ,
    BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
hdown :
  ∀ᵐ (ω : Ω) ∂μ,
    BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ (-f) n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ (-f) n ω) atTop (𝓝 c)
ω : Ω
hω₁ : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
hω₂ : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ (-f) n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ (-f) n ω) atTop (𝓝 c)
this : (∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ (-f) n ω) atTop (𝓝 c)
c : ℝ
hc : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ (-f) n ω)) c
⊢ BddBelow (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω)
have h : ∀ (ω_1 : ℝ) (hω : Membership.mem (γ := Set ℝ) (Set.range fun (n : ℕ) ↦ f n ω) ω_1), -c ≤ ω_1
Tactic: refine ⟨-c, fun ω 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 μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
hbdd' : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ (↑R : ℝ)
hup :
  ∀ᵐ (ω : Ω) ∂μ,
    BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
hdown :
  ∀ᵐ (ω : Ω) ∂μ,
    BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ (-f) n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ (-f) n ω) atTop (𝓝 c)
ω : Ω
hω₁ : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
hω₂ : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ (-f) n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ (-f) n ω) atTop (𝓝 c)
this : (∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ (-f) n ω) atTop (𝓝 c)
c : ℝ
hc : Membership.mem (γ := Set ℝ) (lowerBounds (Set.range fun (n : ℕ) ↦ f n ω)) c
⊢ BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ (-f) n ω)
have h : ∀ (ω_1 : ℝ) (hω : Membership.mem (γ := Set ℝ) (Set.range fun (n : ℕ) ↦ (-f) n ω) ω_1), ω_1 ≤ -c
Tactic: refine ⟨-c, fun ω 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 μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
hbdd' : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ (↑R : ℝ)
hup :
  ∀ᵐ (ω : Ω) ∂μ,
    BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
hdown :
  ∀ᵐ (ω : Ω) ∂μ,
    BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ (-f) n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ (-f) n ω) atTop (𝓝 c)
ω_1 : Ω
hω₁ : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω_1) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω_1) atTop (𝓝 c)
hω₂ : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ (-f) n ω_1) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ (-f) n ω_1) atTop (𝓝 c)
this :
  (∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω_1) atTop (𝓝 c)) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ (-f) n ω_1) atTop (𝓝 c)
c : ℝ
hc : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ (-f) n ω_1)) c
ω : ℝ
hω : Membership.mem (γ := Set ℝ) (Set.range fun (n : ℕ) ↦ f n ω_1) ω
⊢ -c ≤ ω
have h : ∀ (hc : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.range fun (n : ℕ) ↦ (-f) n ω_1) x → x ≤ c) (ω : ℝ)
  (hω : Membership.mem (γ := Set ℝ) (Set.range fun (n : ℕ) ↦ f n ω_1) ω), -c ≤ ω
Tactic: rw [mem_upperBounds] at hc
Cleared hypotheses: hc, ω, 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 μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
hbdd' : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ (↑R : ℝ)
hup :
  ∀ᵐ (ω : Ω) ∂μ,
    BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
hdown :
  ∀ᵐ (ω : Ω) ∂μ,
    BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ (-f) n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ (-f) n ω) atTop (𝓝 c)
ω_1 : Ω
hω₁ : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω_1) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω_1) atTop (𝓝 c)
hω₂ : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ (-f) n ω_1) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ (-f) n ω_1) atTop (𝓝 c)
this :
  (∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω_1) atTop (𝓝 c)) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ (-f) n ω_1) atTop (𝓝 c)
c : ℝ
hc : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.range fun (n : ℕ) ↦ (-f) n ω_1) x → x ≤ c
ω : ℝ
hω : Membership.mem (γ := Set ℝ) (Set.range fun (n : ℕ) ↦ f n ω_1) ω
⊢ -c ≤ ω
have h : Membership.mem (γ := Set ℝ) (Set.range fun (n : ℕ) ↦ (-f) n ω_1) (-ω)
Tactic: refine neg_le.2 (hc _ ?_)
-- 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 : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
hbdd' : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ (↑R : ℝ)
hup :
  ∀ᵐ (ω : Ω) ∂μ,
    BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
hdown :
  ∀ᵐ (ω : Ω) ∂μ,
    BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ (-f) n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ (-f) n ω) atTop (𝓝 c)
ω_1 : Ω
hω₁ : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω_1) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω_1) atTop (𝓝 c)
hω₂ : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ (-f) n ω_1) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ (-f) n ω_1) atTop (𝓝 c)
this :
  (∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω_1) atTop (𝓝 c)) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ (-f) n ω_1) atTop (𝓝 c)
c : ℝ
hc : Membership.mem (γ := Set ℝ) (lowerBounds (Set.range fun (n : ℕ) ↦ f n ω_1)) c
ω : ℝ
hω : Membership.mem (γ := Set ℝ) (Set.range fun (n : ℕ) ↦ (-f) n ω_1) ω
⊢ ω ≤ -c
have h : ∀ (hc : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.range fun (n : ℕ) ↦ f n ω_1) x → c ≤ x) (ω : ℝ)
  (hω : Membership.mem (γ := Set ℝ) (Set.range fun (n : ℕ) ↦ (-f) n ω_1) ω), ω ≤ -c
Tactic: rw [mem_lowerBounds] at hc
Cleared hypotheses: hc, ω, 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 μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
hbdd' : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ (↑R : ℝ)
hup :
  ∀ᵐ (ω : Ω) ∂μ,
    BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
hdown :
  ∀ᵐ (ω : Ω) ∂μ,
    BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ (-f) n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ (-f) n ω) atTop (𝓝 c)
ω_1 : Ω
hω₁ : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω_1) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω_1) atTop (𝓝 c)
hω₂ : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ (-f) n ω_1) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ (-f) n ω_1) atTop (𝓝 c)
this :
  (∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω_1) atTop (𝓝 c)) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ (-f) n ω_1) atTop (𝓝 c)
c : ℝ
hc : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.range fun (n : ℕ) ↦ f n ω_1) x → c ≤ x
ω : ℝ
hω : Membership.mem (γ := Set ℝ) (Set.range fun (n : ℕ) ↦ (-f) n ω_1) ω
⊢ ω ≤ -c
have hω₃ : ∃ (y : ℕ), f y ω_1 = -ω
Tactic: simp_rw [Set.mem_range, Pi.neg_apply, neg_eq_iff_eq_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 μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
hbdd' : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ (↑R : ℝ)
hup :
  ∀ᵐ (ω : Ω) ∂μ,
    BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
hdown :
  ∀ᵐ (ω : Ω) ∂μ,
    BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ (-f) n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ (-f) n ω) atTop (𝓝 c)
ω_1 : Ω
hω₁ : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω_1) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω_1) atTop (𝓝 c)
hω₂ : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ (-f) n ω_1) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ (-f) n ω_1) atTop (𝓝 c)
this :
  (∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω_1) atTop (𝓝 c)) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ (-f) n ω_1) atTop (𝓝 c)
c : ℝ
hc : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.range fun (n : ℕ) ↦ f n ω_1) x → c ≤ x
ω : ℝ
hω : ∃ (y : ℕ), f y ω_1 = -ω
⊢ ω ≤ -c
have h : Membership.mem (γ := Set ℝ) (Set.range fun (n : ℕ) ↦ f n ω_1) (-ω)
Tactic: refine le_neg.1 (hc _ ?_)
-- 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 : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
⊢ ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ f n ω) atTop atTop
have h : ∀ (a : Ω),
  Membership.mem (γ := Set Ω)
    {x : Ω |
      Membership.mem (γ := Set Ω)
          {x : Ω |
            (fun (ω : Ω) ↦
                BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω) ↔ BddBelow (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω))
              x}
          x →
        Membership.mem (γ := Set Ω) {x : Ω | (fun (ω : Ω) ↦ ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ f n ω) atTop atTop) x} x}
    a
Tactic: filter_upwards [hf.bddAbove_range_iff_bddBelow_range hbdd] with ω hω htop using
    not_bddAbove_of_tendsto_atTop htop (hω.2 <| bddBelow_range_of_tendsto_atTop_atTop htop)
-- 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 : Martingale f ℱ μ
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 ω) ↔ BddBelow (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω))
                x}
            x →
          Membership.mem (γ := Set Ω) {x : Ω | (fun (ω : Ω) ↦ ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ f n ω) atTop atTop) x} x}
      a
⊢ ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ f n ω) atTop atTop
have h₁ : ∀ (a : Ω),
  (BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n a) ↔ BddBelow (α := ℝ) (Set.range fun (n : ℕ) ↦ f n a)) →
    ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ f n a) atTop atTop
Tactic: filter_upwards [hf.bddAbove_range_iff_bddBelow_range hbdd] with ω hω htop using
    not_bddAbove_of_tendsto_atTop htop (hω.2 <| bddBelow_range_of_tendsto_atTop_atTop htop)
-- 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 : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
⊢ ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ f n ω) atTop atBot
have h : ∀ (a : Ω),
  Membership.mem (γ := Set Ω)
    {x : Ω |
      Membership.mem (γ := Set Ω)
          {x : Ω |
            (fun (ω : Ω) ↦
                BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω) ↔ BddBelow (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω))
              x}
          x →
        Membership.mem (γ := Set Ω) {x : Ω | (fun (ω : Ω) ↦ ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ f n ω) atTop atBot) x} x}
    a
Tactic: filter_upwards [hf.bddAbove_range_iff_bddBelow_range hbdd] with ω hω htop using
    not_bddBelow_of_tendsto_atBot htop (hω.1 <| bddAbove_range_of_tendsto_atTop_atBot htop)
-- 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 : Martingale f ℱ μ
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 ω) ↔ BddBelow (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω))
                x}
            x →
          Membership.mem (γ := Set Ω) {x : Ω | (fun (ω : Ω) ↦ ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ f n ω) atTop atBot) x} x}
      a
⊢ ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ f n ω) atTop atBot
have h₁ : ∀ (a : Ω),
  (BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n a) ↔ BddBelow (α := ℝ) (Set.range fun (n : ℕ) ↦ f n a)) →
    ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ f n a) atTop atBot
Tactic: filter_upwards [hf.bddAbove_range_iff_bddBelow_range hbdd] with ω hω htop using
    not_bddBelow_of_tendsto_atBot htop (hω.1 <| bddAbove_range_of_tendsto_atTop_atBot htop)
-- Lean 4 proof step from Mathlib.Probability.Martingale.BorelCantelli (goal)
Goal:
Ω : Type u_2
s : ℕ → Set Ω
⊢ process s 0 = 0
have rw : Eq.{u_2 + 1} (α := Ω → ℝ) (∑ k ∈ Finset.range 0, (s (k + 1)).indicator 1) 0
Tactic: rw [process, Finset.range_zero, Finset.sum_empty]
-- Lean 4 proof step from Mathlib.Probability.Martingale.BorelCantelli (goal)
Goal:
Ω : Type u_2
s : ℕ → Set Ω
rw : Eq.{u_2 + 1} (α := Ω → ℝ) (∑ k ∈ Finset.range 0, (s (k + 1)).indicator 1) 0
⊢ process s 0 = 0
have rw₁ : Eq.{u_2 + 1} (α := Ω → ℝ) (∑ k ∈ ∅, (s (k + 1)).indicator 1) 0
Tactic: rw [process, Finset.range_zero, Finset.sum_empty]
-- Lean 4 proof step from Mathlib.Probability.Martingale.BorelCantelli (goal)
Goal:
Ω : Type u_2
s : ℕ → Set Ω
rw : Eq.{u_2 + 1} (α := Ω → ℝ) (∑ k ∈ Finset.range 0, (s (k + 1)).indicator 1) 0
rw₁ : Eq.{u_2 + 1} (α := Ω → ℝ) (∑ k ∈ ∅, (s (k + 1)).indicator 1) 0
⊢ process s 0 = 0
have rw₂ : Eq.{u_2 + 1} (α := Ω → ℝ) 0 0
Tactic: rw [process, Finset.range_zero, Finset.sum_empty]
-- Lean 4 proof step from Mathlib.Probability.Martingale.BorelCantelli (goal)
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]
have simp : 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: simp only [martingalePart_eq_sum, process_zero, zero_add]
-- Lean 4 proof step from Mathlib.Probability.Martingale.BorelCantelli (goal)
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])
have 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]
Tactic: refine Finset.sum_congr rfl fun k _ => ?_
-- Lean 4 proof step from Mathlib.Probability.Martingale.BorelCantelli (hypothesis)
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
ℱ : Filtration ℕ m0
μ : Measure Ω
s : ℕ → Set Ω
n : ℕ
⊢ predictablePart (process s) ℱ μ n = ∑ k ∈ Finset.range n, μ[(s (k + 1)).indicator 1 | (↑ℱ : ℕ → MeasurableSpace Ω) k]
have this : 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
-- Lean 4 proof step from Mathlib.Probability.Martingale.BorelCantelli (hypothesis)
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]
⊢ predictablePart (process s) ℱ μ n = ∑ k ∈ Finset.range n, μ[(s (k + 1)).indicator 1 | (↑ℱ : ℕ → MeasurableSpace Ω) k]
have 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])
Tactic: simp_rw [martingalePart, process, Finset.sum_sub_distrib] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Probability.Martingale.BorelCantelli (goal)
Goal:
Ω : Type u_2
s : ℕ → Set Ω
ω : Ω
n : ℕ
⊢ |process s (n + 1) ω - process s n ω| ≤ 1
have rw : LE.le (α := ℝ) ((s (n + 1)).indicator (fun (a : Ω) ↦ norm (E := ℝ) (1 a)) ω) 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]
-- Lean 4 proof step from Mathlib.Probability.Martingale.BorelCantelli (goal)
Goal:
Ω : Type u_2
s : ℕ → Set Ω
ω : Ω
n : ℕ
⊢ LE.le (α := ℝ) ((s (n + 1)).indicator (fun (a : Ω) ↦ norm (E := ℝ) (1 a)) ω) 1
have refine : ∀ x ∈ s (n + 1), norm (E := ℝ) (1 x) ≤ 1
Tactic: refine Set.indicator_le' (fun _ _ => ?_) (fun _ _ => zero_le_one) _