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
hp : Fact (1 ≤ p)
H :
  ∀ (f : ℕ → α → E),
    (∀ (n : ℕ), MemLp (f n) p μ) →
      ∀ (B : ℕ → ℝ≥0∞),
        LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞ →
          (∀ (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)
B : (n : ℕ) → ℝ := fun (n : ℕ) ↦ (1 / 2) ^ n
hB_pos : ∀ (n : ℕ), 0 < B n
f : ℕ → ↥(Lp E p μ)
hf : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → dist (f n) (f m_1) < B N
M : ℝ
hB : HasSum B M
B1 : (n : ℕ) → ℝ≥0∞ := fun (n : ℕ) ↦ ENNReal.ofReal (B n)
hB1_has : HasSum B1 (ENNReal.ofReal M)
hB1 : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), B1 i) ∞
f1 : ℕ → α → E := fun (n : ℕ) ↦ (↑(↑(f n) : α →ₘ[μ] E) : α → E)
⊢ ∃ (f_lim : α → E),
    MemLp f_lim p μ ∧
      Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm ((↑(↑(f n) : α →ₘ[μ] E) : α → E) - f_lim) p μ) atTop (𝓝 0)
have refine : ∀ (N n m_1 : ℕ) (hn : N ≤ n) (hm : N ≤ m_1), eLpNorm (f1 n - f1 m_1) p μ < B1 N
Tactic: refine H f1 (fun n => Lp.memLp (f n)) B1 hB1 fun N n m hn hm => ?_
-- 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
hp : Fact (1 ≤ p)
H :
  ∀ (f : ℕ → α → E),
    (∀ (n : ℕ), MemLp (f n) p μ) →
      ∀ (B : ℕ → ℝ≥0∞),
        LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞ →
          (∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N) →
            ∃ (f_lim : α → E),
              MemLp f_lim p μ ∧ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
B : (n : ℕ) → ℝ := fun (n : ℕ) ↦ (1 / 2) ^ n
hB_pos : ∀ (n : ℕ), 0 < B n
f : ℕ → ↥(Lp E p μ)
hf : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (f n) (f m) < B N
M : ℝ
hB : HasSum B M
B1 : (n : ℕ) → ℝ≥0∞ := fun (n : ℕ) ↦ ENNReal.ofReal (B n)
hB1_has : HasSum B1 (ENNReal.ofReal M)
hB1 : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), B1 i) ∞
f1 : ℕ → α → E := fun (n : ℕ) ↦ (↑(↑(f n) : α →ₘ[μ] E) : α → E)
N n m : ℕ
hn : N ≤ n
hm : N ≤ m
⊢ eLpNorm (f1 n - f1 m) p μ < B1 N
have hf₁ : dist (f n) (f m) < B N
Tactic: specialize hf N n m hn hm
Cleared hypotheses: hf
-- 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
hp : Fact (1 ≤ p)
H :
  ∀ (f : ℕ → α → E),
    (∀ (n : ℕ), MemLp (f n) p μ) →
      ∀ (B : ℕ → ℝ≥0∞),
        LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞ →
          (∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N) →
            ∃ (f_lim : α → E),
              MemLp f_lim p μ ∧ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
B : (n : ℕ) → ℝ := fun (n : ℕ) ↦ (1 / 2) ^ n
hB_pos : ∀ (n : ℕ), 0 < B n
f : ℕ → ↥(Lp E p μ)
M : ℝ
hB : HasSum B M
B1 : (n : ℕ) → ℝ≥0∞ := fun (n : ℕ) ↦ ENNReal.ofReal (B n)
hB1_has : HasSum B1 (ENNReal.ofReal M)
hB1 : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), B1 i) ∞
f1 : ℕ → α → E := fun (n : ℕ) ↦ (↑(↑(f n) : α →ₘ[μ] E) : α → E)
N n m : ℕ
hn : N ≤ n
hm : N ≤ m
hf : dist (f n) (f m) < B N
⊢ eLpNorm (f1 n - f1 m) p μ < B1 N
have hf₁ : (eLpNorm ((↑(↑(f n) : α →ₘ[μ] E) : α → E) - (↑(↑(f m) : α →ₘ[μ] E) : α → E)) p μ).toReal < B N
Tactic: rw [dist_def] at hf
Cleared hypotheses: hf
-- 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
hp : Fact (1 ≤ p)
H :
  ∀ (f : ℕ → α → E),
    (∀ (n : ℕ), MemLp (f n) p μ) →
      ∀ (B : ℕ → ℝ≥0∞),
        LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞ →
          (∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N) →
            ∃ (f_lim : α → E),
              MemLp f_lim p μ ∧ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
