awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h : (∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i
hp_pos : 0 < p
h_integral : ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ < ∞
⊢ ∀ᵐ (x : α) ∂μ, HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) x - f i x‖ₑ) p < ∞

Tactic:
have rpow_ae_lt_top : ∀ᵐ x ∂μ, (∑' i, ‖f (i + 1) x - f i x‖ₑ) ^ p < ∞ := by
    refine ae_lt_top' (AEMeasurable.pow_const ?_ _) h_integral.ne
    exact AEMeasurable.tsum fun n => ((hf (n + 1)).sub (hf n)).enorm
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h : (∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i
hp_pos : 0 < p
h_integral : ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ < ∞
rpow_ae_lt_top : ∀ᵐ (x : α) ∂μ, HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) x - f i x‖ₑ) p < ∞
⊢ ∀ᵐ (x : α) ∂μ, LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) x - f i x‖ₑ) ∞

Tactic:
rpow_ae_lt_top.mono fun x hx => ?_

Premises used: Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h : (∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i
hp_pos : 0 < p
h_integral : ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ < ∞
rpow_ae_lt_top : ∀ᵐ (x : α) ∂μ, HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) x - f i x‖ₑ) p < ∞
refine :
  ∀ (x : α) (hx : HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) x - f i x‖ₑ) p < ∞),
    LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) x - f i x‖ₑ) ∞
⊢ ∀ᵐ (x : α) ∂μ, LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) x - f i x‖ₑ) ∞

Tactic:
refine rpow_ae_lt_top.mono fun x hx => ?_

Premises used: Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h : (∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i
hp_pos : 0 < p
h_integral : ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ < ∞
rpow_ae_lt_top : ∀ᵐ (x : α) ∂μ, HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) x - f i x‖ₑ) p < ∞
x : α
hx : ∑' (i : ℕ), ‖f (i + 1) x - f i x‖ₑ < HPow.hPow (α := ℝ≥0∞) ∞ p⁻¹
⊢ 0 < p⁻¹

Tactic:
simp [hp_pos]
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h : (∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i
hp_pos : 0 < p
h_integral : ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ < ∞
rpow_ae_lt_top : ∀ᵐ (x : α) ∂μ, HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) x - f i x‖ₑ) p < ∞
x : α
hx : HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) x - f i x‖ₑ) p < ∞
rwa :
  ∀ (hx : ∑' (i : ℕ), ‖f (i + 1) x - f i x‖ₑ < HPow.hPow (α := ℝ≥0∞) ∞ p⁻¹),
    LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) x - f i x‖ₑ) ∞
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (hx : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) x - f i x‖ₑ) ∞),
    LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) x - f i x‖ₑ) ∞
⊢ LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) x - f i x‖ₑ) ∞

Tactic:
rwa [← ENNReal.lt_rpow_inv_iff hp_pos,
    ENNReal.top_rpow_of_pos (by simp [hp_pos] : 0 < p⁻¹)] at hx

Premises used: ENNReal.lt_rpow_inv_iff, ENNReal.top_rpow_of_pos
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
f : ℕ → α → E
p : ℝ
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm' (f n - f m_1) p μ < B N
⊢ ∀ (n : ℕ), eLpNorm' (ε := ℝ) (fun (x : α) ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖) p μ ≤ ∑' (i : ℕ), B i

Tactic:
have h1 :
      ∀ n, eLpNorm' (fun x => ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖) p μ ≤ ∑' i, B i :=
      eLpNorm'_sum_norm_sub_le_tsum_of_cauchy_eLpNorm' hf hp1 h_cau
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
f : ℕ → α → E
p : ℝ
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm' (f n - f m_1) p μ < B N
h1 :
  ∀ (n : ℕ), eLpNorm' (ε := ℝ) (fun (x : α) ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖) p μ ≤ ∑' (i : ℕ), B i
⊢ ∀ (n : ℕ),
    ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p ∂μ ≤
      HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p

