case pos
α : Type u_1
E : Type ?u.1675097
F : Type u_2
G : Type ?u.1675103
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hq_pos : 0 < q
h0 : p = 0
⊢ snorm (fun x => ‖f x‖ ^ q) p μ = snorm f (p * ENNReal.ofReal q) μ ^ q

case neg
α : Type u_1
E : Type ?u.1675097
F : Type u_2
G : Type ?u.1675103
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
⊢ snorm (fun x => ‖f x‖ ^ q) p μ = snorm f (p * ENNReal.ofReal q) μ ^ q
α : Type u_1
E : Type ?u.1675097
F : Type u_2
G : Type ?u.1675103
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hq_pos : 0 < q
⊢ snorm (fun x => ‖f x‖ ^ q) p μ = snorm f (p * ENNReal.ofReal q) μ ^ q
by_cases h0 : p = 0
case pos
α : Type u_1
E : Type ?u.1675097
F : Type u_2
G : Type ?u.1675103
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : p = ⊤
⊢ snorm (fun x => ‖f x‖ ^ q) p μ = snorm f (p * ENNReal.ofReal q) μ ^ q

case neg
α : Type u_1
E : Type ?u.1675097
F : Type u_2
G : Type ?u.1675103
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ snorm (fun x => ‖f x‖ ^ q) p μ = snorm f (p * ENNReal.ofReal q) μ ^ q
case neg
α : Type u_1
E : Type ?u.1675097
F : Type u_2
G : Type ?u.1675103
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
⊢ snorm (fun x => ‖f x‖ ^ q) p μ = snorm f (p * ENNReal.ofReal q) μ ^ q
by_cases hp_top : p = ∞
case neg
α : Type u_1
E : Type ?u.1675097
F : Type u_2
G : Type ?u.1675103
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ snorm' (fun x => ‖f x‖ ^ q) (ENNReal.toReal p) μ = snorm' f (ENNReal.toReal (p * ENNReal.ofReal q)) μ ^ q

α : Type u_1
E : Type ?u.1675097
F : Type u_2
G : Type ?u.1675103
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ p * ENNReal.ofReal q ≠ 0

α : Type u_1
E : Type ?u.1675097
F : Type u_2
G : Type ?u.1675103
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ p * ENNReal.ofReal q ≠ ⊤
case neg
α : Type u_1
E : Type ?u.1675097
F : Type u_2
G : Type ?u.1675103
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ snorm (fun x => ‖f x‖ ^ q) p μ = snorm f (p * ENNReal.ofReal q) μ ^ q
rw [snorm_eq_snorm' h0 hp_top, snorm_eq_snorm' _ _]
α : Type u_1
E : Type ?u.1675097
F : Type u_2
G : Type ?u.1675103
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ p * ENNReal.ofReal q ≠ 0

case neg
α : Type u_1
E : Type ?u.1675097
F : Type u_2
G : Type ?u.1675103
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ snorm' (fun x => ‖f x‖ ^ q) (ENNReal.toReal p) μ = snorm' f (ENNReal.toReal (p * ENNReal.ofReal q)) μ ^ q

α : Type u_1
E : Type ?u.1675097
F : Type u_2
G : Type ?u.1675103
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ p * ENNReal.ofReal q ≠ ⊤
case neg
α : Type u_1
E : Type ?u.1675097
F : Type u_2
G : Type ?u.1675103
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ snorm' (fun x => ‖f x‖ ^ q) (ENNReal.toReal p) μ = snorm' f (ENNReal.toReal (p * ENNReal.ofReal q)) μ ^ q

α : Type u_1
E : Type ?u.1675097
F : Type u_2
G : Type ?u.1675103
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ p * ENNReal.ofReal q ≠ 0

α : Type u_1
E : Type ?u.1675097
F : Type u_2
G : Type ?u.1675103
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ p * ENNReal.ofReal q ≠ ⊤
swap
α : Type u_1
E : Type ?u.1675097
F : Type u_2
G : Type ?u.1675103
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ p * ENNReal.ofReal q ≠ ⊤

case neg
α : Type u_1
E : Type ?u.1675097
F : Type u_2
G : Type ?u.1675103
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ snorm' (fun x => ‖f x‖ ^ q) (ENNReal.toReal p) μ = snorm' f (ENNReal.toReal (p * ENNReal.ofReal q)) μ ^ q
case neg
α : Type u_1
E : Type ?u.1675097
F : Type u_2
G : Type ?u.1675103
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ snorm' (fun x => ‖f x‖ ^ q) (ENNReal.toReal p) μ = snorm' f (ENNReal.toReal (p * ENNReal.ofReal q)) μ ^ q