B : (n : ℕ) → ℝ := fun (n : ℕ) ↦ (1 / 2) ^ n
hB_pos : ∀ (n : ℕ), 0 < B n
f : ℕ → ↥(Lp E p μ)
M : ℝ
hB : HasSum B M
B1 : (n : ℕ) → ℝ≥0∞ := fun (n : ℕ) ↦ ENNReal.ofReal (B n)
hB1_has : HasSum B1 (ENNReal.ofReal M)
hB1 : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), B1 i) ∞
f1 : ℕ → α → E := fun (n : ℕ) ↦ (↑(↑(f n) : α →ₘ[μ] E) : α → E)
N n m : ℕ
hn : N ≤ n
hm : N ≤ m
hf : (eLpNorm ((↑(↑(f n) : α →ₘ[μ] E) : α → E) - (↑(↑(f m) : α →ₘ[μ] E) : α → E)) p μ).toReal < B N
⊢ eLpNorm ((↑(↑(f n) : α →ₘ[μ] E) : α → E) - (↑(↑(f m) : α →ₘ[μ] E) : α → E)) p μ < B1 N
have rwa : eLpNorm ((↑(↑(f n) : α →ₘ[μ] E) : α → E) - (↑(↑(f m) : α →ₘ[μ] E) : α → E)) p μ ≠ ∞
Tactic: rwa [ENNReal.lt_ofReal_iff_toReal_lt]
-- 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
hp : Fact (1 ≤ p)
H :
  ∀ (f : ℕ → α → E),
    (∀ (n : ℕ), MemLp (f n) p μ) →
      ∀ (B : ℕ → ℝ≥0∞),
        LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), B i) ∞ →
          (∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N) →
            ∃ (f_lim : α → E),
              MemLp f_lim p μ ∧ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
