α : Type u_1
E : Type u_2
F : Type ?u.720298
G : Type ?u.720301
m m0 : MeasurableSpace α
p : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
q : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ⊤
h : Memℒp (fun x => ‖f x‖ ^ ENNReal.toReal q) (p / q)
⊢ Memℒp f p
α : Type u_1
E : Type u_2
F : Type ?u.720298
G : Type ?u.720301
m m0 : MeasurableSpace α
p : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
q : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ⊤
⊢ Memℒp (fun x => ‖f x‖ ^ ENNReal.toReal q) (p / q) ↔ Memℒp f p
refine' ⟨fun h => _, fun h => h.norm_rpow_div q⟩
α : Type u_1
E : Type u_2
F : Type ?u.720298
G : Type ?u.720301
m m0 : MeasurableSpace α
p : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
q : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ⊤
h : Memℒp (fun x => ‖f x‖ ^ ENNReal.toReal q) (p / q)
⊢ Memℒp (fun x => ‖f x‖) p
α : Type u_1
E : Type u_2
F : Type ?u.720298
G : Type ?u.720301
m m0 : MeasurableSpace α
p : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
q : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ⊤
h : Memℒp (fun x => ‖f x‖ ^ ENNReal.toReal q) (p / q)
⊢ Memℒp f p
apply (memℒp_norm_iff hf).1
case h.e'_5
α : Type u_1
E : Type u_2
F : Type ?u.720298
G : Type ?u.720301
m m0 : MeasurableSpace α
p : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
q : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ⊤
h : Memℒp (fun x => ‖f x‖ ^ ENNReal.toReal q) (p / q)
⊢ (fun x => ‖f x‖) = fun x => ‖‖f x‖ ^ ENNReal.toReal q‖ ^ ENNReal.toReal q⁻¹

case h.e'_6
α : Type u_1
E : Type u_2
F : Type ?u.720298
G : Type ?u.720301
m m0 : MeasurableSpace α
p : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
q : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ⊤
h : Memℒp (fun x => ‖f x‖ ^ ENNReal.toReal q) (p / q)
⊢ p = p / q / q⁻¹
α : Type u_1
E : Type u_2
F : Type ?u.720298
G : Type ?u.720301
m m0 : MeasurableSpace α
p : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
q : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ⊤
h : Memℒp (fun x => ‖f x‖ ^ ENNReal.toReal q) (p / q)
⊢ Memℒp (fun x => ‖f x‖) p
convert h.norm_rpow_div q⁻¹ using 1
case h.e'_5.h
α : Type u_1
E : Type u_2
F : Type ?u.720298
G : Type ?u.720301
m m0 : MeasurableSpace α
p : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
q : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ⊤
h : Memℒp (fun x => ‖f x‖ ^ ENNReal.toReal q) (p / q)
x : α
⊢ ‖f x‖ = ‖‖f x‖ ^ ENNReal.toReal q‖ ^ ENNReal.toReal q⁻¹
case h.e'_5
α : Type u_1
E : Type u_2
F : Type ?u.720298
G : Type ?u.720301
m m0 : MeasurableSpace α
p : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
q : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ⊤
h : Memℒp (fun x => ‖f x‖ ^ ENNReal.toReal q) (p / q)
⊢ (fun x => ‖f x‖) = fun x => ‖‖f x‖ ^ ENNReal.toReal q‖ ^ ENNReal.toReal q⁻¹
ext x
case h.e'_5.h
α : Type u_1
E : Type u_2
F : Type ?u.720298
G : Type ?u.720301
m m0 : MeasurableSpace α
p : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
q : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ⊤
h : Memℒp (fun x => ‖f x‖ ^ ENNReal.toReal q) (p / q)
x : α
⊢ ENNReal.toReal q ≠ 0
case h.e'_5.h
α : Type u_1
E : Type u_2
F : Type ?u.720298
G : Type ?u.720301
m m0 : MeasurableSpace α
p : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
q : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ⊤
h : Memℒp (fun x => ‖f x‖ ^ ENNReal.toReal q) (p / q)
x : α
⊢ ‖f x‖ = ‖‖f x‖ ^ ENNReal.toReal q‖ ^ ENNReal.toReal q⁻¹
rw [Real.norm_eq_abs, Real.abs_rpow_of_nonneg (norm_nonneg _), ← Real.rpow_mul (abs_nonneg _),
  ENNReal.toReal_inv, mul_inv_cancel, abs_of_nonneg (norm_nonneg _), Real.rpow_one]
no goals
case h.e'_5.h
α : Type u_1
E : Type u_2
F : Type ?u.720298
G : Type ?u.720301
m m0 : MeasurableSpace α
p : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
q : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ⊤
h : Memℒp (fun x => ‖f x‖ ^ ENNReal.toReal q) (p / q)
x : α
⊢ ENNReal.toReal q ≠ 0
simp [ENNReal.toReal_eq_zero_iff, not_or, q_zero, q_top]
no goals
case h.e'_6
α : Type u_1
E : Type u_2
F : Type ?u.720298
G : Type ?u.720301
m m0 : MeasurableSpace α
p : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
q : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ⊤
h : Memℒp (fun x => ‖f x‖ ^ ENNReal.toReal q) (p / q)
⊢ p = p / q / q⁻¹
rw [div_eq_mul_inv, inv_inv, div_eq_mul_inv, mul_assoc, ENNReal.inv_mul_cancel q_zero q_top,
  mul_one]