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 μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
hint : ∀ (n : ℕ), Integrable (f n) μ
hbdd_1 : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), |f (n + 1) ω - f n ω| ≤ (↑R : ℝ)
h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atTop
h₂ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atBot
h₃ : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), 0 ≤ μ[f (n + 1) - f n | (↑ℱ : ℕ → MeasurableSpace Ω) n] ω
ω : Ω
hω₂ : ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atBot
hω₃ : ∀ (n : ℕ), 0 ≤ μ[f (n + 1) - f n | (↑ℱ : ℕ → MeasurableSpace Ω) n] ω
hω₄ : ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
ht : Tendsto (β := ℝ) (fun (x : ℕ) ↦ -f x ω) atTop atBot
b : ℝ
hbdd : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ predictablePart f ℱ μ n ω)) b
hω₁ : ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ (f n + -predictablePart f ℱ μ n) ω) atTop atTop
⊢ False

Tactic:
hω₁ (tendsto_atTop_add_right_of_le _ (-b) (tendsto_neg_atBot_iff.1 ht) fun n =>
      neg_le_neg (hbdd ⟨n, rfl⟩))

Premises used: Filter.tendsto_atTop_add_right_of_le, Filter.tendsto_neg_atBot_iff, Exists.intro, Iff.mp, neg_le_neg, Neg.neg, rfl
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
hint : ∀ (n : ℕ), Integrable (f n) μ
hbdd_1 : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), |f (n + 1) ω - f n ω| ≤ (↑R : ℝ)
h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atTop
h₂ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atBot
h₃ : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), 0 ≤ μ[f (n + 1) - f n | (↑ℱ : ℕ → MeasurableSpace Ω) n] ω
ω : Ω
hω₂ : ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atBot
hω₃ : ∀ (n : ℕ), 0 ≤ μ[f (n + 1) - f n | (↑ℱ : ℕ → MeasurableSpace Ω) n] ω
hω₄ : ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
ht : Tendsto (β := ℝ) (fun (x : ℕ) ↦ -f x ω) atTop atBot
b : ℝ
hbdd : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ predictablePart f ℱ μ n ω)) b
hω₁ : ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ (f n + -predictablePart f ℱ μ n) ω) atTop atTop
⊢ False

Tactic:
exact hω₁ (tendsto_atTop_add_right_of_le _ (-b) (tendsto_neg_atBot_iff.1 ht) fun n =>
      neg_le_neg (hbdd ⟨n, rfl⟩))

Premises used: Filter.tendsto_atTop_add_right_of_le, Filter.tendsto_neg_atBot_iff, Exists.intro, Iff.mp, neg_le_neg, Neg.neg, rfl
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
hint : ∀ (n : ℕ), Integrable (f n) μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), |f (n + 1) ω - f n ω| ≤ (↑R : ℝ)
h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atTop
h₂ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atBot
h₃ : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), 0 ≤ μ[f (n + 1) - f n | (↑ℱ : ℕ → MeasurableSpace Ω) n] ω
ω : Ω
hω₁ : ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atTop
hω₂ : ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atBot
hω₃ : ∀ (n : ℕ), 0 ≤ μ[f (n + 1) - f n | (↑ℱ : ℕ → MeasurableSpace Ω) n] ω
hω₄ : ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
ht : Tendsto (β := ℝ) (fun (n : ℕ) ↦ predictablePart f ℱ μ n ω) atTop atTop
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ f n ω) atTop atTop

Tactic:
tendsto_atTop_atTop_of_monotone' (monotone_nat_of_le_succ hω₄) ?_

