awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
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_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
have rw : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - f_lim) p μ ≤ ε
Tactic: rw [ENNReal.tendsto_atTop_zero]
-- 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
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
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_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
⊢ ∃ (N : ℕ), B N ≤ ε
have suffices : ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → B n ≤ ε
Tactic: suffices h_tendsto_zero : ∃ N : ℕ, ∀ n : ℕ, N ≤ n → B n ≤ ε from
      ⟨h_tendsto_zero.choose, h_tendsto_zero.choose_spec _ le_rfl⟩
-- 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
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
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_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
⊢ ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - f_lim) p μ ≤ ε
have h_B : ∃ (N : ℕ), B N ≤ ε
Tactic: have h_B : ∃ N : ℕ, B N ≤ ε := by
    suffices h_tendsto_zero : ∃ N : ℕ, ∀ n : ℕ, N ≤ n → B n ≤ ε from
      ⟨h_tendsto_zero.choose, h_tendsto_zero.choose_spec _ le_rfl⟩
    exact (ENNReal.tendsto_atTop_zero.mp (ENNReal.tendsto_atTop_zero_of_tsum_ne_top hB)) ε hε
-- 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
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
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_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
h_B : ∃ (N : ℕ), B N ≤ ε
⊢ ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - f_lim) p μ ≤ ε
have obtain : ∀ (N : ℕ) (h_B : B N ≤ ε), ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - f_lim) p μ ≤ ε
Tactic: obtain ⟨N, h_B⟩ := h_B
Cleared hypotheses: h_B
-- 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
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
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_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
N : ℕ
h_B : B N ≤ ε
⊢ ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - f_lim) p μ ≤ ε
have refine : ∀ (n : ℕ) (hn : n ≥ N), eLpNorm (f n - f_lim) p μ ≤ ε
Tactic: refine ⟨N, fun n hn => ?_⟩
-- 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
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
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_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
N : ℕ
h_B : B N ≤ ε
n : ℕ
hn : n ≥ N
⊢ eLpNorm (f n - f_lim) p μ ≤ liminf (fun (m_1 : ℕ) ↦ eLpNorm (f n - f m_1) p μ) atTop
have refine : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n_1 : ℕ) ↦ (f n - f n_1) x) atTop (𝓝 ((f n - f_lim) x))
Tactic: refine eLpNorm_lim_le_liminf_eLpNorm (fun m => (hf n).sub (hf m)) (f n - f_lim) ?_
-- 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
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
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_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
N : ℕ
h_B : B N ≤ ε
n : ℕ
hn : n ≥ N
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n_1 : ℕ) ↦ (f n - f n_1) x) atTop (𝓝 ((f n - f_lim) x))
have refine : ∀ (x : α) (hx : Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))),
  Tendsto (fun (n_1 : ℕ) ↦ (f n - f n_1) x) atTop (𝓝 ((f n - f_lim) x))
Tactic: refine h_lim.mono fun x hx => ?_
-- 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
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
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_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
N : ℕ
h_B : B N ≤ ε
n : ℕ
hn : n ≥ N
x : α
hx : Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))
⊢ Tendsto (fun (n_1 : ℕ) ↦ (f n - f n_1) x) atTop (𝓝 ((f n - f_lim) x))
have simp_rw : Tendsto (fun (n_1 : ℕ) ↦ (f n + -f n_1) x) atTop (𝓝 ((f n + -f_lim) x))
Tactic: simp_rw [sub_eq_add_neg]
-- 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
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
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_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
N : ℕ
h_B : B N ≤ ε
n : ℕ
hn : n ≥ N
⊢ eLpNorm (f n - f_lim) p μ ≤ ε
have h_sub : eLpNorm (f n - f_lim) p μ ≤ liminf (fun (m_1 : ℕ) ↦ eLpNorm (f n - f m_1) p μ) atTop
Tactic: have h_sub : eLpNorm (f n - f_lim) p μ ≤ atTop.liminf fun m => eLpNorm (f n - f m) p μ := by
    refine eLpNorm_lim_le_liminf_eLpNorm (fun m => (hf n).sub (hf m)) (f n - f_lim) ?_
    refine h_lim.mono fun x hx => ?_
    simp_rw [sub_eq_add_neg]
    exact Tendsto.add tendsto_const_nhds (Tendsto.neg hx)
