-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem lintegral_rpow_sum_enorm_sub_le_rpow_tsum
    {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, (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ) ≤ (∑' i, B i) ^ p

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
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 : α), (∑ 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

Result:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hp_pos : 0 < p
hn : (∫⁻ (a : α), ‖∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖‖ₑ ^ p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i
⊢ (∫⁻ (a : α), (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
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
⊢ 0 < p⁻¹

Tactic:
simp [hp_pos]

Result:
no goals

Proof state:
case h.e_a
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hp_pos : 0 < p
hn : (∫⁻ (a : α), ‖∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖‖ₑ ^ p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i
a : α
⊢ ENNReal.ofReal ‖∑ 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 [Real.norm_of_nonneg _]

Result:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hp_pos : 0 < p
hn : (∫⁻ (a : α), ‖∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖‖ₑ ^ p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i
a : α
⊢ 0 ≤ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖

Proof state:
case h.e_a
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hp_pos : 0 < p
hn : (∫⁻ (a : α), ‖∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖‖ₑ ^ p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i
a : α
⊢ ENNReal.ofReal ‖∑ 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:
rw [← ENNReal.ofReal_sum_of_nonneg]

Result:
case h.e_a
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hp_pos : 0 < p
hn : (∫⁻ (a : α), ‖∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖‖ₑ ^ p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i
a : α
⊢ ENNReal.ofReal ‖∑ 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‖)

case h.e_a
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hp_pos : 0 < p
hn : (∫⁻ (a : α), ‖∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖‖ₑ ^ p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i
a : α
⊢ ∀ i ∈ Finset.range (n + 1), 0 ≤ ‖f (i + 1) a - f i a‖

Proof state:
case h
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hp_pos : 0 < p
hn : (∫⁻ (a : α), ‖∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖‖ₑ ^ p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i
a : α
⊢ ‖∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖‖ₑ ^ p = (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p

Tactic:
congr

Result:
case h.e_a
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hp_pos : 0 < p
hn : (∫⁻ (a : α), ‖∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖‖ₑ ^ p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i
a : α
⊢ ‖∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖‖ₑ = ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
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 : α), (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ ≤ (∑' (i : ℕ), B i) ^ p

Tactic:
rw [← inv_inv p, @ENNReal.le_rpow_inv_iff _ _ p⁻¹ (by simp [hp_pos]), inv_inv p]

Result:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
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 : α), (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hp_pos : 0 < p
hn : (∫⁻ (a : α), ‖∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖‖ₑ ^ p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i
⊢ (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

Tactic:
ext1 a

Result:
case h
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hp_pos : 0 < p
hn : (∫⁻ (a : α), ‖∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖‖ₑ ^ p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i
a : α
⊢ ‖∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖‖ₑ ^ p = (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hp_pos : 0 < p
hn : (∫⁻ (a : α), ‖∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖‖ₑ ^ p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i
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
⊢ (∫⁻ (a : α), (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i

Tactic:
rwa [h_nnnorm_nonneg] at hn

Result:
no goals

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hp_pos : 0 < p
hn : (∫⁻ (a : α), ‖∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖‖ₑ ^ p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i
a : α
⊢ 0 ≤ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖

Tactic:
exact Finset.sum_nonneg fun x _ => norm_nonneg _

Result:
no goals

Proof state:
case h.e_a
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hp_pos : 0 < p
hn : (∫⁻ (a : α), ‖∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖‖ₑ ^ p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i
a : α
⊢ ‖∑ 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:
simp_rw [← ofReal_norm_eq_enorm]

Result:
case h.e_a
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hp_pos : 0 < p
hn : (∫⁻ (a : α), ‖∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖‖ₑ ^ p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i
a : α
⊢ ENNReal.ofReal ‖∑ 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‖