Premises used: Filter.tendsto_atTop_atTop_of_monotone', monotone_nat_of_le_succ
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
hint : ∀ (n : ℕ), Integrable (f n) μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), |f (n + 1) ω - f n ω| ≤ (↑R : ℝ)
h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atTop
h₂ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atBot
h₃ : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), 0 ≤ μ[f (n + 1) - f n | (↑ℱ : ℕ → MeasurableSpace Ω) n] ω
ω : Ω
hω₁ : ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atTop
hω₂ : ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atBot
hω₃ : ∀ (n : ℕ), 0 ≤ μ[f (n + 1) - f n | (↑ℱ : ℕ → MeasurableSpace Ω) n] ω
hω₄ : ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
ht : Tendsto (β := ℝ) (fun (n : ℕ) ↦ predictablePart f ℱ μ n ω) atTop atTop
h : ¬BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω)
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ f n ω) atTop atTop

Tactic:
refine tendsto_atTop_atTop_of_monotone' (monotone_nat_of_le_succ hω₄) ?_

Premises used: Filter.tendsto_atTop_atTop_of_monotone', monotone_nat_of_le_succ
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
hint : ∀ (n : ℕ), Integrable (f n) μ
hbdd_1 : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), |f (n + 1) ω - f n ω| ≤ (↑R : ℝ)
h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atTop
h₂ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atBot
h₃ : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), 0 ≤ μ[f (n + 1) - f n | (↑ℱ : ℕ → MeasurableSpace Ω) n] ω
ω : Ω
hω₁ : ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atTop
hω₂ : ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atBot
hω₃ : ∀ (n : ℕ), 0 ≤ μ[f (n + 1) - f n | (↑ℱ : ℕ → MeasurableSpace Ω) n] ω
hω₄ : ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
ht : Tendsto (β := ℝ) (fun (n : ℕ) ↦ predictablePart f ℱ μ n ω) atTop atTop
b : ℝ
hbdd : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ f n ω)) b
⊢ False

Tactic:
hω₂ ((tendsto_atBot_add_left_of_ge _ b fun n =>
      hbdd ⟨n, rfl⟩) <| tendsto_neg_atBot_iff.2 ht)

Premises used: Iff.mpr, Filter.tendsto_neg_atBot_iff, Exists.intro, Filter.tendsto_atBot_add_left_of_ge, rfl
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
hint : ∀ (n : ℕ), Integrable (f n) μ
hbdd_1 : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), |f (n + 1) ω - f n ω| ≤ (↑R : ℝ)
h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atTop
h₂ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atBot
h₃ : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), 0 ≤ μ[f (n + 1) - f n | (↑ℱ : ℕ → MeasurableSpace Ω) n] ω
ω : Ω
hω₁ : ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atTop
hω₂ : ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ martingalePart f ℱ μ n ω) atTop atBot
hω₃ : ∀ (n : ℕ), 0 ≤ μ[f (n + 1) - f n | (↑ℱ : ℕ → MeasurableSpace Ω) n] ω
hω₄ : ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
ht : Tendsto (β := ℝ) (fun (n : ℕ) ↦ predictablePart f ℱ μ n ω) atTop atTop
b : ℝ
hbdd : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ f n ω)) b
⊢ False

Tactic:
exact hω₂ ((tendsto_atBot_add_left_of_ge _ b fun n =>
      hbdd ⟨n, rfl⟩) <| tendsto_neg_atBot_iff.2 ht)

Premises used: Iff.mpr, Filter.tendsto_neg_atBot_iff, Exists.intro, Filter.tendsto_atBot_add_left_of_ge, rfl
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
s : ℕ → Set Ω
hs : ∀ (n : ℕ), MeasurableSet (s n)
refine_2 :
  ∀
    (this :
      ∀ᵐ (ω : Ω) ∂μ,
        Tendsto (β := ℝ) (fun (n : ℕ) ↦ process s n ω) atTop atTop ↔
          Tendsto (β := ℝ) (fun (n : ℕ) ↦ predictablePart (process s) ℱ μ n ω) atTop atTop),
    ∀ᵐ (ω : Ω) ∂μ,
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, (s (k + 1)).indicator 1 ω) atTop atTop ↔
        Tendsto (β := ℝ)
          (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, μ[(s (k + 1)).indicator 1 | (↑ℱ : ℕ → MeasurableSpace Ω) k] ω) atTop
          atTop