B : (n : ℕ) → ℝ := fun (n : ℕ) ↦ (1 / 2) ^ n
hB_pos : ∀ (n : ℕ), 0 < B n
f : ℕ → ↥(Lp E p μ)
M : ℝ
hB : HasSum B M
B1 : (n : ℕ) → ℝ≥0∞ := fun (n : ℕ) ↦ ENNReal.ofReal (B n)
hB1_has : HasSum B1 (ENNReal.ofReal M)
hB1 : LT.lt (α := ℝ≥0∞) (∑' (i : ℕ), B1 i) ∞
f1 : ℕ → α → E := fun (n : ℕ) ↦ (↑(↑(f n) : α →ₘ[μ] E) : α → E)
N n m : ℕ
hn : N ≤ n
hm : N ≤ m
hf : (eLpNorm ((↑(↑(f n) : α →ₘ[μ] E) : α → E) - (↑(↑(f m) : α →ₘ[μ] E) : α → E)) p μ).toReal < B N
⊢ eLpNorm ((↑(↑(f n) : α →ₘ[μ] E) : α → E) - (↑(↑(f m) : α →ₘ[μ] E) : α → E)) p μ ≠ ∞
have rw : eLpNorm (↑(↑(f n - f m) : α →ₘ[μ] E) : α → E) p μ ≠ ∞
Tactic: rw [eLpNorm_congr_ae (Lp.coeFn_sub _ _).symm]
-- 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∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm' (f n - f m_1) p μ < B N
n : ℕ
f_norm_diff : (i : ℕ) → (x : α) → ℝ := fun (i : ℕ) (x : α) ↦ ‖f (i + 1) x - f i x‖
⊢ eLpNorm' (ε := ℝ) (fun (x : α) ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖) p μ ≤ ∑' (i : ℕ), B i
have hgf_norm_diff : ∀ (n : ℕ),
  Eq.{u_1 + 1} (α := (x : α) → ℝ) (fun (x : α) ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖)
    (∑ i ∈ Finset.range (n + 1), f_norm_diff i)
Tactic: have hgf_norm_diff :
    ∀ n,
      (fun x => ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖) =
        ∑ i ∈ Finset.range (n + 1), f_norm_diff i :=
    fun n => funext fun x => by simp [f_norm_diff]
-- 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∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm' (f n - f m_1) p μ < B N
n : ℕ
f_norm_diff : (i : ℕ) → (x : α) → ℝ := fun (i : ℕ) (x : α) ↦ ‖f (i + 1) x - f i x‖
hgf_norm_diff :
  ∀ (n : ℕ),
    Eq.{u_1 + 1} (α := (x : α) → ℝ) (fun (x : α) ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖)
      (∑ i ∈ Finset.range (n + 1), f_norm_diff i)
⊢ eLpNorm' (ε := ℝ) (fun (x : α) ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖) p μ ≤ ∑' (i : ℕ), B i
have rw : eLpNorm' (ε := ℝ) (∑ i ∈ Finset.range (n + 1), f_norm_diff i) p μ ≤ ∑' (i : ℕ), B i
Tactic: rw [hgf_norm_diff]
-- 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∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm' (f n - f m_1) p μ < B N
n : ℕ
f_norm_diff : (i : ℕ) → (x : α) → ℝ := fun (i : ℕ) (x : α) ↦ ‖f (i + 1) x - f i x‖
hgf_norm_diff :
  ∀ (n : ℕ),
    Eq.{u_1 + 1} (α := (x : α) → ℝ) (fun (x : α) ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖)
      (∑ i ∈ Finset.range (n + 1), f_norm_diff i)
⊢ eLpNorm' (ε := ℝ) (∑ i ∈ Finset.range (n + 1), f_norm_diff i) p μ ≤ ∑' (i : ℕ), B i
have refine : LE.le (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), eLpNorm' (ε := ℝ) (fun (x : α) ↦ ‖(f (i + 1) - f i) x‖) p μ)
  (∑' (i : ℕ), B i)
Tactic: refine (eLpNorm'_sum_le (fun i _ => ((hf (i + 1)).sub (hf i)).norm) hp1).trans ?_
-- 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∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm' (f n - f m_1) p μ < B N
n : ℕ
f_norm_diff : (i : ℕ) → (x : α) → ℝ := fun (i : ℕ) (x : α) ↦ ‖f (i + 1) x - f i x‖
hgf_norm_diff :
  ∀ (n : ℕ),
    Eq.{u_1 + 1} (α := (x : α) → ℝ) (fun (x : α) ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖)
      (∑ i ∈ Finset.range (n + 1), f_norm_diff i)
⊢ LE.le (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), eLpNorm' (ε := ℝ) (fun (x : α) ↦ ‖(f (i + 1) - f i) x‖) p μ)
    (∑' (i : ℕ), B i)
have simp_rw : LE.le (α := ℝ≥0∞) (∑ x ∈ Finset.range (n + 1), eLpNorm' (f (x + 1) - f x) p μ) (∑' (i : ℕ), B i)
Tactic: simp_rw [eLpNorm'_norm]
-- 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∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm' (f n - f m_1) p μ < B N
n : ℕ
f_norm_diff : (i : ℕ) → (x : α) → ℝ := fun (i : ℕ) (x : α) ↦ ‖f (i + 1) x - f i x‖
hgf_norm_diff :
  ∀ (n : ℕ),
    Eq.{u_1 + 1} (α := (x : α) → ℝ) (fun (x : α) ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖)
      (∑ i ∈ Finset.range (n + 1), f_norm_diff i)
⊢ LE.le (α := ℝ≥0∞) (∑ x ∈ Finset.range (n + 1), eLpNorm' (f (x + 1) - f x) p μ) (∑' (i : ℕ), B i)
have refine : ∀ i ∈ Finset.range (n + 1), eLpNorm' (f (i + 1) - f i) p μ ≤ B i
Tactic: refine (Finset.sum_le_sum ?_).trans <| ENNReal.sum_le_tsum _
-- 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
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hn : eLpNorm' (ε := ℝ) (fun (x : α) ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖) p μ ≤ ∑' (i : ℕ), B i
⊢ ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p ∂μ ≤
    HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p
have hp_pos : 0 < p
Tactic: have hp_pos : 0 < p := zero_lt_one.trans_le hp1
-- 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
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hn : eLpNorm' (ε := ℝ) (fun (x : α) ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖) p μ ≤ ∑' (i : ℕ), B i
hp_pos : 0 < p
⊢ ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p ∂μ ≤
    HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p
have rw : (∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i
Tactic: rw [← inv_inv p, @ENNReal.le_rpow_inv_iff _ _ p⁻¹ (by simp [hp_pos]), inv_inv p]
-- 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
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hn : eLpNorm' (ε := ℝ) (fun (x : α) ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖) p μ ≤ ∑' (i : ℕ), B i
hp_pos : 0 < p
⊢ (∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i
have hn₁ : (∫⁻ (a : α), enorm (E := ℝ) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖) ^ p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i
Tactic: simp_rw [eLpNorm'_eq_lintegral_enorm, one_div] at hn
Cleared hypotheses: hn
-- 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
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hp_pos : 0 < p
hn : (∫⁻ (a : α), enorm (E := ℝ) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖) ^ p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i
⊢ Eq.{u_1 + 1} (α := (a : α) → ℝ≥0∞)
    (fun (a : α) ↦ enorm (E := ℝ) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖) ^ p) fun (a : α) ↦
    HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p
have h : ∀ (a : α),
  enorm (E := ℝ) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖) ^ p =
    HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p
Tactic: ext1 a
-- 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
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hp_pos : 0 < p
hn : (∫⁻ (a : α), enorm (E := ℝ) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖) ^ p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i
a : α
⊢ enorm (E := ℝ) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖) ^ p =
    HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p
have h : enorm (E := ℝ) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖) = ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ
Tactic: congr
-- 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
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hp_pos : 0 < p
hn : (∫⁻ (a : α), enorm (E := ℝ) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖) ^ p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i
a : α
⊢ enorm (E := ℝ) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖) =
    ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ
have h : ENNReal.ofReal (norm (E := ℝ) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖)) =
  ∑ x ∈ Finset.range (n + 1), ENNReal.ofReal ‖f (x + 1) a - f x a‖
Tactic: simp_rw [← ofReal_norm]
-- 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
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hp_pos : 0 < p
hn : (∫⁻ (a : α), enorm (E := ℝ) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖) ^ p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i
a : α
⊢ ENNReal.ofReal (norm (E := ℝ) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖)) =
    ∑ x ∈ Finset.range (n + 1), ENNReal.ofReal ‖f (x + 1) a - f x a‖
have h : ENNReal.ofReal (norm (E := ℝ) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖)) =
  ENNReal.ofReal (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖)