-- 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
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
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_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
N : ℕ
h_B : B N ≤ ε
n : ℕ
hn : n ≥ N
h_sub : eLpNorm (f n - f_lim) p μ ≤ liminf (fun (m_1 : ℕ) ↦ eLpNorm (f n - f m_1) p μ) atTop
⊢ eLpNorm (f n - f_lim) p μ ≤ ε
have refine : liminf (fun (m_1 : ℕ) ↦ eLpNorm (f n - f m_1) p μ) atTop ≤ ε
Tactic: refine h_sub.trans ?_
-- 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
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
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_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
N : ℕ
h_B : B N ≤ ε
n : ℕ
hn : n ≥ N
h_sub : eLpNorm (f n - f_lim) p μ ≤ liminf (fun (m_1 : ℕ) ↦ eLpNorm (f n - f m_1) p μ) atTop
⊢ liminf (fun (m_1 : ℕ) ↦ eLpNorm (f n - f m_1) p μ) atTop ≤ ε
have refine : ∀ (a : ℕ), ∃ b ≥ a, eLpNorm (f n - f b) p μ ≤ ε
Tactic: refine liminf_le_of_frequently_le' (frequently_atTop.mpr ?_)
-- 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
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
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_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
N : ℕ
h_B : B N ≤ ε
n : ℕ
hn : n ≥ N
h_sub : eLpNorm (f n - f_lim) p μ ≤ liminf (fun (m_1 : ℕ) ↦ eLpNorm (f n - f m_1) p μ) atTop
⊢ ∀ (a : ℕ), ∃ b ≥ a, eLpNorm (f n - f b) p μ ≤ ε
have refine : ∀ (N1 : ℕ), eLpNorm (f n - f (max N N1)) p μ ≤ ε
Tactic: refine fun N1 => ⟨max N N1, le_max_right _ _, ?_⟩
-- 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
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), MemLp (f n) p μ
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
⊢ MemLp f_lim p μ
have refine : eLpNorm f_lim p μ < ∞
Tactic: refine ⟨h_lim_meas, ?_⟩
-- 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
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), MemLp (f n) p μ
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
⊢ eLpNorm f_lim p μ < ∞
have h_tendsto₁ : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - f_lim) p μ ≤ ε
Tactic: rw [ENNReal.tendsto_atTop_zero] at h_tendsto
Cleared hypotheses: h_tendsto
-- 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
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), MemLp (f n) p μ
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - f_lim) p μ ≤ ε
⊢ eLpNorm f_lim p μ < ∞
have obtain : ∀ (N : ℕ) (h_tendsto_1 : ∀ n ≥ N, eLpNorm (f n - f_lim) p μ ≤ 1), eLpNorm f_lim p μ < ∞
Tactic: obtain ⟨N, h_tendsto_1⟩ := h_tendsto 1 zero_lt_one
-- 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
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), MemLp (f n) p μ
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - f_lim) p μ ≤ ε
N : ℕ
h_tendsto_1 : ∀ n ≥ N, eLpNorm (f n - f_lim) p μ ≤ 1
⊢ eLpNorm f_lim p μ < ∞
have h_tendsto_1₁ : eLpNorm (f N - f_lim) p μ ≤ 1
Tactic: specialize h_tendsto_1 N (le_refl N)
Cleared hypotheses: h_tendsto_1
-- 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
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), MemLp (f n) p μ
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - f_lim) p μ ≤ ε
N : ℕ
h_tendsto_1 : eLpNorm (f N - f_lim) p μ ≤ 1
⊢ eLpNorm f_lim p μ < ∞
have h_add : f_lim = f_lim - f N + f N
Tactic: have h_add : f_lim = f_lim - f N + f N := by abel
-- 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
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), MemLp (f n) p μ
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - f_lim) p μ ≤ ε
N : ℕ
h_tendsto_1 : eLpNorm (f N - f_lim) p μ ≤ 1
h_add : f_lim = f_lim - f N + f N
⊢ eLpNorm f_lim p μ < ∞
have rw : eLpNorm (f_lim - f N + f N) p μ < ∞
Tactic: rw [h_add]
-- 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
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), MemLp (f n) p μ
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - f_lim) p μ ≤ ε
N : ℕ
h_tendsto_1 : eLpNorm (f N - f_lim) p μ ≤ 1
h_add : f_lim = f_lim - f N + f N
⊢ eLpNorm (f_lim - f N + f N) p μ < ∞
have refine : eLpNorm (f_lim - f N) p μ + eLpNorm (f N) p μ < ∞
Tactic: refine lt_of_le_of_lt (eLpNorm_add_le (h_lim_meas.sub (hf N).1) (hf N).1 hp) ?_
-- 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
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), MemLp (f n) p μ
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - f_lim) p μ ≤ ε
N : ℕ
h_tendsto_1 : eLpNorm (f N - f_lim) p μ ≤ 1
h_add : f_lim = f_lim - f N + f N
⊢ eLpNorm (f_lim - f N) p μ + eLpNorm (f N) p μ < ∞
have rw : eLpNorm (f_lim - f N) p μ < ∞ ∧ eLpNorm (f N) p μ < ∞
Tactic: rw [ENNReal.add_lt_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
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), MemLp (f n) p μ
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - f_lim) p μ ≤ ε
N : ℕ
h_tendsto_1 : eLpNorm (f N - f_lim) p μ ≤ 1
h_add : f_lim = f_lim - f N + f N
⊢ eLpNorm (f_lim - f N) p μ < ∞ ∧ eLpNorm (f N) p μ < ∞
have left : eLpNorm (f_lim - f N) p μ < ∞
Tactic: constructor
-- 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
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), MemLp (f n) p μ
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - f_lim) p μ ≤ ε
N : ℕ
h_tendsto_1 : eLpNorm (f N - f_lim) p μ ≤ 1
h_add : f_lim = f_lim - f N + f N
left : eLpNorm (f_lim - f N) p μ < ∞
⊢ eLpNorm (f_lim - f N) p μ < ∞ ∧ eLpNorm (f N) p μ < ∞
have right : eLpNorm (f N) p μ < ∞
Tactic: constructor
-- 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
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), MemLp (f n) p μ
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - f_lim) p μ ≤ ε
N : ℕ
h_tendsto_1 : eLpNorm (f N - f_lim) p μ ≤ 1
h_add : f_lim = f_lim - f N + f N
⊢ eLpNorm (f_lim - f N) p μ < ∞
have left : eLpNorm (f_lim - f N) p μ ≤ 1
Tactic: refine lt_of_le_of_lt ?_ ENNReal.one_lt_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
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), MemLp (f n) p μ
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - f_lim) p μ ≤ ε
N : ℕ
h_tendsto_1 : eLpNorm (f N - f_lim) p μ ≤ 1
h_add : f_lim = f_lim - f N + f N
⊢ eLpNorm (f_lim - f N) p μ ≤ 1
have h_neg : f_lim - f N = -(f N - f_lim)
Tactic: have h_neg : f_lim - f N = -(f N - f_lim) := by simp
-- 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
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), MemLp (f n) p μ
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - f_lim) p μ ≤ ε
N : ℕ
h_tendsto_1 : eLpNorm (f N - f_lim) p μ ≤ 1
h_add : f_lim = f_lim - f N + f N
h_neg : f_lim - f N = -(f N - f_lim)
⊢ eLpNorm (f_lim - f N) p μ ≤ 1
have left : eLpNorm (-(f N - f_lim)) p μ ≤ 1
Tactic: rwa [h_neg, eLpNorm_neg]
-- 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
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), MemLp (f n) 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
⊢ ∃ (f_lim : α → E), MemLp f_lim p μ ∧ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
have obtain : ∀ (f_lim : α → E) (h_f_lim_meas : StronglyMeasurable f_lim)
  (h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))),
  ∃ (f_lim : α → E), MemLp f_lim p μ ∧ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