refine_1 : ∀ (ω : Ω) (n : ℕ), process s n ω ≤ process s (n + 1) ω
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, (s (k + 1)).indicator 1 ω) atTop atTop ↔
      Tendsto (β := ℝ)
        (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, μ[(s (k + 1)).indicator 1 | (↑ℱ : ℕ → MeasurableSpace Ω) k] ω) atTop atTop

Tactic:
have := tendsto_sum_indicator_atTop_iff (Eventually.of_forall fun ω n => ?_)
    (stronglyAdapted_process hs) (integrable_process μ hs)
    (Eventually.of_forall <| process_difference_le s)
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
s : ℕ → Set Ω
hs : ∀ (n : ℕ), MeasurableSet (s n)
ω : Ω
n : ℕ
refine_1 : LE.le (α := ℝ) 0 ((s (n + 1)).indicator 1 ω)
⊢ process s n ω ≤ process s (n + 1) ω

Tactic:
rw [process, process, ← sub_nonneg, Finset.sum_apply, Finset.sum_apply,
      Finset.sum_range_succ_sub_sum]

Premises used: Finset.sum_apply, Finset.sum_range_succ_sub_sum, sub_nonneg, MeasureTheory.BorelCantelli.process
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
s : ℕ → Set Ω
hs : ∀ (n : ℕ), MeasurableSet (s n)
ω : Ω
n : ℕ
⊢ LE.le (α := ℝ) 0 ((s (n + 1)).indicator 1 ω)

Tactic:
Set.indicator_nonneg (fun _ _ => zero_le_one) _

Premises used: zero_le_one, Set.indicator_nonneg
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
s : ℕ → Set Ω
hs : ∀ (n : ℕ), MeasurableSet (s n)
ω : Ω
n : ℕ
⊢ LE.le (α := ℝ) 0 ((s (n + 1)).indicator 1 ω)

Tactic:
exact Set.indicator_nonneg (fun _ _ => zero_le_one) _

Premises used: zero_le_one, Set.indicator_nonneg
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
s : ℕ → Set Ω
hs : ∀ (n : ℕ), MeasurableSet (s n)
this :
  ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ process s n ω) atTop atTop ↔
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ predictablePart (process s) ℱ μ n ω) atTop atTop
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ (∑ k ∈ Finset.range n, (s (k + 1)).indicator 1) ω) atTop atTop ↔
      Tendsto (β := ℝ)
        (fun (n : ℕ) ↦ (∑ k ∈ Finset.range n, μ[(s (k + 1)).indicator 1 | (↑ℱ : ℕ → MeasurableSpace Ω) k]) ω) atTop
        atTop

Tactic:
simp_rw [process, predictablePart_process_ae_eq] at this

Premises used: MeasureTheory.BorelCantelli.predictablePart_process_ae_eq, MeasureTheory.BorelCantelli.process
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
s : ℕ → Set Ω
hs : ∀ (n : ℕ), MeasurableSet (s n)
this :
  ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ (∑ k ∈ Finset.range n, (s (k + 1)).indicator 1) ω) atTop atTop ↔
      Tendsto (β := ℝ)
        (fun (n : ℕ) ↦ (∑ k ∈ Finset.range n, μ[(s (k + 1)).indicator 1 | (↑ℱ : ℕ → MeasurableSpace Ω) k]) ω) atTop
        atTop
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, (s (k + 1)).indicator 1 ω) atTop atTop ↔
      Tendsto (β := ℝ)
        (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, μ[(s (k + 1)).indicator 1 | (↑ℱ : ℕ → MeasurableSpace Ω) k] ω) atTop atTop

