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 : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
g : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ f n ω - f 0 ω
hg : Submartingale g ℱ μ
⊢ g 0 = 0
have h : ∀ (ω : Ω), g 0 ω = 0 ω
Tactic: ext ω
-- 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 ω
hg : Submartingale g ℱ μ
⊢ ∀ᵐ (ω : Ω) ∂μ,
    BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
have hg0 : g 0 = 0
Tactic: have hg0 : g 0 = 0 := by
    ext ω
    simp only [g, sub_self, Pi.zero_apply]
-- 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 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
⊢ ∀ᵐ (ω : Ω) ∂μ,
    BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
have hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ (↑R : ℝ)
Tactic: have hgbdd : ∀ᵐ ω ∂μ, ∀ i : ℕ, |g (i + 1) ω - g i ω| ≤ ↑R := by
    simpa only [g, sub_sub_sub_cancel_right]
-- 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 ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
g : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ (↑R : ℝ)
⊢ ∀ᵐ (ω : Ω) ∂μ,
    BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
have h : ∀ (ω : Ω)
  (hω : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ g n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ g n ω) atTop (𝓝 c)),
  BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
Tactic: filter_upwards [hg.bddAbove_iff_exists_tendsto_aux hg0 hgbdd] with ω 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 : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
g : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ (↑R : ℝ)
ω : Ω
hω : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ g n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ g n ω) atTop (𝓝 c)
⊢ BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
have h : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω) ↔ BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ g n ω)
Tactic: convert! hω using 1
-- 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 ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
g : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ (↑R : ℝ)
ω : Ω
hω : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ g n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ g n ω) atTop (𝓝 c)
h : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω) ↔ BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ g n ω)
⊢ BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
have h₁ : (∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ g n ω) atTop (𝓝 c)
Tactic: convert! hω using 1
-- 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 ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
g : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ (↑R : ℝ)
ω : Ω
hω : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ g n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ g n ω) atTop (𝓝 c)
⊢ BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω) ↔ BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ g n ω)
have h : ∀ (h : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω)), BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ g n ω)
Tactic: refine ⟨fun h => ?_, 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 : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
g : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ (↑R : ℝ)
ω : Ω
hω : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ g n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ g n ω) atTop (𝓝 c)
h : ∀ (h : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω)), BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ g n ω)
⊢ BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω) ↔ BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ g n ω)
have h₁ : ∀ (h : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ g n ω)), BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω)
Tactic: refine ⟨fun h => ?_, 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 : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
g : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ (↑R : ℝ)
ω : Ω
hω : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ g n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ g n ω) atTop (𝓝 c)
h : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω)
⊢ BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ g n ω)
have h₁ : ∀ (b : ℝ) (hb : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ f n ω)) b),
  BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ g n ω)
Tactic: obtain ⟨b, hb⟩ := 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 : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
g : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ (↑R : ℝ)
ω : Ω
hω : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ g n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ g n ω) atTop (𝓝 c)
h : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ g n ω)
⊢ BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω)
have h₁ : ∀ (b : ℝ) (hb : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ g n ω)) b),
  BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω)
