awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (hypothesis)
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 : α) ∂μ, LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) x - f i x‖ₑ) ∞
have rpow_ae_lt_top : ∀ᵐ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
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‖ₑ) ∞
have 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‖ₑ) ∞
Tactic: refine rpow_ae_lt_top.mono fun x hx => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
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 < ∞
⊢ LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) x - f i x‖ₑ) ∞
have 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‖ₑ) ∞
Tactic: rwa [← ENNReal.lt_rpow_inv_iff hp_pos,
    ENNReal.top_rpow_of_pos (by simp [hp_pos] : 0 < p⁻¹)] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
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‖ₑ) ∞
⊢ LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) x - f i x‖ₑ) ∞
have rwa₁ : ∀ (hx : 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
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (hypothesis)
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
have h1 : ∀ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (hypothesis)
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
⊢ ∀ᵐ (x : α) ∂μ, Summable.{u_3, 0} (α := E) fun (i : ℕ) ↦ f (i + 1) x - f i x
have 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
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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (hypothesis)
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
⊢ ∀ᵐ (x : α) ∂μ, Summable.{u_3, 0} (α := E) fun (i : ℕ) ↦ f (i + 1) x - f i x
have h3 : (∫⁻ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (hypothesis)
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 : α) ∂μ, Summable.{u_3, 0} (α := E) fun (i : ℕ) ↦ f (i + 1) x - f i x
have h4 : ∀ᵐ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (hypothesis)
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 : α) ∂μ, ∃ (l : E), Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 l)
have h_summable : ∀ᵐ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
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)
have 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)
Tactic: refine h_summable.mono fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (hypothesis)
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
⊢ ∃ (l : E), Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 l)
have 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)))
Tactic: have hx_sum := hx.hasSum.tendsto_sum_nat
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (hypothesis)
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)))
⊢ ∃ (l : E), Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 l)
have hx_sum₁ : 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
Cleared hypotheses: hx_sum
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
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
⊢ ∀ᵐ (x : α) ∂μ, ∃ (l : E), Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 l)
have pos : ∀ (hp_top : p = ∞), ∀ᵐ (x : α) ∂μ, ∃ (l : E), Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 l)
Tactic: by_cases hp_top : p = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
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)
⊢ ∀ᵐ (x : α) ∂μ, ∃ (l : E), Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 l)
have neg : ∀ (hp_top : ¬p = ∞), ∀ᵐ (x : α) ∂μ, ∃ (l : E), Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 l)
Tactic: by_cases hp_top : p = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (hypothesis)
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 = ∞
⊢ ∀ᵐ (x : α) ∂μ, ∃ (l : E), Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 l)
have hp₁ : LE.le (α := ℝ≥0∞) 1 ∞
Tactic: simp_rw [hp_top] at *
Cleared hypotheses: hp, h_cau, hp_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (hypothesis)
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 ∞
⊢ ∀ᵐ (x : α) ∂μ, ∃ (l : E), Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 l)
have h_cau₁ : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) ∞ μ < B N
Tactic: simp_rw [hp_top] at *
Cleared hypotheses: hp, h_cau, hp_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (hypothesis)
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
⊢ ∀ᵐ (x : α) ∂μ, ∃ (l : E), Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 l)
have hp_top₁ : True
Tactic: simp_rw [hp_top] at *
Cleared hypotheses: hp, h_cau, hp_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
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
have 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
Tactic: simp_rw [ae_all_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (hypothesis)
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 : α) ∂μ, ∃ (l : E), Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 l)
have h_cau_ae : ∀ᵐ (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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (hypothesis)
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
⊢ ∀ᵐ (x : α) ∂μ, ∃ (l : E), Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 l)
have h_cau₁ : ∀ (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
Cleared hypotheses: h_cau
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
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)
have 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
Tactic: refine h_cau_ae.mono fun x hx => cauchySeq_tendsto_of_complete ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
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
have pos : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (f n x) (f m x) ≤ (fun (n : ℕ) ↦ (B n).toReal) N
Tactic: refine cauchySeq_of_le_tendsto_0 (fun n => (B n).toReal) ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
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
pos : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (f n x) (f m x) ≤ (fun (n : ℕ) ↦ (B n).toReal) N
⊢ CauchySeq.{u_3, 0} (α := E) fun (n : ℕ) ↦ f n x
have pos₁ : Tendsto (β := ℝ) (fun (n : ℕ) ↦ (B n).toReal) atTop (𝓝 0)
Tactic: refine cauchySeq_of_le_tendsto_0 (fun n => (B n).toReal) ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (hypothesis)
Goal:
α : Type u_1
m_1 : 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 : ℕ), N ≤ n → N ≤ m → essSup (fun (x : α) ↦ ‖(f n - f m) x‖ₑ) μ < B N
x : α
hx : ∀ (N n m : ℕ), N ≤ n → N ≤ m → ‖(f n - f m) x‖ₑ < B N
n m N : ℕ
hnN : N ≤ n
hmN : N ≤ m
⊢ dist (f n x) (f m x) ≤ (fun (n : ℕ) ↦ (B n).toReal) N
have hx₁ : ‖(f n - f m) x‖ₑ < B N
Tactic: specialize hx N n m hnN hmN
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
Goal:
α : Type u_1
m_1 : 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 : ℕ), N ≤ n → N ≤ m → essSup (fun (x : α) ↦ ‖(f n - f m) x‖ₑ) μ < B N
x : α
n m N : ℕ
hnN : N ≤ n
hmN : N ≤ m
hx : ‖(f n - f m) x‖ₑ < B N
⊢ dist (f n x) (f m x) ≤ (fun (n : ℕ) ↦ (B n).toReal) N
have pos : ‖f n x - f m x‖ₑ ≤ B N
Tactic: rw [_root_.dist_eq_norm,
        ← ENNReal.ofReal_le_iff_le_toReal (ENNReal.ne_top_of_tsum_ne_top hB N),
        ofReal_norm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (hypothesis)
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 = ∞
⊢ ∀ᵐ (x : α) ∂μ, ∃ (l : E), Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 l)
have hp1 : 1 ≤ p.toReal
Tactic: have hp1 : 1 ≤ p.toReal := by
    rw [← ENNReal.ofReal_le_iff_le_toReal hp_top, ENNReal.ofReal_one]
    exact hp
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (hypothesis)
Goal:
α : Type u_1
m_1 : 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 : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N
hp_top : ¬p = ∞
hp1 : 1 ≤ p.toReal
N n m : ℕ
hn : N ≤ n
hm : N ≤ m
⊢ eLpNorm' (f n - f m) p.toReal μ < B N
have h_cau₁ : eLpNorm (f n - f m) p μ < B N
Tactic: specialize h_cau N n m hn hm
Cleared hypotheses: h_cau
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
Goal:
α : Type u_1
m_1 : 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) ∞
hp_top : ¬p = ∞
hp1 : 1 ≤ p.toReal
N n m : ℕ
hn : N ≤ n
hm : N ≤ m
h_cau : eLpNorm (f n - f m) p μ < B N
⊢ eLpNorm' (f n - f m) p.toReal μ < B N
have rwa : ∀ (h_cau : eLpNorm' (f n - f m) p.toReal μ < B N), eLpNorm' (f n - f m) p.toReal μ < B N
Tactic: rwa [eLpNorm_eq_eLpNorm' (zero_lt_one.trans_le hp).ne.symm hp_top] at h_cau
Cleared hypotheses: h_cau
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (hypothesis)
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 = ∞
hp1 : 1 ≤ p.toReal
⊢ ∀ᵐ (x : α) ∂μ, ∃ (l : E), Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 l)
have h_cau' : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm' (f n - f m_1) p.toReal μ < B N
Tactic: have h_cau' : ∀ N n m : ℕ, N ≤ n → N ≤ m → eLpNorm' (f n - f m) p.toReal μ < B N := by
    intro N n m hn hm
    specialize h_cau N n m hn hm
    rwa [eLpNorm_eq_eLpNorm' (zero_lt_one.trans_le hp).ne.symm hp_top] at h_cau