Tactic: rw [← ENNReal.ofReal_sum_of_nonneg]
-- 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
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hp_pos : 0 < p
hn : (∫⁻ (a : α), enorm (E := ℝ) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖) ^ p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i
a : α
h :
  ENNReal.ofReal (norm (E := ℝ) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖)) =
    ENNReal.ofReal (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖)
⊢ ENNReal.ofReal (norm (E := ℝ) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖)) =
    ∑ x ∈ Finset.range (n + 1), ENNReal.ofReal ‖f (x + 1) a - f x a‖
have h₁ : ∀ i ∈ Finset.range (n + 1), 0 ≤ ‖f (i + 1) a - f i a‖
Tactic: rw [← ENNReal.ofReal_sum_of_nonneg]
-- 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
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hp_pos : 0 < p
hn : (∫⁻ (a : α), enorm (E := ℝ) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖) ^ p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i
a : α
⊢ ENNReal.ofReal (norm (E := ℝ) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖)) =
    ENNReal.ofReal (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖)
have rw : LE.le (α := ℝ) 0 (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖)
Tactic: rw [Real.norm_of_nonneg _]
-- 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
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hp_pos : 0 < p
hn : (∫⁻ (a : α), enorm (E := ℝ) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖) ^ p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i
⊢ (∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i
have h_nnnorm_nonneg : Eq.{u_1 + 1} (α := (a : α) → ℝ≥0∞)
  (fun (a : α) ↦ enorm (E := ℝ) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖) ^ p) fun (a : α) ↦
  HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p