Tactic:
simpa using this
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
ℱ : Filtration ℕ m0
μ : Measure Ω
inst : IsFiniteMeasure μ
s : ℕ → Set Ω
hs : ∀ (n : ℕ), MeasurableSet (s n)
rw :
  ∀ᵐ (ω : Ω) ∂μ,
    Membership.mem (γ := Set Ω)
        {ω : Ω |
          Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, (s (k + 1)).indicator (fun (x : Ω) ↦ 1) ω) atTop atTop}
        ω ↔
      Tendsto (β := ℝ)
        (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, μ[(s (k + 1)).indicator 1 | (↑ℱ : ℕ → MeasurableSpace Ω) k] ω) atTop atTop
⊢ ∀ᵐ (ω : Ω) ∂μ,
    ω ∈ limsup s atTop ↔
      Tendsto (β := ℝ)
        (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, μ[(s (k + 1)).indicator 1 | (↑ℱ : ℕ → MeasurableSpace Ω) k] ω) atTop atTop

Tactic:
rw [← limsup_nat_add s 1,
    Set.limsup_eq_tendsto_sum_indicator_atTop (zero_lt_one (α := ℝ)) (fun n ↦ s (n + 1))]

Premises used: Filter.limsup_nat_add, Set.limsup_eq_tendsto_sum_indicator_atTop, zero_lt_one, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
ℱ : Filtration ℕ m0
μ : Measure Ω
inst : IsFiniteMeasure μ
s : ℕ → Set Ω
hs : ∀ (n : ℕ), MeasurableSet (s n)
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Membership.mem (γ := Set Ω)
        {ω : Ω |
          Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, (s (k + 1)).indicator (fun (x : Ω) ↦ 1) ω) atTop atTop}
        ω ↔
      Tendsto (β := ℝ)
        (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, μ[(s (k + 1)).indicator 1 | (↑ℱ : ℕ → MeasurableSpace Ω) k] ω) atTop atTop

Tactic:
tendsto_sum_indicator_atTop_iff' hs

Premises used: Set.Mem, setOf, MeasureTheory.tendsto_sum_indicator_atTop_iff', Filter.Tendsto
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
ℱ : Filtration ℕ m0
μ : Measure Ω
inst : IsFiniteMeasure μ
s : ℕ → Set Ω
hs : ∀ (n : ℕ), MeasurableSet (s n)
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Membership.mem (γ := Set Ω)
        {ω : Ω |
          Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, (s (k + 1)).indicator (fun (x : Ω) ↦ 1) ω) atTop atTop}
        ω ↔
      Tendsto (β := ℝ)
        (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, μ[(s (k + 1)).indicator 1 | (↑ℱ : ℕ → MeasurableSpace Ω) k] ω) atTop atTop

Tactic:
exact tendsto_sum_indicator_atTop_iff' hs

Premises used: MeasureTheory.tendsto_sum_indicator_atTop_iff'
-- Module: Mathlib.Probability.Martingale.Centering
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
simp_rw : Eq (α := Ω → E) (∑ i ∈ Finset.range 0, μ[f (i + 1) - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i]) 0
simp_rw₁ : Eq (α := Ω → E) (∑ i ∈ ∅, μ[f (i + 1) - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i]) 0
⊢ predictablePart f ℱ μ 0 = 0

Tactic:
simp_rw [predictablePart, Finset.range_zero, Finset.sum_empty]

Premises used: MeasureTheory.predictablePart, Finset.sum_empty, Finset.range_zero
-- Module: Mathlib.Probability.Martingale.Centering
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
n : ℕ
⊢ predictablePart f ℱ μ (n + 1) = predictablePart f ℱ μ n + μ[f (n + 1) - f n | (↑ℱ : ℕ → MeasurableSpace Ω) n]

Tactic:
simp [predictablePart, Finset.sum_range_add]

