-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem memLp_norm_rpow_iff {q : ℝ≥0∞} {f : α → E} (hf : AEStronglyMeasurable f μ) (q_zero : q ≠ 0)
    (q_top : q ≠ ∞) : MemLp (fun x : α => ‖f x‖ ^ q.toReal) (p / q) μ ↔ MemLp f p μ

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
q : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ⊤
h : MemLp (fun x => ‖f x‖ ^ q.toReal) (p / q) μ
⊢ MemLp f p μ

Tactic:
apply (memLp_norm_iff hf).1

Result:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
q : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ⊤
h : MemLp (fun x => ‖f x‖ ^ q.toReal) (p / q) μ
⊢ MemLp (fun x => ‖f x‖) p μ

Proof state:
case h.e'_6.h
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
q : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ⊤
h : MemLp (fun x => ‖f x‖ ^ q.toReal) (p / q) μ
x : α
⊢ q.toReal ≠ 0

Tactic:
simp [ENNReal.toReal_eq_zero_iff, not_or, q_zero, q_top]

Result:
no goals

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
q : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ⊤
⊢ MemLp (fun x => ‖f x‖ ^ q.toReal) (p / q) μ ↔ MemLp f p μ

Tactic:
refine ⟨fun h => ?_, fun h => h.norm_rpow_div q⟩

Result:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
q : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ⊤
h : MemLp (fun x => ‖f x‖ ^ q.toReal) (p / q) μ
⊢ MemLp f p μ

Proof state:
case h.e'_7
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
q : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ⊤
h : MemLp (fun x => ‖f x‖ ^ q.toReal) (p / q) μ
⊢ p = p / q / q⁻¹

Tactic:
rw [div_eq_mul_inv, inv_inv, div_eq_mul_inv, mul_assoc, ENNReal.inv_mul_cancel q_zero q_top,
  mul_one]

Result:
no goals

Proof state:
case h.e'_6.h
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
q : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ⊤
h : MemLp (fun x => ‖f x‖ ^ q.toReal) (p / q) μ
x : α
⊢ ‖f x‖ = ‖‖f x‖ ^ q.toReal‖ ^ q⁻¹.toReal

Tactic:
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]

Result:
case h.e'_6.h
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
q : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ⊤
h : MemLp (fun x => ‖f x‖ ^ q.toReal) (p / q) μ
x : α
⊢ q.toReal ≠ 0

Proof state:
case h.e'_6
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
q : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ⊤
h : MemLp (fun x => ‖f x‖ ^ q.toReal) (p / q) μ
⊢ (fun x => ‖f x‖) = fun x => ‖‖f x‖ ^ q.toReal‖ ^ q⁻¹.toReal

Tactic:
ext x

Result:
case h.e'_6.h
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
q : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ⊤
h : MemLp (fun x => ‖f x‖ ^ q.toReal) (p / q) μ
x : α
⊢ ‖f x‖ = ‖‖f x‖ ^ q.toReal‖ ^ q⁻¹.toReal

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
q : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ⊤
h : MemLp (fun x => ‖f x‖ ^ q.toReal) (p / q) μ
⊢ MemLp (fun x => ‖f x‖) p μ

Tactic:
convert h.norm_rpow_div q⁻¹ using 1

Result:
case h.e'_6
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
q : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ⊤
h : MemLp (fun x => ‖f x‖ ^ q.toReal) (p / q) μ
⊢ (fun x => ‖f x‖) = fun x => ‖‖f x‖ ^ q.toReal‖ ^ q⁻¹.toReal

case h.e'_7
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
q : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ⊤
h : MemLp (fun x => ‖f x‖ ^ q.toReal) (p / q) μ
⊢ p = p / q / q⁻¹