α : Type u_1
E : Type u_2
F : Type ?u.8156900
G : Type ?u.8156903
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hn : snorm' (fun x => ∑ i in Finset.range (n + 1), ‖f (i + 1) x - f i x‖) p μ ≤ ∑' (i : ℕ), B i
hp_pos : 0 < p
⊢ (∫⁻ (a : α), (∑ i in Finset.range (n + 1), ↑‖f (i + 1) a - f i a‖₊) ^ p ∂μ) ≤ (∑' (i : ℕ), B i) ^ p
α : Type u_1
E : Type u_2
F : Type ?u.8156900
G : Type ?u.8156903
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hn : snorm' (fun x => ∑ i in Finset.range (n + 1), ‖f (i + 1) x - f i x‖) p μ ≤ ∑' (i : ℕ), B i
⊢ (∫⁻ (a : α), (∑ i in Finset.range (n + 1), ↑‖f (i + 1) a - f i a‖₊) ^ p ∂μ) ≤ (∑' (i : ℕ), B i) ^ p
have hp_pos : 0 < p := zero_lt_one.trans_le hp1
α : Type u_1
E : Type u_2
F : Type ?u.8156900
G : Type ?u.8156903
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hn : snorm' (fun x => ∑ i in Finset.range (n + 1), ‖f (i + 1) x - f i x‖) p μ ≤ ∑' (i : ℕ), B i
hp_pos : 0 < p
⊢ (∫⁻ (a : α), (∑ i in Finset.range (n + 1), ↑‖f (i + 1) a - f i a‖₊) ^ p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i
α : Type u_1
E : Type u_2
F : Type ?u.8156900
G : Type ?u.8156903
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hn : snorm' (fun x => ∑ i in Finset.range (n + 1), ‖f (i + 1) x - f i x‖) p μ ≤ ∑' (i : ℕ), B i
hp_pos : 0 < p
⊢ (∫⁻ (a : α), (∑ i in Finset.range (n + 1), ↑‖f (i + 1) a - f i a‖₊) ^ p ∂μ) ≤ (∑' (i : ℕ), B i) ^ p
rw [← one_div_one_div p, @ENNReal.le_rpow_one_div_iff _ _ (1 / p) (by simp [hp_pos]),
  one_div_one_div p]
α : Type u_1
E : Type u_2
F : Type ?u.8156900
G : Type ?u.8156903
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hn : (∫⁻ (a : α), ↑‖∑ i in Finset.range (n + 1), ‖f (i + 1) a - f i a‖‖₊ ^ p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i
hp_pos : 0 < p
⊢ (∫⁻ (a : α), (∑ i in Finset.range (n + 1), ↑‖f (i + 1) a - f i a‖₊) ^ p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i
α : Type u_1
E : Type u_2
F : Type ?u.8156900
G : Type ?u.8156903
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hn : snorm' (fun x => ∑ i in Finset.range (n + 1), ‖f (i + 1) x - f i x‖) p μ ≤ ∑' (i : ℕ), B i
hp_pos : 0 < p
⊢ (∫⁻ (a : α), (∑ i in Finset.range (n + 1), ↑‖f (i + 1) a - f i a‖₊) ^ p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i
simp_rw [snorm'] at hn
α : Type u_1
E : Type u_2
F : Type ?u.8156900
G : Type ?u.8156903
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hp_pos : 0 < p
h_nnnorm_nonneg :
  (fun a => ↑‖∑ i in Finset.range (n + 1), ‖f (i + 1) a - f i a‖‖₊ ^ p) = fun a =>
    (∑ i in Finset.range (n + 1), ↑‖f (i + 1) a - f i a‖₊) ^ p
hn :
  (∫⁻ (a : α), (fun x => ↑‖∑ i in Finset.range (n + 1), ‖f (i + 1) x - f i x‖‖₊ ^ p) a ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i
⊢ (∫⁻ (a : α), (∑ i in Finset.range (n + 1), ↑‖f (i + 1) a - f i a‖₊) ^ p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i
α : Type u_1
E : Type u_2
F : Type ?u.8156900
G : Type ?u.8156903
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hn : (∫⁻ (a : α), ↑‖∑ i in Finset.range (n + 1), ‖f (i + 1) a - f i a‖‖₊ ^ p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i
hp_pos : 0 < p
h_nnnorm_nonneg :
  (fun a => ↑‖∑ i in Finset.range (n + 1), ‖f (i + 1) a - f i a‖‖₊ ^ p) = fun a =>
    (∑ i in Finset.range (n + 1), ↑‖f (i + 1) a - f i a‖₊) ^ p
⊢ (∫⁻ (a : α), (∑ i in Finset.range (n + 1), ↑‖f (i + 1) a - f i a‖₊) ^ p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i
change
  (∫⁻ a, (fun x => ↑‖∑ i in Finset.range (n + 1), ‖f (i + 1) x - f i x‖‖₊ ^ p) a ∂μ) ^ (1 / p) ≤
    ∑' i, B i at hn
no goals
α : Type u_1
E : Type u_2
F : Type ?u.8156900
G : Type ?u.8156903
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hp_pos : 0 < p
h_nnnorm_nonneg :
  (fun a => ↑‖∑ i in Finset.range (n + 1), ‖f (i + 1) a - f i a‖‖₊ ^ p) = fun a =>
    (∑ i in Finset.range (n + 1), ↑‖f (i + 1) a - f i a‖₊) ^ p
hn :
  (∫⁻ (a : α), (fun x => ↑‖∑ i in Finset.range (n + 1), ‖f (i + 1) x - f i x‖‖₊ ^ p) a ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i
⊢ (∫⁻ (a : α), (∑ i in Finset.range (n + 1), ↑‖f (i + 1) a - f i a‖₊) ^ p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i
rwa [h_nnnorm_nonneg] at hn
no goals
α : Type u_1
E : Type u_2
F : Type ?u.8156900
G : Type ?u.8156903
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hn : snorm' (fun x => ∑ i in Finset.range (n + 1), ‖f (i + 1) x - f i x‖) p μ ≤ ∑' (i : ℕ), B i
hp_pos : 0 < p
⊢ 0 < 1 / p
simp [hp_pos]
case h
α : Type u_1
E : Type u_2
F : Type ?u.8156900
G : Type ?u.8156903
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hn : (∫⁻ (a : α), ↑‖∑ i in Finset.range (n + 1), ‖f (i + 1) a - f i a‖‖₊ ^ p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i
hp_pos : 0 < p
a : α
⊢ ↑‖∑ i in Finset.range (n + 1), ‖f (i + 1) a - f i a‖‖₊ ^ p =
    (∑ i in Finset.range (n + 1), ↑‖f (i + 1) a - f i a‖₊) ^ p
α : Type u_1
E : Type u_2
F : Type ?u.8156900
G : Type ?u.8156903
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hn : (∫⁻ (a : α), ↑‖∑ i in Finset.range (n + 1), ‖f (i + 1) a - f i a‖‖₊ ^ p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i
hp_pos : 0 < p
⊢ (fun a => ↑‖∑ i in Finset.range (n + 1), ‖f (i + 1) a - f i a‖‖₊ ^ p) = fun a =>
    (∑ i in Finset.range (n + 1), ↑‖f (i + 1) a - f i a‖₊) ^ p
ext1 a
case h.e_a
α : Type u_1
E : Type u_2
F : Type ?u.8156900
G : Type ?u.8156903
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hn : (∫⁻ (a : α), ↑‖∑ i in Finset.range (n + 1), ‖f (i + 1) a - f i a‖‖₊ ^ p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i
hp_pos : 0 < p
a : α
⊢ ↑‖∑ i in Finset.range (n + 1), ‖f (i + 1) a - f i a‖‖₊ = ∑ i in Finset.range (n + 1), ↑‖f (i + 1) a - f i a‖₊
case h
α : Type u_1
E : Type u_2
F : Type ?u.8156900
G : Type ?u.8156903
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hn : (∫⁻ (a : α), ↑‖∑ i in Finset.range (n + 1), ‖f (i + 1) a - f i a‖‖₊ ^ p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i
hp_pos : 0 < p
a : α
⊢ ↑‖∑ i in Finset.range (n + 1), ‖f (i + 1) a - f i a‖‖₊ ^ p =
    (∑ i in Finset.range (n + 1), ↑‖f (i + 1) a - f i a‖₊) ^ p
congr
case h.e_a
α : Type u_1
E : Type u_2
F : Type ?u.8156900
G : Type ?u.8156903
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hn : (∫⁻ (a : α), ↑‖∑ i in Finset.range (n + 1), ‖f (i + 1) a - f i a‖‖₊ ^ p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i
hp_pos : 0 < p
a : α
⊢ ENNReal.ofReal ‖∑ i in Finset.range (n + 1), ‖f (i + 1) a - f i a‖‖ =
    ∑ x in Finset.range (n + 1), ENNReal.ofReal ‖f (x + 1) a - f x a‖
case h.e_a
α : Type u_1
E : Type u_2
F : Type ?u.8156900
G : Type ?u.8156903
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hn : (∫⁻ (a : α), ↑‖∑ i in Finset.range (n + 1), ‖f (i + 1) a - f i a‖‖₊ ^ p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i
hp_pos : 0 < p
a : α
⊢ ↑‖∑ i in Finset.range (n + 1), ‖f (i + 1) a - f i a‖‖₊ = ∑ i in Finset.range (n + 1), ↑‖f (i + 1) a - f i a‖₊
simp_rw [← ofReal_norm_eq_coe_nnnorm]
case h.e_a
α : Type u_1
E : Type u_2
F : Type ?u.8156900
G : Type ?u.8156903
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hn : (∫⁻ (a : α), ↑‖∑ i in Finset.range (n + 1), ‖f (i + 1) a - f i a‖‖₊ ^ p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i
hp_pos : 0 < p
a : α
⊢ ENNReal.ofReal ‖∑ i in Finset.range (n + 1), ‖f (i + 1) a - f i a‖‖ =
    ENNReal.ofReal (∑ i in Finset.range (n + 1), ‖f (i + 1) a - f i a‖)

case h.e_a
α : Type u_1
E : Type u_2
F : Type ?u.8156900
G : Type ?u.8156903
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hn : (∫⁻ (a : α), ↑‖∑ i in Finset.range (n + 1), ‖f (i + 1) a - f i a‖‖₊ ^ p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i
hp_pos : 0 < p
a : α
⊢ ∀ (i : ℕ), i ∈ Finset.range (n + 1) → 0 ≤ ‖f (i + 1) a - f i a‖
case h.e_a
α : Type u_1
E : Type u_2
F : Type ?u.8156900
G : Type ?u.8156903
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hn : (∫⁻ (a : α), ↑‖∑ i in Finset.range (n + 1), ‖f (i + 1) a - f i a‖‖₊ ^ p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i
hp_pos : 0 < p
a : α
⊢ ENNReal.ofReal ‖∑ i in Finset.range (n + 1), ‖f (i + 1) a - f i a‖‖ =
    ∑ x in Finset.range (n + 1), ENNReal.ofReal ‖f (x + 1) a - f x a‖
rw [← ENNReal.ofReal_sum_of_nonneg]
α : Type u_1
E : Type u_2
F : Type ?u.8156900
G : Type ?u.8156903
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hn : (∫⁻ (a : α), ↑‖∑ i in Finset.range (n + 1), ‖f (i + 1) a - f i a‖‖₊ ^ p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i
hp_pos : 0 < p
a : α
⊢ 0 ≤ ∑ i in Finset.range (n + 1), ‖f (i + 1) a - f i a‖
case h.e_a
α : Type u_1
E : Type u_2
F : Type ?u.8156900
G : Type ?u.8156903
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hn : (∫⁻ (a : α), ↑‖∑ i in Finset.range (n + 1), ‖f (i + 1) a - f i a‖‖₊ ^ p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i
hp_pos : 0 < p
a : α
⊢ ENNReal.ofReal ‖∑ i in Finset.range (n + 1), ‖f (i + 1) a - f i a‖‖ =
    ENNReal.ofReal (∑ i in Finset.range (n + 1), ‖f (i + 1) a - f i a‖)
rw [Real.norm_of_nonneg _]
no goals
α : Type u_1
E : Type u_2
F : Type ?u.8156900
G : Type ?u.8156903
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hn : (∫⁻ (a : α), ↑‖∑ i in Finset.range (n + 1), ‖f (i + 1) a - f i a‖‖₊ ^ p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i
hp_pos : 0 < p
a : α
⊢ 0 ≤ ∑ i in Finset.range (n + 1), ‖f (i + 1) a - f i a‖
exact Finset.sum_nonneg fun x _ => norm_nonneg _
no goals
case h.e_a
α : Type u_1
E : Type u_2
F : Type ?u.8156900
G : Type ?u.8156903
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hn : (∫⁻ (a : α), ↑‖∑ i in Finset.range (n + 1), ‖f (i + 1) a - f i a‖‖₊ ^ p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i
hp_pos : 0 < p
a : α
⊢ ∀ (i : ℕ), i ∈ Finset.range (n + 1) → 0 ≤ ‖f (i + 1) a - f i a‖
exact fun x _ => norm_nonneg _