Tactic:
have h2 n :
        ∫⁻ a, (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ ≤ (∑' i, B i) ^ p :=
      lintegral_rpow_sum_enorm_sub_le_rpow_tsum hp1 n (h1 n)
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
f : ℕ → α → E
p : ℝ
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm' (f n - f m_1) p μ < B N
h1 :
  ∀ (n : ℕ), eLpNorm' (ε := ℝ) (fun (x : α) ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖) p μ ≤ ∑' (i : ℕ), B i
h2 :
  ∀ (n : ℕ),
    ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p ∂μ ≤
      HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p
⊢ (∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i

Tactic:
have h3 : (∫⁻ a, (∑' i, ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ) ^ (1 / p) ≤ ∑' i, B i :=
      lintegral_rpow_tsum_coe_enorm_sub_le_tsum hf hp1 h2
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
f : ℕ → α → E
p : ℝ
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm' (f n - f m_1) p μ < B N
h1 :
  ∀ (n : ℕ), eLpNorm' (ε := ℝ) (fun (x : α) ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖) p μ ≤ ∑' (i : ℕ), B i
h2 :
  ∀ (n : ℕ),
    ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p ∂μ ≤
      HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p
h3 : (∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i
⊢ ∀ᵐ (x : α) ∂μ, LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) x - f i x‖ₑ) ∞

Tactic:
have h4 : ∀ᵐ x ∂μ, ∑' i, ‖f (i + 1) x - f i x‖ₑ < ∞ :=
      tsum_enorm_sub_ae_lt_top hf hp1 hB h3
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
f : ℕ → α → E
p : ℝ
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm' (f n - f m_1) p μ < B N
h1 :
  ∀ (n : ℕ), eLpNorm' (ε := ℝ) (fun (x : α) ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖) p μ ≤ ∑' (i : ℕ), B i
h2 :
  ∀ (n : ℕ),
    ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p ∂μ ≤
      HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p
h3 : (∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i
h4 : ∀ᵐ (x : α) ∂μ, LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) x - f i x‖ₑ) ∞
⊢ ∀ᵐ (x : α) ∂μ, Summable.{u_3, 0} (α := E) fun (i : ℕ) ↦ f (i + 1) x - f i x

Tactic:
h4.mono fun x hx => .of_nnnorm <| ENNReal.tsum_coe_ne_top_iff_summable.mp hx.ne

Premises used: Summable.of_nnnorm, Filter.Eventually.mono, ENNReal.tsum_coe_ne_top_iff_summable, Iff.mp, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
f : ℕ → α → E
p : ℝ
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm' (f n - f m_1) p μ < B N
h1 :
  ∀ (n : ℕ), eLpNorm' (ε := ℝ) (fun (x : α) ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖) p μ ≤ ∑' (i : ℕ), B i
h2 :
  ∀ (n : ℕ),
    ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p ∂μ ≤
      HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p
h3 : (∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i
h4 : ∀ᵐ (x : α) ∂μ, LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) x - f i x‖ₑ) ∞
⊢ ∀ᵐ (x : α) ∂μ, Summable.{u_3, 0} (α := E) fun (i : ℕ) ↦ f (i + 1) x - f i x

Tactic:
exact h4.mono fun x hx => .of_nnnorm <| ENNReal.tsum_coe_ne_top_iff_summable.mp hx.ne

Premises used: Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
f : ℕ → α → E
p : ℝ
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm' (f n - f m_1) p μ < B N
⊢ ∀ᵐ (x : α) ∂μ, Summable.{u_3, 0} (α := E) fun (i : ℕ) ↦ f (i + 1) x - f i x

Tactic:
have h_summable : ∀ᵐ x ∂μ, Summable fun i : ℕ => f (i + 1) x - f i x := by
    have h1 :
      ∀ n, eLpNorm' (fun x => ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖) p μ ≤ ∑' i, B i :=
      eLpNorm'_sum_norm_sub_le_tsum_of_cauchy_eLpNorm' hf hp1 h_cau
    have h2 n :
        ∫⁻ a, (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ ≤ (∑' i, B i) ^ p :=
      lintegral_rpow_sum_enorm_sub_le_rpow_tsum hp1 n (h1 n)
    have h3 : (∫⁻ a, (∑' i, ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ) ^ (1 / p) ≤ ∑' i, B i :=
      lintegral_rpow_tsum_coe_enorm_sub_le_tsum hf hp1 h2
    have h4 : ∀ᵐ x ∂μ, ∑' i, ‖f (i + 1) x - f i x‖ₑ < ∞ :=
      tsum_enorm_sub_ae_lt_top hf hp1 hB h3
    exact h4.mono fun x hx => .of_nnnorm <| ENNReal.tsum_coe_ne_top_iff_summable.mp hx.ne
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
f : ℕ → α → E
p : ℝ
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm' (f n - f m_1) p μ < B N
h_summable : ∀ᵐ (x : α) ∂μ, Summable.{u_3, 0} (α := E) fun (i : ℕ) ↦ f (i + 1) x - f i x
⊢ ∀ᵐ (x : α) ∂μ, ∃ (l : E), Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 l)

Tactic:
h_summable.mono fun x hx ↦ ?_

Premises used: Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
f : ℕ → α → E
p : ℝ
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm' (f n - f m_1) p μ < B N
h_summable : ∀ᵐ (x : α) ∂μ, Summable.{u_3, 0} (α := E) fun (i : ℕ) ↦ f (i + 1) x - f i x
refine :
  ∀ (x : α) (hx : Summable.{u_3, 0} (α := E) fun (i : ℕ) ↦ f (i + 1) x - f i x),
    ∃ (l : E), Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 l)
⊢ ∀ᵐ (x : α) ∂μ, ∃ (l : E), Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 l)

Tactic:
refine h_summable.mono fun x hx ↦ ?_

Premises used: Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
f : ℕ → α → E
p : ℝ
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm' (f n - f m_1) p μ < B N
h_summable : ∀ᵐ (x : α) ∂μ, Summable.{u_3, 0} (α := E) fun (i : ℕ) ↦ f (i + 1) x - f i x
x : α
hx : Summable.{u_3, 0} (α := E) fun (i : ℕ) ↦ f (i + 1) x - f i x
⊢ Tendsto.{0, u_3} (β := E) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, (f (i + 1) x - f i x)) atTop
    (𝓝 (∑' (b : ℕ), (f (b + 1) x - f b x)))

Tactic:
have hx_sum := hx.hasSum.tendsto_sum_nat
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
f : ℕ → α → E
p : ℝ
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm' (f n - f m_1) p μ < B N
h_summable : ∀ᵐ (x : α) ∂μ, Summable.{u_3, 0} (α := E) fun (i : ℕ) ↦ f (i + 1) x - f i x
x : α
hx : Summable.{u_3, 0} (α := E) fun (i : ℕ) ↦ f (i + 1) x - f i x
hx_sum :
  Tendsto.{0, u_3} (β := E) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, (f (i + 1) x - f i x)) atTop
    (𝓝 (∑' (b : ℕ), (f (b + 1) x - f b x)))
⊢ Tendsto.{0, u_3} (β := E) (fun (n : ℕ) ↦ f n x - f 0 x) atTop (𝓝 (∑' (b : ℕ), (f (b + 1) x - f b x)))

Tactic:
rw [funext fun n ↦ Finset.sum_range_sub (fun m ↦ f m x) n] at hx_sum

Premises used: funext, Finset.sum_range_sub
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
f : ℕ → α → E
p : ℝ
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm' (f n - f m_1) p μ < B N
h_summable : ∀ᵐ (x : α) ∂μ, Summable.{u_3, 0} (α := E) fun (i : ℕ) ↦ f (i + 1) x - f i x
x : α
hx : Summable.{u_3, 0} (α := E) fun (i : ℕ) ↦ f (i + 1) x - f i x
hx_sum : Tendsto.{0, u_3} (β := E) (fun (n : ℕ) ↦ f n x - f 0 x) atTop (𝓝 (∑' (b : ℕ), (f (b + 1) x - f b x)))
⊢ Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (∑' (i : ℕ), (f (i + 1) x - f i x) + f 0 x))

Tactic:
simpa using hx_sum.add_const (f 0 x)

Premises used: Filter.Tendsto.add_const, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
f : ℕ → α → E
p : ℝ
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm' (f n - f m_1) p μ < B N
h_summable : ∀ᵐ (x : α) ∂μ, Summable.{u_3, 0} (α := E) fun (i : ℕ) ↦ f (i + 1) x - f i x
x : α
hx : Summable.{u_3, 0} (α := E) fun (i : ℕ) ↦ f (i + 1) x - f i x
hx_sum : Tendsto.{0, u_3} (β := E) (fun (n : ℕ) ↦ f n x - f 0 x) atTop (𝓝 (∑' (b : ℕ), (f (b + 1) x - f b x)))
⊢ ∃ (l : E), Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 l)

Tactic:
exact ⟨∑' i, (f (i + 1) x - f i x) + f 0 x, by simpa using hx_sum.add_const (f 0 x)⟩
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N
pos : ∀ (hp_top : p = ∞), ∀ᵐ (x : α) ∂μ, ∃ (l : E), Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 l)
neg : ∀ (hp_top : ¬p = ∞), ∀ᵐ (x : α) ∂μ, ∃ (l : E), Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 l)
⊢ ∀ᵐ (x : α) ∂μ, ∃ (l : E), Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 l)

Tactic:
by_cases hp_top : p = ∞
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N
hp_top : p = ∞
⊢ LE.le (α := ℝ≥0∞) 1 ∞

Tactic:
simp_rw [hp_top] at *
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N
hp_top : p = ∞
hp₁ : LE.le (α := ℝ≥0∞) 1 ∞
⊢ ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) ∞ μ < B N

Tactic:
simp_rw [hp_top] at *
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N
hp_top : p = ∞
hp₁ : LE.le (α := ℝ≥0∞) 1 ∞
h_cau₁ : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) ∞ μ < B N
⊢ True

Tactic:
simp_rw [hp_top] at *
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
hp : LE.le (α := ℝ≥0∞) 1 ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) ∞ μ < B N
hp_top : True
simp_rw : ∀ (i i_1 i_2 : ℕ) (i_3 : i ≤ i_1) (i_4 : i ≤ i_2), ∀ᵐ (a : α) ∂μ, ‖(f i_1 - f i_2) a‖ₑ < B i
⊢ ∀ᵐ (x : α) ∂μ, ∀ (N n m : ℕ), N ≤ n → N ≤ m → ‖(f n - f m) x‖ₑ < B N

Tactic:
simp_rw [ae_all_iff]

Premises used: MeasureTheory.ae_all_iff
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
hp : LE.le (α := ℝ≥0∞) 1 ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) ∞ μ < B N
hp_top : True
⊢ ∀ (i i_1 i_2 : ℕ) (i_3 : i ≤ i_1) (i_4 : i ≤ i_2), ∀ᵐ (a : α) ∂μ, ‖(f i_1 - f i_2) a‖ₑ < B i

Tactic:
fun N n m hnN hmN => ae_lt_of_essSup_lt (h_cau N n m hnN hmN)

Premises used: ae_lt_of_essSup_lt
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
hp : LE.le (α := ℝ≥0∞) 1 ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) ∞ μ < B N
hp_top : True
⊢ ∀ (i i_1 i_2 : ℕ) (i_3 : i ≤ i_1) (i_4 : i ≤ i_2), ∀ᵐ (a : α) ∂μ, ‖(f i_1 - f i_2) a‖ₑ < B i

Tactic:
exact fun N n m hnN hmN => ae_lt_of_essSup_lt (h_cau N n m hnN hmN)

Premises used: ae_lt_of_essSup_lt
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
hp : LE.le (α := ℝ≥0∞) 1 ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) ∞ μ < B N
hp_top : True
⊢ ∀ᵐ (x : α) ∂μ, ∀ (N n m : ℕ), N ≤ n → N ≤ m → ‖(f n - f m) x‖ₑ < B N

Tactic:
have h_cau_ae : ∀ᵐ x ∂μ, ∀ N n m, N ≤ n → N ≤ m → ‖(f n - f m) x‖ₑ < B N := by
      simp_rw [ae_all_iff]
      exact fun N n m hnN hmN => ae_lt_of_essSup_lt (h_cau N n m hnN hmN)
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
hp : LE.le (α := ℝ≥0∞) 1 ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) ∞ μ < B N
hp_top : True
h_cau_ae : ∀ᵐ (x : α) ∂μ, ∀ (N n m : ℕ), N ≤ n → N ≤ m → ‖(f n - f m) x‖ₑ < B N
⊢ ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → essSup (fun (x : α) ↦ ‖(f n - f m_1) x‖ₑ) μ < B N

Tactic:
simp_rw [eLpNorm_exponent_top, eLpNormEssSup] at h_cau

Premises used: MeasureTheory.eLpNorm_exponent_top, MeasureTheory.eLpNormEssSup
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
hp : LE.le (α := ℝ≥0∞) 1 ∞
hp_top : True
h_cau_ae : ∀ᵐ (x : α) ∂μ, ∀ (N n m : ℕ), N ≤ n → N ≤ m → ‖(f n - f m) x‖ₑ < B N
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → essSup (fun (x : α) ↦ ‖(f n - f m_1) x‖ₑ) μ < B N
⊢ ∀ᵐ (x : α) ∂μ, ∃ (l : E), Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 l)

