α : Type u_1
E : Type ?u.1597979
F : Type u_2
G : Type ?u.1597985
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
p q : ℝ
hq_pos : 0 < q
⊢ (∫⁻ (a : α), ↑‖‖f a‖ ^ q‖₊ ^ p ∂μ) ^ (1 / p) = ((∫⁻ (a : α), ↑‖f a‖₊ ^ (p * q) ∂μ) ^ (1 / (p * q))) ^ q
α : Type u_1
E : Type ?u.1597979
F : Type u_2
G : Type ?u.1597985
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
p q : ℝ
hq_pos : 0 < q
⊢ snorm' (fun x => ‖f x‖ ^ q) p μ = snorm' f (p * q) μ ^ q
simp_rw [snorm']
α : Type u_1
E : Type ?u.1597979
F : Type u_2
G : Type ?u.1597985
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
p q : ℝ
hq_pos : 0 < q
⊢ (∫⁻ (a : α), ↑‖‖f a‖ ^ q‖₊ ^ p ∂μ) ^ (1 / p) = (∫⁻ (a : α), ↑‖f a‖₊ ^ (p * q) ∂μ) ^ (1 / p * (1 / q) * q)
α : Type u_1
E : Type ?u.1597979
F : Type u_2
G : Type ?u.1597985
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
p q : ℝ
hq_pos : 0 < q
⊢ (∫⁻ (a : α), ↑‖‖f a‖ ^ q‖₊ ^ p ∂μ) ^ (1 / p) = ((∫⁻ (a : α), ↑‖f a‖₊ ^ (p * q) ∂μ) ^ (1 / (p * q))) ^ q
rw [← ENNReal.rpow_mul, ← one_div_mul_one_div]
α : Type u_1
E : Type ?u.1597979
F : Type u_2
G : Type ?u.1597985
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
p q : ℝ
hq_pos : 0 < q
⊢ (∫⁻ (a : α), ↑‖‖f a‖ ^ q‖₊ ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ↑‖f a‖₊ ^ (p * q) ∂μ) ^ (p⁻¹ * q⁻¹ * q)
α : Type u_1
E : Type ?u.1597979
F : Type u_2
G : Type ?u.1597985
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
p q : ℝ
hq_pos : 0 < q
⊢ (∫⁻ (a : α), ↑‖‖f a‖ ^ q‖₊ ^ p ∂μ) ^ (1 / p) = (∫⁻ (a : α), ↑‖f a‖₊ ^ (p * q) ∂μ) ^ (1 / p * (1 / q) * q)
simp_rw [one_div]
α : Type u_1
E : Type ?u.1597979
F : Type u_2
G : Type ?u.1597985
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
p q : ℝ
hq_pos : 0 < q
⊢ (∫⁻ (a : α), ↑‖‖f a‖ ^ q‖₊ ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ↑‖f a‖₊ ^ (p * q) ∂μ) ^ p⁻¹
α : Type u_1
E : Type ?u.1597979
F : Type u_2
G : Type ?u.1597985
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
p q : ℝ
hq_pos : 0 < q
⊢ (∫⁻ (a : α), ↑‖‖f a‖ ^ q‖₊ ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ↑‖f a‖₊ ^ (p * q) ∂μ) ^ (p⁻¹ * q⁻¹ * q)
rw [mul_assoc, inv_mul_cancel hq_pos.ne.symm, mul_one]
case e_a.e_f
α : Type u_1
E : Type ?u.1597979
F : Type u_2
G : Type ?u.1597985
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
p q : ℝ
hq_pos : 0 < q
⊢ (fun a => ↑‖‖f a‖ ^ q‖₊ ^ p) = fun a => ↑‖f a‖₊ ^ (p * q)
α : Type u_1
E : Type ?u.1597979
F : Type u_2
G : Type ?u.1597985
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
p q : ℝ
hq_pos : 0 < q
⊢ (∫⁻ (a : α), ↑‖‖f a‖ ^ q‖₊ ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ↑‖f a‖₊ ^ (p * q) ∂μ) ^ p⁻¹
congr
case e_a.e_f.h
α : Type u_1
E : Type ?u.1597979
F : Type u_2
G : Type ?u.1597985
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
p q : ℝ
hq_pos : 0 < q
x : α
⊢ ↑‖‖f x‖ ^ q‖₊ ^ p = ↑‖f x‖₊ ^ (p * q)
case e_a.e_f
α : Type u_1
E : Type ?u.1597979
F : Type u_2
G : Type ?u.1597985
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
p q : ℝ
hq_pos : 0 < q
⊢ (fun a => ↑‖‖f a‖ ^ q‖₊ ^ p) = fun a => ↑‖f a‖₊ ^ (p * q)
ext1 x
case e_a.e_f.h
α : Type u_1
E : Type ?u.1597979
F : Type u_2
G : Type ?u.1597985
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
p q : ℝ
hq_pos : 0 < q
x : α
⊢ ENNReal.ofReal ‖‖f x‖ ^ q‖ ^ p = ENNReal.ofReal ‖f x‖ ^ (p * q)
case e_a.e_f.h
α : Type u_1
E : Type ?u.1597979
F : Type u_2
G : Type ?u.1597985
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
p q : ℝ
hq_pos : 0 < q
x : α
⊢ ↑‖‖f x‖ ^ q‖₊ ^ p = ↑‖f x‖₊ ^ (p * q)
simp_rw [← ofReal_norm_eq_coe_nnnorm]
no goals
case e_a.e_f.h
α : Type u_1
E : Type ?u.1597979
F : Type u_2
G : Type ?u.1597985
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
p q : ℝ
hq_pos : 0 < q
x : α
⊢ ENNReal.ofReal ‖‖f x‖ ^ q‖ ^ p = ENNReal.ofReal ‖f x‖ ^ (p * q)
rw [Real.norm_eq_abs, abs_eq_self.mpr (Real.rpow_nonneg_of_nonneg (norm_nonneg _) _), mul_comm, ←
  ENNReal.ofReal_rpow_of_nonneg (norm_nonneg _) hq_pos.le, ENNReal.rpow_mul]