-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem eLpNorm'_sum_norm_sub_le_tsum_of_cauchy_eLpNorm' {f : ℕ → α → E}
    (hf : ∀ n, AEStronglyMeasurable (f n) μ) {p : ℝ} (hp1 : 1 ≤ p) {B : ℕ → ℝ≥0∞}
    (h_cau : ∀ N n m : ℕ, N ≤ n → N ≤ m → eLpNorm' (f n - f m) p μ < B N) (n : ℕ) :
    eLpNorm' (fun x => ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖) p μ ≤ ∑' i, B i

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm' (f n - f m) p μ < B N
n : ℕ
f_norm_diff : ℕ → α → ℝ := fun i x => ‖f (i + 1) x - f i x‖
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
⊢ ∑ x ∈ Finset.range (n + 1), eLpNorm' (f (x + 1) - f x) p μ ≤ ∑' (i : ℕ), B i

Tactic:
refine (Finset.sum_le_sum ?_).trans (sum_le_tsum _ (fun m _ => zero_le _) ENNReal.summable)

Result:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm' (f n - f m) p μ < B N
n : ℕ
f_norm_diff : ℕ → α → ℝ := fun i x => ‖f (i + 1) x - f i x‖
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
⊢ ∀ i ∈ Finset.range (n + 1), eLpNorm' (f (i + 1) - f i) p μ ≤ B i

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm' (f n - f m) p μ < B N
n : ℕ
f_norm_diff : ℕ → α → ℝ := fun i x => ‖f (i + 1) x - f i x‖
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
⊢ ∑ i ∈ Finset.range (n + 1), eLpNorm' (fun x => ‖(f (i + 1) - f i) x‖) p μ ≤ ∑' (i : ℕ), B i

Tactic:
simp_rw [eLpNorm'_norm]

Result:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm' (f n - f m) p μ < B N
n : ℕ
f_norm_diff : ℕ → α → ℝ := fun i x => ‖f (i + 1) x - f i x‖
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
⊢ ∑ x ∈ Finset.range (n + 1), eLpNorm' (f (x + 1) - f x) p μ ≤ ∑' (i : ℕ), B i

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm' (f n - f m) p μ < B N
n : ℕ
f_norm_diff : ℕ → α → ℝ := fun i x => ‖f (i + 1) x - f i x‖
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
⊢ ∀ i ∈ Finset.range (n + 1), eLpNorm' (f (i + 1) - f i) p μ ≤ B i

Tactic:
exact fun m _ => (h_cau m (m + 1) m (Nat.le_succ m) (le_refl m)).le

Result:
no goals

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm' (f n - f m) p μ < B N
n : ℕ
f_norm_diff : ℕ → α → ℝ := fun i x => ‖f (i + 1) x - f i x‖
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
⊢ eLpNorm' (∑ i ∈ Finset.range (n + 1), f_norm_diff i) p μ ≤ ∑' (i : ℕ), B i

Tactic:
refine (eLpNorm'_sum_le (fun i _ => ((hf (i + 1)).sub (hf i)).norm) hp1).trans ?_

Result:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm' (f n - f m) p μ < B N
n : ℕ
f_norm_diff : ℕ → α → ℝ := fun i x => ‖f (i + 1) x - f i x‖
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
⊢ ∑ i ∈ Finset.range (n + 1), eLpNorm' (fun x => ‖(f (i + 1) - f i) x‖) p μ ≤ ∑' (i : ℕ), B i

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm' (f n - f m) p μ < B N
n✝ : ℕ
f_norm_diff : ℕ → α → ℝ := fun i x => ‖f (i + 1) x - f i x‖
n : ℕ
x : α
⊢ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖ = (∑ i ∈ Finset.range (n + 1), f_norm_diff i) x

Tactic:
simp [f_norm_diff]

Result:
no goals

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm' (f n - f m) p μ < B N
n : ℕ
f_norm_diff : ℕ → α → ℝ := 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

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]

Result:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm' (f n - f m) p μ < B N
n : ℕ
f_norm_diff : ℕ → α → ℝ := fun i x => ‖f (i + 1) x - f i x‖
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
⊢ eLpNorm' (fun x => ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖) p μ ≤ ∑' (i : ℕ), B i

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm' (f n - f m) p μ < B N
n : ℕ
⊢ eLpNorm' (fun x => ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖) p μ ≤ ∑' (i : ℕ), B i

Tactic:
let f_norm_diff i x := ‖f (i + 1) x - f i x‖

Result:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm' (f n - f m) p μ < B N
n : ℕ
f_norm_diff : ℕ → α → ℝ := 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