Premises used: Finset.sum_range_add, MeasureTheory.predictablePart
-- Module: Mathlib.Probability.Martingale.Centering
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst_2 : CompleteSpace E
c : ℝ
n : ℕ
simp :
  EventuallyEq.{u_1, u_2} (β := E) (ae μ)
    (∑ i ∈ Finset.range n, μ[(c • f) (i + 1) - (c • f) i | (↑ℱ : ℕ → MeasurableSpace Ω) i])
    (∑ x ∈ Finset.range n, c • μ[f (x + 1) - f x | (↑ℱ : ℕ → MeasurableSpace Ω) x])
⊢ predictablePart (c • f) ℱ μ n =ᶠ[ae μ] c • predictablePart f ℱ μ n

Tactic:
simp only [predictablePart, Finset.smul_sum]

Premises used: MeasureTheory.predictablePart, Finset.smul_sum
-- Module: Mathlib.Probability.Martingale.Centering
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst_2 : CompleteSpace E
c : ℝ
n : ℕ
⊢ EventuallyEq.{u_1, u_2} (β := E) (ae μ)
    (∑ i ∈ Finset.range n, μ[(c • f) (i + 1) - (c • f) i | (↑ℱ : ℕ → MeasurableSpace Ω) i])
    (∑ x ∈ Finset.range n, c • μ[f (x + 1) - f x | (↑ℱ : ℕ → MeasurableSpace Ω) x])

Tactic:
eventuallyEq_sum fun i hi => ?_

Premises used: eventuallyEq_sum
-- Module: Mathlib.Probability.Martingale.Centering
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst_2 : CompleteSpace E
c : ℝ
n : ℕ
refine :
  ∀ (i : ℕ) (hi : i ∈ Finset.range n),
    μ[(c • f) (i + 1) - (c • f) i | (↑ℱ : ℕ → MeasurableSpace Ω) i] =ᶠ[ae μ]
      c • μ[f (i + 1) - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i]
⊢ EventuallyEq.{u_1, u_2} (β := E) (ae μ)
    (∑ i ∈ Finset.range n, μ[(c • f) (i + 1) - (c • f) i | (↑ℱ : ℕ → MeasurableSpace Ω) i])
    (∑ x ∈ Finset.range n, c • μ[f (x + 1) - f x | (↑ℱ : ℕ → MeasurableSpace Ω) x])

Tactic:
refine eventuallyEq_sum fun i hi => ?_

Premises used: eventuallyEq_sum
-- Module: Mathlib.Probability.Martingale.Centering
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst_2 : CompleteSpace E
c : ℝ
n i : ℕ
hi : i ∈ Finset.range n
⊢ μ[(c • f) (i + 1) - (c • f) i | (↑ℱ : ℕ → MeasurableSpace Ω) i] =ᶠ[ae μ]
    c • μ[f (i + 1) - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i]

Tactic:
simp [← smul_sub, condExp_smul]

Premises used: MeasureTheory.condExp_smul, smul_sub
-- Module: Mathlib.Probability.Martingale.Centering
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst_2 : CompleteSpace E
hfint : ∀ (n : ℕ), Integrable (f n) μ
hgint : ∀ (n : ℕ), Integrable (g n) μ
n : ℕ
simp :
  EventuallyEq.{u_1, u_2} (β := E) (ae μ)
    (∑ i ∈ Finset.range n, μ[(f + g) (i + 1) - (f + g) i | (↑ℱ : ℕ → MeasurableSpace Ω) i])
    (∑ x ∈ Finset.range n,
      (μ[f (x + 1) - f x | (↑ℱ : ℕ → MeasurableSpace Ω) x] + μ[g (x + 1) - g x | (↑ℱ : ℕ → MeasurableSpace Ω) x]))
⊢ predictablePart (f + g) ℱ μ n =ᶠ[ae μ] predictablePart f ℱ μ n + predictablePart g ℱ μ n

Tactic:
simp only [predictablePart, ← Finset.sum_add_distrib]