α : Type u_1
E : Type ?u.1675097
F : Type u_2
G : Type ?u.1675103
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ p * ENNReal.ofReal q ≠ ⊤
swap
case neg
α : Type u_1
E : Type ?u.1675097
F : Type u_2
G : Type ?u.1675103
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ snorm' (fun x => ‖f x‖ ^ q) (ENNReal.toReal p) μ = snorm' f (ENNReal.toReal p * q) μ ^ q
case neg
α : Type u_1
E : Type ?u.1675097
F : Type u_2
G : Type ?u.1675103
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ snorm' (fun x => ‖f x‖ ^ q) (ENNReal.toReal p) μ = snorm' f (ENNReal.toReal (p * ENNReal.ofReal q)) μ ^ q
rw [ENNReal.toReal_mul, ENNReal.toReal_ofReal hq_pos.le]
no goals
case neg
α : Type u_1
E : Type ?u.1675097
F : Type u_2
G : Type ?u.1675103
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ snorm' (fun x => ‖f x‖ ^ q) (ENNReal.toReal p) μ = snorm' f (ENNReal.toReal p * q) μ ^ q
exact snorm'_norm_rpow f p.toReal q hq_pos
no goals
case pos
α : Type u_1
E : Type ?u.1675097
F : Type u_2
G : Type ?u.1675103
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hq_pos : 0 < q
h0 : p = 0
⊢ snorm (fun x => ‖f x‖ ^ q) p μ = snorm f (p * ENNReal.ofReal q) μ ^ q
simp [h0, ENNReal.zero_rpow_of_pos hq_pos]
case pos
α : Type u_1
E : Type ?u.1675097
F : Type u_2
G : Type ?u.1675103
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : p = ⊤
⊢ essSup (fun x => ↑‖‖f x‖ ^ q‖₊) μ = essSup (fun x => ↑‖f x‖₊) μ ^ q
case pos
α : Type u_1
E : Type ?u.1675097
F : Type u_2
G : Type ?u.1675103
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : p = ⊤
⊢ snorm (fun x => ‖f x‖ ^ q) p μ = snorm f (p * ENNReal.ofReal q) μ ^ q
simp only [hp_top, snorm_exponent_top, ENNReal.top_mul', hq_pos.not_le, ENNReal.ofReal_eq_zero,
  if_false, snorm_exponent_top, snormEssSup]
case pos
α : Type u_1
E : Type ?u.1675097
F : Type u_2
G : Type ?u.1675103
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : p = ⊤
h_rpow : essSup (fun x => ↑‖‖f x‖ ^ q‖₊) μ = essSup (fun x => ↑‖f x‖₊ ^ q) μ
⊢ essSup (fun x => ↑‖‖f x‖ ^ q‖₊) μ = essSup (fun x => ↑‖f x‖₊) μ ^ q
case pos
α : Type u_1
E : Type ?u.1675097
F : Type u_2
G : Type ?u.1675103
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : p = ⊤
⊢ essSup (fun x => ↑‖‖f x‖ ^ q‖₊) μ = essSup (fun x => ↑‖f x‖₊) μ ^ q
have h_rpow :
  essSup (fun x : α => (‖‖f x‖ ^ q‖₊ : ℝ≥0∞)) μ =
    essSup (fun x : α => (‖f x‖₊ : ℝ≥0∞) ^ q) μ := by
  congr
  ext1 x
  conv_rhs => rw [← nnnorm_norm]
  rw [ENNReal.coe_rpow_of_nonneg _ hq_pos.le, ENNReal.coe_eq_coe]
  ext
  push_cast
  rw [Real.norm_rpow_of_nonneg (norm_nonneg _)]
