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

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

Tactic:
simp only [q_zero, ENNReal.zero_toReal, Real.rpow_zero]

Result:
case pos
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ⊤
q_zero : q = 0
⊢ eLpNorm (fun x => 1) (p / 0) μ < ⊤

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

Tactic:
simp [q_top]

Result:
no goals

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

Tactic:
refine ⟨(hf.1.norm.aemeasurable.pow_const q.toReal).aestronglyMeasurable, ?_⟩

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

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

Tactic:
by_cases q_top : q = ∞

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

case neg
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ⊤
⊢ eLpNorm (fun x => ‖f x‖ ^ q.toReal) (p / q) μ < ⊤

Proof state:
case pos
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ⊤
q_zero : q = 0
p_zero : p = 0
⊢ eLpNorm (fun x => 1) (p / 0) μ < ⊤

Tactic:
simp [p_zero]

Result:
no goals

Proof state:
case neg
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ⊤
q_zero : ¬q = 0
⊢ eLpNorm f p μ ≠ ⊤

Tactic:
exact hf.2.ne

Result:
no goals

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

Tactic:
rw [eLpNorm_norm_rpow _ (ENNReal.toReal_pos q_zero q_top)]

Result:
case neg
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ⊤
q_zero : ¬q = 0
⊢ eLpNorm f (p / q * ENNReal.ofReal q.toReal) μ ^ q.toReal < ⊤

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

Tactic:
by_cases q_zero : q = 0

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

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

Proof state:
case neg
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ⊤
q_zero : q = 0
p_zero : ¬p = 0
⊢ eLpNorm (fun x => 1) (p / 0) μ < ⊤

Tactic:
rw [ENNReal.div_zero p_zero]

Result:
case neg
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ⊤
q_zero : q = 0
p_zero : ¬p = 0
⊢ eLpNorm (fun x => 1) ⊤ μ < ⊤

Proof state:
case neg
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ⊤
q_zero : ¬q = 0
⊢ eLpNorm f (p / q * ENNReal.ofReal q.toReal) μ ≠ ⊤

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

Result:
case neg
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ⊤
q_zero : ¬q = 0
⊢ eLpNorm f p μ ≠ ⊤

Proof state:
case pos
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ⊤
q_zero : q = 0
⊢ eLpNorm (fun x => 1) (p / 0) μ < ⊤

Tactic:
by_cases p_zero : p = 0

Result:
case pos
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ⊤
q_zero : q = 0
p_zero : p = 0
⊢ eLpNorm (fun x => 1) (p / 0) μ < ⊤

case neg
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ⊤
q_zero : q = 0
p_zero : ¬p = 0
⊢ eLpNorm (fun x => 1) (p / 0) μ < ⊤

Proof state:
case neg
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ⊤
q_zero : q = 0
p_zero : ¬p = 0
⊢ eLpNorm (fun x => 1) ⊤ μ < ⊤

Tactic:
exact (memLp_top_const (1 : ℝ)).2

Result:
no goals

Proof state:
case neg
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ⊤
q_zero : ¬q = 0
⊢ eLpNorm f (p / q * ENNReal.ofReal q.toReal) μ ^ q.toReal < ⊤

Tactic:
apply ENNReal.rpow_lt_top_of_nonneg ENNReal.toReal_nonneg

Result:
case neg
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ⊤
q_zero : ¬q = 0
⊢ eLpNorm f (p / q * ENNReal.ofReal q.toReal) μ ≠ ⊤