Premises used: Finset.sum_add_distrib, MeasureTheory.predictablePart
-- Module: Mathlib.Probability.Martingale.Centering
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst_2 : CompleteSpace E
hfint : ∀ (n : ℕ), Integrable (f n) μ
hgint : ∀ (n : ℕ), Integrable (g n) μ
n : ℕ
⊢ EventuallyEq.{u_1, u_2} (β := E) (ae μ)
    (∑ i ∈ Finset.range n, μ[(f + g) (i + 1) - (f + g) i | (↑ℱ : ℕ → MeasurableSpace Ω) i])
    (∑ x ∈ Finset.range n,
      (μ[f (x + 1) - f x | (↑ℱ : ℕ → MeasurableSpace Ω) x] + μ[g (x + 1) - g x | (↑ℱ : ℕ → MeasurableSpace Ω) x]))

Tactic:
eventuallyEq_sum fun i hi => ?_

Premises used: eventuallyEq_sum
-- Module: Mathlib.Probability.Martingale.Centering
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst_2 : CompleteSpace E
hfint : ∀ (n : ℕ), Integrable (f n) μ
hgint : ∀ (n : ℕ), Integrable (g n) μ
n : ℕ
refine :
  ∀ (i : ℕ) (hi : i ∈ Finset.range n),
    μ[(f + g) (i + 1) - (f + g) i | (↑ℱ : ℕ → MeasurableSpace Ω) i] =ᶠ[ae μ]
      μ[f (i + 1) - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i] + μ[g (i + 1) - g i | (↑ℱ : ℕ → MeasurableSpace Ω) i]
⊢ EventuallyEq.{u_1, u_2} (β := E) (ae μ)
    (∑ i ∈ Finset.range n, μ[(f + g) (i + 1) - (f + g) i | (↑ℱ : ℕ → MeasurableSpace Ω) i])
    (∑ x ∈ Finset.range n,
      (μ[f (x + 1) - f x | (↑ℱ : ℕ → MeasurableSpace Ω) x] + μ[g (x + 1) - g x | (↑ℱ : ℕ → MeasurableSpace Ω) x]))

Tactic:
refine eventuallyEq_sum fun i hi => ?_

Premises used: eventuallyEq_sum
-- Module: Mathlib.Probability.Martingale.Centering
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst_2 : CompleteSpace E
hfint : ∀ (n : ℕ), Integrable (f n) μ
hgint : ∀ (n : ℕ), Integrable (g n) μ
n i : ℕ
hi : i ∈ Finset.range n
simp :
  μ[f (i + 1) + g (i + 1) - (f i + g i) | (↑ℱ : ℕ → MeasurableSpace Ω) i] =ᶠ[ae μ]
    μ[f (i + 1) - f i + (g (i + 1) - g i) | (↑ℱ : ℕ → MeasurableSpace Ω) i]
⊢ μ[(f + g) (i + 1) - (f + g) i | (↑ℱ : ℕ → MeasurableSpace Ω) i] =ᶠ[ae μ]
    μ[f (i + 1) - f i + (g (i + 1) - g i) | (↑ℱ : ℕ → MeasurableSpace Ω) i]

Tactic:
simp
-- Module: Mathlib.Probability.Martingale.Centering
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst_2 : CompleteSpace E
hfint : ∀ (n : ℕ), Integrable (f n) μ
hgint : ∀ (n : ℕ), Integrable (g n) μ
n i : ℕ
hi : i ∈ Finset.range n
abel_nf :
  μ[f (i + 1) + (g (i + 1) + (HSMul.hSMul (α := ℤ) (-1) (f i) + HSMul.hSMul (α := ℤ) (-1) (g i))) |
      (↑ℱ : ℕ → MeasurableSpace Ω) i] =ᶠ[ae μ]
    μ[f (i + 1) + (g (i + 1) + (HSMul.hSMul (α := ℤ) (-1) (f i) + HSMul.hSMul (α := ℤ) (-1) (g i))) |
      (↑ℱ : ℕ → MeasurableSpace Ω) i]