case pos
α : Type u_1
E : Type ?u.1675097
F : Type u_2
G : Type ?u.1675103
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : p = ⊤
h_rpow : essSup (fun x => ↑‖‖f x‖ ^ q‖₊) μ = essSup (fun x => ↑‖f x‖₊ ^ q) μ
⊢ essSup (fun x => ↑‖f x‖₊ ^ q) μ = essSup (fun x => ↑‖f x‖₊) μ ^ q
case pos
α : Type u_1
E : Type ?u.1675097
F : Type u_2
G : Type ?u.1675103
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : p = ⊤
h_rpow : essSup (fun x => ↑‖‖f x‖ ^ q‖₊) μ = essSup (fun x => ↑‖f x‖₊ ^ q) μ
⊢ essSup (fun x => ↑‖‖f x‖ ^ q‖₊) μ = essSup (fun x => ↑‖f x‖₊) μ ^ q
rw [h_rpow]
case pos
α : Type u_1
E : Type ?u.1675097
F : Type u_2
G : Type ?u.1675103
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : p = ⊤
h_rpow : essSup (fun x => ↑‖‖f x‖ ^ q‖₊) μ = essSup (fun x => ↑‖f x‖₊ ^ q) μ
h_rpow_mono : StrictMono fun x => x ^ q
⊢ essSup (fun x => ↑‖f x‖₊ ^ q) μ = essSup (fun x => ↑‖f x‖₊) μ ^ q
case pos
α : Type u_1
E : Type ?u.1675097
F : Type u_2
G : Type ?u.1675103
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : p = ⊤
h_rpow : essSup (fun x => ↑‖‖f x‖ ^ q‖₊) μ = essSup (fun x => ↑‖f x‖₊ ^ q) μ
⊢ essSup (fun x => ↑‖f x‖₊ ^ q) μ = essSup (fun x => ↑‖f x‖₊) μ ^ q
have h_rpow_mono := ENNReal.strictMono_rpow_of_pos hq_pos
case pos
α : Type u_1
E : Type ?u.1675097
F : Type u_2
G : Type ?u.1675103
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : p = ⊤
h_rpow : essSup (fun x => ↑‖‖f x‖ ^ q‖₊) μ = essSup (fun x => ↑‖f x‖₊ ^ q) μ
h_rpow_mono : StrictMono fun x => x ^ q
h_rpow_surj : Function.Surjective fun y => y ^ q
⊢ essSup (fun x => ↑‖f x‖₊ ^ q) μ = essSup (fun x => ↑‖f x‖₊) μ ^ q
case pos
α : Type u_1
E : Type ?u.1675097
F : Type u_2
G : Type ?u.1675103
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : p = ⊤
h_rpow : essSup (fun x => ↑‖‖f x‖ ^ q‖₊) μ = essSup (fun x => ↑‖f x‖₊ ^ q) μ
h_rpow_mono : StrictMono fun x => x ^ q
⊢ essSup (fun x => ↑‖f x‖₊ ^ q) μ = essSup (fun x => ↑‖f x‖₊) μ ^ q
have h_rpow_surj := (ENNReal.rpow_left_bijective hq_pos.ne.symm).2
case pos
α : Type u_1
E : Type ?u.1675097
F : Type u_2
G : Type ?u.1675103
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : p = ⊤
h_rpow : essSup (fun x => ↑‖‖f x‖ ^ q‖₊) μ = essSup (fun x => ↑‖f x‖₊ ^ q) μ
h_rpow_mono : StrictMono fun x => x ^ q
h_rpow_surj : Function.Surjective fun y => y ^ q
iso : ℝ≥0∞ ≃o ℝ≥0∞ := StrictMono.orderIsoOfSurjective (fun x => x ^ q) h_rpow_mono h_rpow_surj
⊢ essSup (fun x => ↑‖f x‖₊ ^ q) μ = essSup (fun x => ↑‖f x‖₊) μ ^ q
case pos
α : Type u_1
E : Type ?u.1675097
F : Type u_2
G : Type ?u.1675103
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : p = ⊤
h_rpow : essSup (fun x => ↑‖‖f x‖ ^ q‖₊) μ = essSup (fun x => ↑‖f x‖₊ ^ q) μ
h_rpow_mono : StrictMono fun x => x ^ q
h_rpow_surj : Function.Surjective fun y => y ^ q
⊢ essSup (fun x => ↑‖f x‖₊ ^ q) μ = essSup (fun x => ↑‖f x‖₊) μ ^ q
let iso := h_rpow_mono.orderIsoOfSurjective _ h_rpow_surj
no goals
case pos
α : Type u_1
E : Type ?u.1675097
F : Type u_2
G : Type ?u.1675103
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : p = ⊤
h_rpow : essSup (fun x => ↑‖‖f x‖ ^ q‖₊) μ = essSup (fun x => ↑‖f x‖₊ ^ q) μ
h_rpow_mono : StrictMono fun x => x ^ q
h_rpow_surj : Function.Surjective fun y => y ^ q
iso : ℝ≥0∞ ≃o ℝ≥0∞ := StrictMono.orderIsoOfSurjective (fun x => x ^ q) h_rpow_mono h_rpow_surj
⊢ essSup (fun x => ↑‖f x‖₊ ^ q) μ = essSup (fun x => ↑‖f x‖₊) μ ^ q
exact (iso.essSup_apply (fun x => (‖f x‖₊ : ℝ≥0∞)) μ).symm
case e_f
α : Type u_1
E : Type ?u.1675097
F : Type u_2
G : Type ?u.1675103
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : p = ⊤
⊢ (fun x => ↑‖‖f x‖ ^ q‖₊) = fun x => ↑‖f x‖₊ ^ q
α : Type u_1
E : Type ?u.1675097
F : Type u_2
G : Type ?u.1675103
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : p = ⊤
⊢ essSup (fun x => ↑‖‖f x‖ ^ q‖₊) μ = essSup (fun x => ↑‖f x‖₊ ^ q) μ
congr
case e_f.h
α : Type u_1
E : Type ?u.1675097
F : Type u_2
G : Type ?u.1675103
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : p = ⊤
x : α
⊢ ↑‖‖f x‖ ^ q‖₊ = ↑‖f x‖₊ ^ q
case e_f
α : Type u_1
E : Type ?u.1675097
F : Type u_2
G : Type ?u.1675103
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : p = ⊤
⊢ (fun x => ↑‖‖f x‖ ^ q‖₊) = fun x => ↑‖f x‖₊ ^ q
ext1 x
case e_f.h
α : Type u_1
E : Type ?u.1675097
F : Type u_2
G : Type ?u.1675103
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : p = ⊤
x : α
⊢ ↑‖‖f x‖ ^ q‖₊ = ↑‖‖f x‖‖₊ ^ q
case e_f.h
α : Type u_1
E : Type ?u.1675097
F : Type u_2
G : Type ?u.1675103
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : p = ⊤
x : α
⊢ ↑‖‖f x‖ ^ q‖₊ = ↑‖f x‖₊ ^ q
conv_rhs => rw [← nnnorm_norm]
case e_f.h
α : Type u_1
E : Type ?u.1675097
F : Type u_2
G : Type ?u.1675103
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : p = ⊤
x : α
⊢ ‖‖f x‖ ^ q‖₊ = ‖‖f x‖‖₊ ^ q
case e_f.h
α : Type u_1
E : Type ?u.1675097
F : Type u_2
G : Type ?u.1675103
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : p = ⊤
x : α
⊢ ↑‖‖f x‖ ^ q‖₊ = ↑‖‖f x‖‖₊ ^ q
rw [ENNReal.coe_rpow_of_nonneg _ hq_pos.le, ENNReal.coe_eq_coe]
case e_f.h.a
α : Type u_1
E : Type ?u.1675097
F : Type u_2
G : Type ?u.1675103
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : p = ⊤
x : α
⊢ ↑‖‖f x‖ ^ q‖₊ = ↑(‖‖f x‖‖₊ ^ q)
case e_f.h
α : Type u_1
E : Type ?u.1675097
F : Type u_2
G : Type ?u.1675103
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : p = ⊤
x : α
⊢ ‖‖f x‖ ^ q‖₊ = ‖‖f x‖‖₊ ^ q
ext
case e_f.h.a
α : Type u_1
E : Type ?u.1675097
F : Type u_2
G : Type ?u.1675103
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : p = ⊤
x : α
⊢ ‖‖f x‖ ^ q‖ = ‖‖f x‖‖ ^ q
case e_f.h.a
α : Type u_1
E : Type ?u.1675097
F : Type u_2
G : Type ?u.1675103
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : p = ⊤
x : α
⊢ ↑‖‖f x‖ ^ q‖₊ = ↑(‖‖f x‖‖₊ ^ q)
push_cast
no goals
case e_f.h.a
α : Type u_1
E : Type ?u.1675097
F : Type u_2
G : Type ?u.1675103
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : p = ⊤
x : α
⊢ ‖‖f x‖ ^ q‖ = ‖‖f x‖‖ ^ q
rw [Real.norm_rpow_of_nonneg (norm_nonneg _)]
α : Type u_1
E : Type ?u.1675097
F : Type u_2
G : Type ?u.1675103
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ ENNReal.ofReal q ≠ 0
α : Type u_1
E : Type ?u.1675097
F : Type u_2
G : Type ?u.1675103
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ p * ENNReal.ofReal q ≠ 0
refine' mul_ne_zero h0 _
no goals
α : Type u_1
E : Type ?u.1675097
F : Type u_2
G : Type ?u.1675103
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ ENNReal.ofReal q ≠ 0
rwa [Ne.def, ENNReal.ofReal_eq_zero, not_le]
no goals
α : Type u_1
E : Type ?u.1675097
F : Type u_2
G : Type ?u.1675103
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ p * ENNReal.ofReal q ≠ ⊤
exact ENNReal.mul_ne_top hp_top ENNReal.ofReal_ne_top