awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Martingale.BorelCantelli
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 ω)
h₁ : BddBelow (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω) → BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ (-f) n ω)
⊢ BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ (-f) n ω) ↔ BddBelow (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω)

Tactic:
constructor
-- Module: Mathlib.Probability.Martingale.BorelCantelli
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 ω)

Tactic:
⟨-c, fun ω hω => ?_⟩

Premises used: Set.Nonempty, BddBelow, Exists.intro, Neg.neg
-- Module: Mathlib.Probability.Martingale.BorelCantelli
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
h : ∀ (ω_1 : ℝ) (hω : Membership.mem (γ := Set ℝ) (Set.range fun (n : ℕ) ↦ f n ω) ω_1), -c ≤ ω_1
⊢ BddBelow (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω)

Tactic:
refine ⟨-c, fun ω hω => ?_⟩
-- Module: Mathlib.Probability.Martingale.BorelCantelli
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 ω)

Tactic:
⟨-c, fun ω hω => ?_⟩

Premises used: BddAbove, Set.Nonempty, Exists.intro, Neg.neg
-- Module: Mathlib.Probability.Martingale.BorelCantelli
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
h : ∀ (ω_1 : ℝ) (hω : Membership.mem (γ := Set ℝ) (Set.range fun (n : ℕ) ↦ (-f) n ω) ω_1), ω_1 ≤ -c
⊢ BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ (-f) n ω)

Tactic:
refine ⟨-c, fun ω hω => ?_⟩
-- Module: Mathlib.Probability.Martingale.BorelCantelli
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) ω
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 ≤ ω
⊢ -c ≤ ω

Tactic:
rw [mem_upperBounds] at hc

Premises used: mem_upperBounds
-- Module: Mathlib.Probability.Martingale.BorelCantelli
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 ≤ ω

Tactic:
neg_le.2 (hc _ ?_)

Premises used: Iff.mpr, neg_le
-- Module: Mathlib.Probability.Martingale.BorelCantelli
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) ω
h : Membership.mem (γ := Set ℝ) (Set.range fun (n : ℕ) ↦ (-f) n ω_1) (-ω)
⊢ -c ≤ ω

Tactic:
refine neg_le.2 (hc _ ?_)

Premises used: Iff.mpr, neg_le
-- Module: Mathlib.Probability.Martingale.BorelCantelli
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) ω
⊢ Membership.mem (γ := Set ℝ) (Set.range fun (n : ℕ) ↦ (-f) n ω_1) (-ω)

Tactic:
simpa only [Pi.neg_apply, Set.mem_range, neg_inj]

Premises used: Set.mem_range, neg_inj, Pi.neg_apply
-- Module: Mathlib.Probability.Martingale.BorelCantelli
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) ω
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
⊢ ω ≤ -c

Tactic:
rw [mem_lowerBounds] at hc

Premises used: mem_lowerBounds
-- Module: Mathlib.Probability.Martingale.BorelCantelli
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) ω
⊢ ∃ (y : ℕ), f y ω_1 = -ω

Tactic:
simp_rw [Set.mem_range, Pi.neg_apply, neg_eq_iff_eq_neg] at hω

Premises used: Set.mem_range, neg_eq_iff_eq_neg, Pi.neg_apply
-- Module: Mathlib.Probability.Martingale.BorelCantelli
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

Tactic:
le_neg.1 (hc _ ?_)

Premises used: le_neg, Iff.mp
-- Module: Mathlib.Probability.Martingale.BorelCantelli
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 = -ω
h : Membership.mem (γ := Set ℝ) (Set.range fun (n : ℕ) ↦ f n ω_1) (-ω)
⊢ ω ≤ -c

Tactic:
refine le_neg.1 (hc _ ?_)

Premises used: le_neg, Iff.mp
-- Module: Mathlib.Probability.Martingale.BorelCantelli
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 = -ω
⊢ Membership.mem (γ := Set ℝ) (Set.range fun (n : ℕ) ↦ f n ω_1) (-ω)

Tactic:
simpa only [Set.mem_range]

Premises used: Set.mem_range
-- Module: Mathlib.Probability.Martingale.BorelCantelli
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ω : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω) ↔ BddBelow (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω)
htop : Tendsto (β := ℝ) (fun (n : ℕ) ↦ f n ω) atTop atTop
⊢ False

Tactic:
not_bddAbove_of_tendsto_atTop htop (hω.2 <| bddBelow_range_of_tendsto_atTop_atTop htop)

Premises used: Iff.mpr, Filter.not_bddAbove_of_tendsto_atTop, Filter.bddBelow_range_of_tendsto_atTop_atTop
-- Module: Mathlib.Probability.Martingale.BorelCantelli
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
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
h₂ :
  ∀ (ω : Ω) (hω : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω) ↔ BddBelow (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω))
    (htop : Tendsto (β := ℝ) (fun (n : ℕ) ↦ f n ω) atTop atTop), False
⊢ ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ f n ω) 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)

Premises used: MeasureTheory.Martingale.bddAbove_range_iff_bddBelow_range
-- Module: Mathlib.Probability.Martingale.BorelCantelli
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ω : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω) ↔ BddBelow (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω)
htop : Tendsto (β := ℝ) (fun (n : ℕ) ↦ f n ω) atTop atBot
⊢ False

Tactic:
not_bddBelow_of_tendsto_atBot htop (hω.1 <| bddAbove_range_of_tendsto_atTop_atBot htop)

Premises used: Filter.not_bddBelow_of_tendsto_atBot, Iff.mp, Filter.bddAbove_range_of_tendsto_atTop_atBot
-- Module: Mathlib.Probability.Martingale.BorelCantelli
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
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
h₂ :
  ∀ (ω : Ω) (hω : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω) ↔ BddBelow (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω))
    (htop : Tendsto (β := ℝ) (fun (n : ℕ) ↦ f n ω) atTop atBot), False
⊢ ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ f n ω) 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)

Premises used: MeasureTheory.Martingale.bddAbove_range_iff_bddBelow_range
-- Module: Mathlib.Probability.Martingale.BorelCantelli
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
rw₂ rw₃ : Eq.{u_2 + 1} (α := Ω → ℝ) 0 0
⊢ process s 0 = 0

Tactic:
rw [process, Finset.range_zero, Finset.sum_empty]

Premises used: Finset.sum_empty, MeasureTheory.BorelCantelli.process, Finset.range_zero
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
ℱ : Filtration ℕ m0
s : ℕ → Set Ω
hs : ∀ (n : ℕ), MeasurableSet (s n)
⊢ StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ (process s)

Tactic:
fun _ => Finset.stronglyMeasurable_sum _ fun _ hk =>
    stronglyMeasurable_one.indicator <| ℱ.mono (Finset.mem_range.1 hk) _ <| hs _

Premises used: MeasureTheory.stronglyMeasurable_one, Finset.stronglyMeasurable_sum, Finset.mem_range, Finset.range, MeasureTheory.StronglyAdapted, MeasureTheory.StronglyMeasurable.indicator, HAdd.hAdd, Iff.mp, MeasureTheory.Filtration.mono, OfNat.ofNat, MeasureTheory.BorelCantelli.process
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
ℱ : Filtration ℕ m0
μ : Measure Ω
s : ℕ → Set Ω
n : ℕ
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])
⊢ martingalePart (process s) ℱ μ n =
    ∑ 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]

Premises used: MeasureTheory.BorelCantelli.process_zero, zero_add, MeasureTheory.martingalePart_eq_sum