⊢ μ[f (i + 1) + g (i + 1) - (f i + g i) | (↑ℱ : ℕ → MeasurableSpace Ω) i] =ᶠ[ae μ]
    μ[f (i + 1) - f i + (g (i + 1) - g i) | (↑ℱ : ℕ → MeasurableSpace Ω) i]

Tactic:
abel_nf
-- Module: Mathlib.Probability.Martingale.Centering
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst_2 : CompleteSpace E
hfint : ∀ (n : ℕ), Integrable (f n) μ
hgint : ∀ (n : ℕ), Integrable (g n) μ
n i : ℕ
hi : i ∈ Finset.range n
⊢ μ[f (i + 1) + (g (i + 1) + (HSMul.hSMul (α := ℤ) (-1) (f i) + HSMul.hSMul (α := ℤ) (-1) (g i))) |
      (↑ℱ : ℕ → MeasurableSpace Ω) i] =ᶠ[ae μ]
    μ[f (i + 1) + (g (i + 1) + (HSMul.hSMul (α := ℤ) (-1) (f i) + HSMul.hSMul (α := ℤ) (-1) (g i))) |
      (↑ℱ : ℕ → MeasurableSpace Ω) i]

Tactic:
rfl
-- Module: Mathlib.Probability.Martingale.Centering
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst_2 : CompleteSpace E
hfint : ∀ (n : ℕ), Integrable (f n) μ
hgint : ∀ (n : ℕ), Integrable (g n) μ
n i : ℕ
hi : i ∈ Finset.range n
⊢ μ[f (i + 1) - f i + (g (i + 1) - g i) | (↑ℱ : ℕ → MeasurableSpace Ω) i] =ᶠ[ae μ]
    μ[f (i + 1) - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i] + μ[g (i + 1) - g i | (↑ℱ : ℕ → MeasurableSpace Ω) i]

Tactic:
apply condExp_add ((hfint (i + 1)).sub (hfint i)) ((hgint (i + 1)).sub (hgint i))

Premises used: MeasureTheory.Integrable.sub, MeasureTheory.condExp_add, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Probability.Martingale.Centering
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst_2 : CompleteSpace E
hfint : ∀ (n : ℕ), Integrable (f n) μ
hgint : ∀ (n : ℕ), Integrable (g n) μ
n i : ℕ
hi : i ∈ Finset.range n
_ :
  μ[(f + g) (i + 1) - (f + g) i | (↑ℱ : ℕ → MeasurableSpace Ω) i] =ᶠ[ae μ]
    μ[f (i + 1) - f i + (g (i + 1) - g i) | (↑ℱ : ℕ → MeasurableSpace Ω) i]
_₁ :
  μ[f (i + 1) - f i + (g (i + 1) - g i) | (↑ℱ : ℕ → MeasurableSpace Ω) i] =ᶠ[ae μ]
    μ[f (i + 1) - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i] + μ[g (i + 1) - g i | (↑ℱ : ℕ → MeasurableSpace Ω) i]
⊢ μ[(f + g) (i + 1) - (f + g) i | (↑ℱ : ℕ → MeasurableSpace Ω) i] =ᶠ[ae μ]
    μ[f (i + 1) - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i] + μ[g (i + 1) - g i | (↑ℱ : ℕ → MeasurableSpace Ω) i]

Tactic:
calc
  _ =ᵐ[μ] μ[(f (i + 1) - f i) + (g (i + 1) - g i) | ℱ i] := by simp; abel_nf; rfl
  _ =ᵐ[μ] _ := by apply condExp_add ((hfint (i + 1)).sub (hfint i)) ((hgint (i + 1)).sub (hgint i))

Premises used: MeasureTheory.Filtration.seq, HSub.hSub, HAdd.hAdd, OfNat.ofNat