α : Type u_1
E : Type ?u.953790
F : Type u_2
G : Type ?u.953796
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
c : F
hq_pos : 0 < q
⊢ (↑‖c‖₊ ^ q) ^ (1 / q) * ↑↑μ Set.univ ^ (1 / q) = ↑‖c‖₊ * ↑↑μ Set.univ ^ (1 / q)
α : Type u_1
E : Type ?u.953790
F : Type u_2
G : Type ?u.953796
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
c : F
hq_pos : 0 < q
⊢ snorm' (fun x => c) q μ = ↑‖c‖₊ * ↑↑μ Set.univ ^ (1 / q)
rw [snorm', lintegral_const, ENNReal.mul_rpow_of_nonneg _ _ (by simp [hq_pos.le] : 0 ≤ 1 / q)]
case e_a
α : Type u_1
E : Type ?u.953790
F : Type u_2
G : Type ?u.953796
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
c : F
hq_pos : 0 < q
⊢ (↑‖c‖₊ ^ q) ^ (1 / q) = ↑‖c‖₊
α : Type u_1
E : Type ?u.953790
F : Type u_2
G : Type ?u.953796
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
c : F
hq_pos : 0 < q
⊢ (↑‖c‖₊ ^ q) ^ (1 / q) * ↑↑μ Set.univ ^ (1 / q) = ↑‖c‖₊ * ↑↑μ Set.univ ^ (1 / q)
congr
case e_a
α : Type u_1
E : Type ?u.953790
F : Type u_2
G : Type ?u.953796
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
c : F
hq_pos : 0 < q
⊢ ↑‖c‖₊ ^ (q * (1 / q)) = ↑‖c‖₊
case e_a
α : Type u_1
E : Type ?u.953790
F : Type u_2
G : Type ?u.953796
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
c : F
hq_pos : 0 < q
⊢ (↑‖c‖₊ ^ q) ^ (1 / q) = ↑‖c‖₊
rw [← ENNReal.rpow_mul]
case e_a
α : Type u_1
E : Type ?u.953790
F : Type u_2
G : Type ?u.953796
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
c : F
hq_pos : 0 < q
hq_cancel : q * (1 / q) = 1
⊢ ↑‖c‖₊ ^ (q * (1 / q)) = ↑‖c‖₊

case hq_cancel
α : Type u_1
E : Type ?u.953790
F : Type u_2
G : Type ?u.953796
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
c : F
hq_pos : 0 < q
⊢ q * (1 / q) = 1
case e_a
α : Type u_1
E : Type ?u.953790
F : Type u_2
G : Type ?u.953796
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
c : F
hq_pos : 0 < q
⊢ ↑‖c‖₊ ^ (q * (1 / q)) = ↑‖c‖₊
suffices hq_cancel : q * (1 / q) = 1
no goals
case hq_cancel
α : Type u_1
E : Type ?u.953790
F : Type u_2
G : Type ?u.953796
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
c : F
hq_pos : 0 < q
⊢ q * (1 / q) = 1
rw [one_div, mul_inv_cancel (ne_of_lt hq_pos).symm]
no goals
α : Type u_1
E : Type ?u.953790
F : Type u_2
G : Type ?u.953796
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
c : F
hq_pos : 0 < q
⊢ 0 ≤ 1 / q
simp [hq_pos.le]
no goals
case e_a
α : Type u_1
E : Type ?u.953790
F : Type u_2
G : Type ?u.953796
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
c : F
hq_pos : 0 < q
hq_cancel : q * (1 / q) = 1
⊢ ↑‖c‖₊ ^ (q * (1 / q)) = ↑‖c‖₊
rw [hq_cancel, ENNReal.rpow_one]