Tactic: have h_nnnorm_nonneg :
    (fun a => ‖∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖‖ₑ ^ p) = fun a =>
      (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p := by
    ext1 a
    congr
    simp_rw [← ofReal_norm]
    rw [← ENNReal.ofReal_sum_of_nonneg]
    · rw [Real.norm_of_nonneg _]
      exact Finset.sum_nonneg fun x _ => norm_nonneg _
    · exact fun x _ => norm_nonneg _
-- 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
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hp_pos : 0 < p
hn : (∫⁻ (a : α), enorm (E := ℝ) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖) ^ p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i
h_nnnorm_nonneg :
  Eq.{u_1 + 1} (α := (a : α) → ℝ≥0∞)
    (fun (a : α) ↦ enorm (E := ℝ) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖) ^ p) fun (a : α) ↦
    HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p
⊢ (∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i
have rwa : ∀
  (hn :
    (∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p ∂μ) ^ p⁻¹ ≤
      ∑' (i : ℕ), B i)
  (h_nnnorm_nonneg :
    Eq.{u_1 + 1} (α := (a : α) → ℝ≥0∞)
      (fun (a : α) ↦ enorm (E := ℝ) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖) ^ p) fun (a : α) ↦
      HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p),
  (∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i
Tactic: rwa [h_nnnorm_nonneg] at hn
Cleared hypotheses: hn, h_nnnorm_nonneg
-- 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∞
h :
  ∀ (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
have hp_pos : 0 < p
Tactic: have hp_pos : 0 < p := zero_lt_one.trans_le hp1
-- 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∞
h :
  ∀ (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
hp_pos : 0 < p
h_pow :
  ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖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
have rwa : (∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i
Tactic: rwa [one_div, ← ENNReal.le_rpow_inv_iff (by simp [hp_pos] : 0 < p⁻¹), inv_inv]
-- 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∞
h :
  ∀ (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
hp_pos : 0 < p
h_pow :
  ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ ≤
    HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p
rwa : (∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i
⊢ (∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i
have rwa₁ : ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ ≤
  HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p⁻¹⁻¹
Tactic: rwa [one_div, ← ENNReal.le_rpow_inv_iff (by simp [hp_pos] : 0 < p⁻¹), inv_inv]
-- 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∞
h :
  ∀ (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
hp_pos : 0 < p
⊢ (∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i
have suffices : ∫⁻ (a : α), HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) p ∂μ ≤ HPow.hPow (α := ℝ≥0∞) (∑' (i : ℕ), B i) p
Tactic: suffices h_pow : (∫⁻ a, (∑' i, ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ) ≤ (∑' i, B i) ^ p by
      rwa [one_div, ← ENNReal.le_rpow_inv_iff (by simp [hp_pos] : 0 < p⁻¹), inv_inv]
-- 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∞
h :
  ∀ (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
hp_pos : 0 < p
g : ℕ → ℝ≥0∞
⊢ Eq (α := ℝ≥0∞) (∑' (i : ℕ), g i) (liminf (fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), g i) atTop)
have rw : Eq (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, g i) atTop)
  (liminf (fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), g i) atTop)
Tactic: rw [ENNReal.tsum_eq_liminf_sum_nat, ← liminf_nat_add _ 1]
-- 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∞
h :
  ∀ (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
hp_pos : 0 < p
g : ℕ → ℝ≥0∞
rw :
  Eq (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, g i) atTop)
    (liminf (fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), g i) atTop)
⊢ Eq (α := ℝ≥0∞) (∑' (i : ℕ), g i) (liminf (fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), g i) atTop)
have rw₁ : Eq (α := ℝ≥0∞) (liminf (fun (i : ℕ) ↦ ∑ i ∈ Finset.range (i + 1), g i) atTop)
  (liminf (fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), g i) atTop)
Tactic: rw [ENNReal.tsum_eq_liminf_sum_nat, ← liminf_nat_add _ 1]