Tactic:
h_cau_ae.mono fun x hx => cauchySeq_tendsto_of_complete ?_

Premises used: cauchySeq_tendsto_of_complete, Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
hp : LE.le (α := ℝ≥0∞) 1 ∞
hp_top : True
h_cau_ae : ∀ᵐ (x : α) ∂μ, ∀ (N n m : ℕ), N ≤ n → N ≤ m → ‖(f n - f m) x‖ₑ < B N
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → essSup (fun (x : α) ↦ ‖(f n - f m_1) x‖ₑ) μ < B N
pos :
  ∀ (x : α) (hx : ∀ (N n m : ℕ), N ≤ n → N ≤ m → ‖(f n - f m) x‖ₑ < B N),
    CauchySeq.{u_3, 0} (α := E) fun (n : ℕ) ↦ f n x
⊢ ∀ᵐ (x : α) ∂μ, ∃ (l : E), Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 l)

Tactic:
refine h_cau_ae.mono fun x hx => cauchySeq_tendsto_of_complete ?_

Premises used: cauchySeq_tendsto_of_complete, Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
B : ℕ → ℝ≥0∞
hB : Ne (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞
hp : LE.le (α := ℝ≥0∞) 1 ∞
hp_top : True
h_cau_ae : ∀ᵐ (x : α) ∂μ, ∀ (N n m : ℕ), N ≤ n → N ≤ m → ‖(f n - f m) x‖ₑ < B N
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → essSup (fun (x : α) ↦ ‖(f n - f m_1) x‖ₑ) μ < B N
x : α
hx : ∀ (N n m : ℕ), N ≤ n → N ≤ m → ‖(f n - f m) x‖ₑ < B N
⊢ CauchySeq.{u_3, 0} (α := E) fun (n : ℕ) ↦ f n x

Tactic:
cauchySeq_of_le_tendsto_0 (fun n => (B n).toReal) ?_ ?_

Premises used: cauchySeq_of_le_tendsto_0, ENNReal.toReal