Tactic: obtain ⟨b, hb⟩ := 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 : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
g : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ (↑R : ℝ)
ω : Ω
hω : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ g n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ g n ω) atTop (𝓝 c)
b : ℝ
hb : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ f n ω)) b
⊢ BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ g n ω)
have h : ∀ (y : ℝ) (hy : Membership.mem (γ := Set ℝ) (Set.range fun (n : ℕ) ↦ g n ω) y), y ≤ b + |f 0 ω|
Tactic: refine ⟨b + |f 0 ω|, fun y hy => ?_⟩
-- 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 ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
g : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ (↑R : ℝ)
ω : Ω
hω : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ g n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ g n ω) atTop (𝓝 c)
b : ℝ
hb : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ g n ω)) b
⊢ BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω)
have h : ∀ (y : ℝ) (hy : Membership.mem (γ := Set ℝ) (Set.range fun (n : ℕ) ↦ f n ω) y), y ≤ b + |f 0 ω|
Tactic: refine ⟨b + |f 0 ω|, fun y hy => ?_⟩
-- 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 ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
g : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ (↑R : ℝ)
ω : Ω
hω : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ g n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ g n ω) atTop (𝓝 c)
b : ℝ
hb : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ f n ω)) b
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Set.range fun (n : ℕ) ↦ g n ω) y
⊢ y ≤ b + |f 0 ω|
have h : ∀ (n : ℕ), (fun (n : ℕ) ↦ g n ω) n ≤ b + |f 0 ω|
Tactic: obtain ⟨n, rfl⟩ := hy
Cleared hypotheses: y, hy
-- 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 ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
g : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ (↑R : ℝ)
ω : Ω
hω : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ g n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ g n ω) atTop (𝓝 c)
b : ℝ
hb : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ g n ω)) b
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Set.range fun (n : ℕ) ↦ f n ω) y
⊢ y ≤ b + |f 0 ω|
have h : ∀ (n : ℕ), (fun (n : ℕ) ↦ f n ω) n ≤ b + |f 0 ω|
Tactic: obtain ⟨n, rfl⟩ := hy
Cleared hypotheses: y, hy
-- 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 ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
g : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ (↑R : ℝ)
ω : Ω
hω : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ g n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ g n ω) atTop (𝓝 c)
b : ℝ
hb : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ f n ω)) b
n : ℕ
⊢ (fun (n : ℕ) ↦ g n ω) n ≤ b + |f 0 ω|
have h : f n ω + -f 0 ω ≤ b + |f 0 ω|
Tactic: simp_rw [g, sub_eq_add_neg]
-- 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 ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
g : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ (↑R : ℝ)
ω : Ω
hω : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ g n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ g n ω) atTop (𝓝 c)
⊢ (∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ g n ω) atTop (𝓝 c)
have h : ∀ (h : ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)), ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ g n ω) atTop (𝓝 c)
Tactic: refine ⟨fun h => ?_, 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 : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
g : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ (↑R : ℝ)
ω : Ω
hω : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ g n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ g n ω) atTop (𝓝 c)
h : ∀ (h : ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)), ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ g n ω) atTop (𝓝 c)
⊢ (∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ g n ω) atTop (𝓝 c)
have h₁ : ∀ (h : ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ g n ω) atTop (𝓝 c)), ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
Tactic: refine ⟨fun h => ?_, 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 : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
g : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ (↑R : ℝ)
ω : Ω
hω : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ g n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ g n ω) atTop (𝓝 c)
h : ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
⊢ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ g n ω) atTop (𝓝 c)
have h₁ : ∀ (c : ℝ) (hc : Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)), ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ g n ω) atTop (𝓝 c)
Tactic: obtain ⟨c, hc⟩ := 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 : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
g : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ (↑R : ℝ)
ω : Ω
hω : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ g n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ g n ω) atTop (𝓝 c)
h : ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ g n ω) atTop (𝓝 c)
⊢ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
have h₁ : ∀ (c : ℝ) (hc : Tendsto (fun (n : ℕ) ↦ g n ω) atTop (𝓝 c)), ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
Tactic: obtain ⟨c, hc⟩ := 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 : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
g : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ (↑R : ℝ)
ω : Ω
hω : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ g n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ g n ω) atTop (𝓝 c)
c : ℝ
hc : Tendsto (fun (n : ℕ) ↦ g n ω) atTop (𝓝 c)
⊢ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
have h : Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (c + f 0 ω))
Tactic: refine ⟨c + f 0 ω, ?_⟩
-- 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 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ (↑R : ℝ)
ω : Ω
hω : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ g n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ g n ω) atTop (𝓝 c)
c : ℝ
hc : Tendsto (fun (n : ℕ) ↦ g n ω) atTop (𝓝 c)
⊢ Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (c + f 0 ω))
have this : Tendsto (fun (x : ℕ) ↦ g x ω + f 0 ω) atTop (𝓝 (c + f 0 ω))
Tactic: have := hc.add_const (f 0 ω)
-- 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 : ℝ)
⊢ ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ (↑R : ℝ)
have h : ∀ (ω : Ω) (hω : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)) (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ (↑R : ℝ)
Tactic: filter_upwards [hbdd] with ω hω i
-- 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 : ℝ)
⊢ ∀ᵐ (ω : Ω) ∂μ, BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω) ↔ BddBelow (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω)
have hbdd' : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ (↑R : ℝ)
Tactic: have hbdd' : ∀ᵐ ω ∂μ, ∀ i, |(-f) (i + 1) ω - (-f) i ω| ≤ R := by
    filter_upwards [hbdd] with ω hω i
    simp only [Pi.neg_apply]
    grind
-- 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 : ℝ)
⊢ ∀ᵐ (ω : Ω) ∂μ, BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω) ↔ BddBelow (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω)
have hup : ∀ᵐ (ω : Ω) ∂μ, BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
Tactic: have hup := hf.submartingale.bddAbove_iff_exists_tendsto 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 μ
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)
⊢ ∀ᵐ (ω : Ω) ∂μ, BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω) ↔ BddBelow (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω)
have hdown : ∀ᵐ (ω : Ω) ∂μ,
  BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ (-f) n ω) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ (-f) n ω) atTop (𝓝 c)
Tactic: have hdown := hf.neg.submartingale.bddAbove_iff_exists_tendsto 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 : 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)
⊢ ∀ᵐ (ω : Ω) ∂μ, BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω) ↔ BddBelow (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω)
have h : ∀ (ω : Ω)
  (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 ω)
Tactic: filter_upwards [hup, hdown] with ω 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 μ
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 : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ (-f) n ω) atTop (𝓝 c)
have mp : (∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)) → ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ (-f) n ω) atTop (𝓝 c)
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)
mp : (∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)) → ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ (-f) n ω) atTop (𝓝 c)
⊢ (∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)) ↔ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ (-f) n ω) atTop (𝓝 c)
have mpr : (∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ (-f) n ω) atTop (𝓝 c)) → ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
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)
c : ℝ
hc : Tendsto (fun (n : ℕ) ↦ (-f) n ω) atTop (𝓝 c)
⊢ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
have mpr : Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (-c))
Tactic: refine ⟨-c, ?_⟩