Tactic: obtain ⟨f_lim, h_f_lim_meas, h_lim⟩ :
      ∃ f_lim : α → E, StronglyMeasurable f_lim ∧
        ∀ᵐ x ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x)) :=
    exists_stronglyMeasurable_limit_of_tendsto_ae (fun n => (hf n).1)
      (ae_tendsto_of_cauchy_eLpNorm (fun n => (hf n).1) hp hB 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
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), MemLp (f n) 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
f_lim : α → E
h_f_lim_meas : StronglyMeasurable f_lim
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))
⊢ ∃ (f_lim : α → E), MemLp f_lim p μ ∧ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
have h_tendsto' : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
Tactic: have h_tendsto' : atTop.Tendsto (fun n => eLpNorm (f n - f_lim) p μ) (𝓝 0) :=
    cauchy_tendsto_of_tendsto (fun m => (hf m).1) f_lim hB h_cau h_lim
-- 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
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), MemLp (f n) 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
f_lim : α → E
h_f_lim_meas : StronglyMeasurable f_lim
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))
h_tendsto' : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
⊢ ∃ (f_lim : α → E), MemLp f_lim p μ ∧ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
have h_ℒp_lim : MemLp f_lim p μ
Tactic: have h_ℒp_lim : MemLp f_lim p μ :=
    memLp_of_cauchy_tendsto hp hf f_lim h_f_lim_meas.aestronglyMeasurable h_tendsto'
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
mα : MeasurableSpace α
μ : Measure α
f : α → E
hf : FinStronglyMeasurable f μ
h'f : ¬f =ᶠ[ae μ] 0
⊢ ∃ (s : Set α),
    MeasurableSet s ∧
      LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ∧
        LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
have contrapose! : ∀
  (h'f :
    ∀ (s : Set α) (_ : MeasurableSet s) (_ : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)),
      LE.le (α := ℝ≥0∞) (∞ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)),
  f =ᶠ[ae μ] 0
Tactic: contrapose! h'f
Cleared hypotheses: h'f
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
mα : MeasurableSpace α
μ : Measure α
f : α → E
hf : FinStronglyMeasurable f μ
h'f :
  ∀ (s : Set α) (_ : MeasurableSet s) (_ : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)),
    LE.le (α := ℝ≥0∞) (∞ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ f =ᶠ[ae μ] 0
have rcases : ∀ (fn : ℕ → SimpleFunc α E)
  (hfn :
    ∀ (n : ℕ),
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support.{u_1, u_2} (M := E) (⇑(fn n) : (a : α) → E)) : ℝ≥0∞)
        (∞ : ℝ≥0∞))
  (hfn_lim : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fn n : (a : α) → E) x) atTop (𝓝 (f x))), f =ᶠ[ae μ] 0
Tactic: rcases hf with ⟨fn, hfn, hfn_lim⟩
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
mα : MeasurableSpace α
μ : Measure α
f : α → E
h'f :
  ∀ (s : Set α) (_ : MeasurableSet s) (_ : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)),
    LE.le (α := ℝ≥0∞) (∞ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
fn : ℕ → SimpleFunc α E
hfn :
  ∀ (n : ℕ),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support.{u_1, u_2} (M := E) (⇑(fn n) : (a : α) → E)) : ℝ≥0∞)
      (∞ : ℝ≥0∞)
hfn_lim : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fn n : (a : α) → E) x) atTop (𝓝 (f x))
n : ℕ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support.{u_1, u_2} (M := E) (⇑(fn n) : (a : α) → E)) : ℝ≥0∞)
    (0 : ℝ≥0∞)
have by_contra! : ∀
  (this :
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support.{u_1, u_2} (M := E) (⇑(fn n) : (a : α) → E)) : ℝ≥0∞)
      (0 : ℝ≥0∞)),
  False
Tactic: by_contra!
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp (hypothesis)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
mα : MeasurableSpace α
μ : Measure α
f : α → E
h'f :
  ∀ (s : Set α) (_ : MeasurableSet s) (_ : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)),
    LE.le (α := ℝ≥0∞) (∞ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
fn : ℕ → SimpleFunc α E
hfn :
  ∀ (n : ℕ),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support.{u_1, u_2} (M := E) (⇑(fn n) : (a : α) → E)) : ℝ≥0∞)
      (∞ : ℝ≥0∞)
hfn_lim : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fn n : (a : α) → E) x) atTop (𝓝 (f x))
n : ℕ
this :
  Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support.{u_1, u_2} (M := E) (⇑(fn n) : (a : α) → E)) : ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ False
have this₁ : LE.le (α := ℝ≥0∞) (∞ : ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) (Function.support.{u_1, u_2} (M := E) (⇑(fn n) : (a : α) → E)) : ℝ≥0∞)
Tactic: have := h'f (Function.support (fn n)) (fn n).measurableSet_support (by positivity)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp (hypothesis)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
mα : MeasurableSpace α
μ : Measure α
f : α → E
h'f :
  ∀ (s : Set α) (_ : MeasurableSet s) (_ : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)),
    LE.le (α := ℝ≥0∞) (∞ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
fn : ℕ → SimpleFunc α E
hfn :
  ∀ (n : ℕ),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support.{u_1, u_2} (M := E) (⇑(fn n) : (a : α) → E)) : ℝ≥0∞)
      (∞ : ℝ≥0∞)
hfn_lim : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fn n : (a : α) → E) x) atTop (𝓝 (f x))
⊢ f =ᶠ[ae μ] 0
have A : ∀ (n : ℕ),
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support.{u_1, u_2} (M := E) (⇑(fn n) : (a : α) → E)) : ℝ≥0∞)
    (0 : ℝ≥0∞)
Tactic: have A n : μ (Function.support (fn n)) = 0 := by
    by_contra!
    have := h'f (Function.support (fn n)) (fn n).measurableSet_support (by positivity)
    grind