α : Type u_2
E : Type u_1
F : Type ?u.713508
G : Type ?u.713511
m m0 : MeasurableSpace α
p : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → E
hf : Memℒp f p
q : ℝ≥0∞
⊢ snorm (fun x => ‖f x‖ ^ ENNReal.toReal q) (p / q) μ < ⊤
α : Type u_2
E : Type u_1
F : Type ?u.713508
G : Type ?u.713511
m m0 : MeasurableSpace α
p : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → E
hf : Memℒp f p
q : ℝ≥0∞
⊢ Memℒp (fun x => ‖f x‖ ^ ENNReal.toReal q) (p / q)
refine' ⟨(hf.1.norm.aemeasurable.pow_const q.toReal).aestronglyMeasurable, _⟩
case pos
α : Type u_2
E : Type u_1
F : Type ?u.713508
G : Type ?u.713511
m m0 : MeasurableSpace α
p : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → E
hf : Memℒp f p
q : ℝ≥0∞
q_top : q = ⊤
⊢ snorm (fun x => ‖f x‖ ^ ENNReal.toReal q) (p / q) μ < ⊤

case neg
α : Type u_2
E : Type u_1
F : Type ?u.713508
G : Type ?u.713511
m m0 : MeasurableSpace α
p : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → E
hf : Memℒp f p
q : ℝ≥0∞
q_top : ¬q = ⊤
⊢ snorm (fun x => ‖f x‖ ^ ENNReal.toReal q) (p / q) μ < ⊤
α : Type u_2
E : Type u_1
F : Type ?u.713508
G : Type ?u.713511
m m0 : MeasurableSpace α
p : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → E
hf : Memℒp f p
q : ℝ≥0∞
⊢ snorm (fun x => ‖f x‖ ^ ENNReal.toReal q) (p / q) μ < ⊤
by_cases q_top : q = ∞
case pos
α : Type u_2
E : Type u_1
F : Type ?u.713508
G : Type ?u.713511
m m0 : MeasurableSpace α
p : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → E
hf : Memℒp f p
q : ℝ≥0∞
q_top : ¬q = ⊤
q_zero : q = 0
⊢ snorm (fun x => ‖f x‖ ^ ENNReal.toReal q) (p / q) μ < ⊤

case neg
α : Type u_2
E : Type u_1
F : Type ?u.713508
G : Type ?u.713511
m m0 : MeasurableSpace α
p : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → E
hf : Memℒp f p
q : ℝ≥0∞
q_top : ¬q = ⊤
q_zero : ¬q = 0
⊢ snorm (fun x => ‖f x‖ ^ ENNReal.toReal q) (p / q) μ < ⊤
case neg
α : Type u_2
E : Type u_1
F : Type ?u.713508
G : Type ?u.713511
m m0 : MeasurableSpace α
p : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → E
hf : Memℒp f p
q : ℝ≥0∞
q_top : ¬q = ⊤
⊢ snorm (fun x => ‖f x‖ ^ ENNReal.toReal q) (p / q) μ < ⊤
by_cases q_zero : q = 0
case neg
α : Type u_2
E : Type u_1
F : Type ?u.713508
G : Type ?u.713511
m m0 : MeasurableSpace α
p : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → E
hf : Memℒp f p
q : ℝ≥0∞
q_top : ¬q = ⊤
q_zero : ¬q = 0
⊢ snorm (fun x => f x) (p / q * ENNReal.ofReal (ENNReal.toReal q)) μ ^ ENNReal.toReal q < ⊤
case neg
α : Type u_2
E : Type u_1
F : Type ?u.713508
G : Type ?u.713511
m m0 : MeasurableSpace α
p : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → E
hf : Memℒp f p
q : ℝ≥0∞
q_top : ¬q = ⊤
q_zero : ¬q = 0
⊢ snorm (fun x => ‖f x‖ ^ ENNReal.toReal q) (p / q) μ < ⊤
rw [snorm_norm_rpow _ (ENNReal.toReal_pos q_zero q_top)]
case neg
α : Type u_2
E : Type u_1
F : Type ?u.713508
G : Type ?u.713511
m m0 : MeasurableSpace α
p : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → E
hf : Memℒp f p
q : ℝ≥0∞
q_top : ¬q = ⊤
q_zero : ¬q = 0
⊢ snorm (fun x => f x) (p / q * ENNReal.ofReal (ENNReal.toReal q)) μ ≠ ⊤
case neg
α : Type u_2
E : Type u_1
F : Type ?u.713508
G : Type ?u.713511
m m0 : MeasurableSpace α
p : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → E
hf : Memℒp f p
q : ℝ≥0∞
q_top : ¬q = ⊤
q_zero : ¬q = 0
⊢ snorm (fun x => f x) (p / q * ENNReal.ofReal (ENNReal.toReal q)) μ ^ ENNReal.toReal q < ⊤
apply ENNReal.rpow_lt_top_of_nonneg ENNReal.toReal_nonneg
case neg
α : Type u_2
E : Type u_1
F : Type ?u.713508
G : Type ?u.713511
m m0 : MeasurableSpace α
p : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → E
hf : Memℒp f p
q : ℝ≥0∞
q_top : ¬q = ⊤
q_zero : ¬q = 0
⊢ snorm (fun x => f x) p μ ≠ ⊤
case neg
α : Type u_2
E : Type u_1
F : Type ?u.713508
G : Type ?u.713511
m m0 : MeasurableSpace α
p : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → E
hf : Memℒp f p
q : ℝ≥0∞
q_top : ¬q = ⊤
q_zero : ¬q = 0
⊢ snorm (fun x => f x) (p / q * ENNReal.ofReal (ENNReal.toReal q)) μ ≠ ⊤
rw [ENNReal.ofReal_toReal q_top, div_eq_mul_inv, mul_assoc, ENNReal.inv_mul_cancel q_zero q_top,
  mul_one]
no goals
case neg
α : Type u_2
E : Type u_1
F : Type ?u.713508
G : Type ?u.713511
m m0 : MeasurableSpace α
p : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → E
hf : Memℒp f p
q : ℝ≥0∞
q_top : ¬q = ⊤
q_zero : ¬q = 0
⊢ snorm (fun x => f x) p μ ≠ ⊤
exact hf.2.ne
no goals
case pos
α : Type u_2
E : Type u_1
F : Type ?u.713508
G : Type ?u.713511
m m0 : MeasurableSpace α
p : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → E
hf : Memℒp f p
q : ℝ≥0∞
q_top : q = ⊤
⊢ snorm (fun x => ‖f x‖ ^ ENNReal.toReal q) (p / q) μ < ⊤
simp [q_top]
case pos
α : Type u_2
E : Type u_1
F : Type ?u.713508
G : Type ?u.713511
m m0 : MeasurableSpace α
p : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → E
hf : Memℒp f p
q : ℝ≥0∞
q_top : ¬q = ⊤
q_zero : q = 0
⊢ snorm (fun x => 1) (p / 0) μ < ⊤
case pos
α : Type u_2
E : Type u_1
F : Type ?u.713508
G : Type ?u.713511
m m0 : MeasurableSpace α
p : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → E
hf : Memℒp f p
q : ℝ≥0∞
q_top : ¬q = ⊤
q_zero : q = 0
⊢ snorm (fun x => ‖f x‖ ^ ENNReal.toReal q) (p / q) μ < ⊤
simp [q_zero]
case pos
α : Type u_2
E : Type u_1
F : Type ?u.713508
G : Type ?u.713511
m m0 : MeasurableSpace α
p : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → E
hf : Memℒp f p
q : ℝ≥0∞
q_top : ¬q = ⊤
q_zero : q = 0
p_zero : p = 0
⊢ snorm (fun x => 1) (p / 0) μ < ⊤

case neg
α : Type u_2
E : Type u_1
F : Type ?u.713508
G : Type ?u.713511
m m0 : MeasurableSpace α
p : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → E
hf : Memℒp f p
q : ℝ≥0∞
q_top : ¬q = ⊤
q_zero : q = 0
p_zero : ¬p = 0
⊢ snorm (fun x => 1) (p / 0) μ < ⊤
case pos
α : Type u_2
E : Type u_1
F : Type ?u.713508
G : Type ?u.713511
m m0 : MeasurableSpace α
p : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → E
hf : Memℒp f p
q : ℝ≥0∞
q_top : ¬q = ⊤
q_zero : q = 0
⊢ snorm (fun x => 1) (p / 0) μ < ⊤
by_cases p_zero : p = 0
case neg
α : Type u_2
E : Type u_1
F : Type ?u.713508
G : Type ?u.713511
m m0 : MeasurableSpace α
p : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → E
hf : Memℒp f p
q : ℝ≥0∞
q_top : ¬q = ⊤
q_zero : q = 0
p_zero : ¬p = 0
⊢ snorm (fun x => 1) ⊤ μ < ⊤
case neg
α : Type u_2
E : Type u_1
F : Type ?u.713508
G : Type ?u.713511
m m0 : MeasurableSpace α
p : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → E
hf : Memℒp f p
q : ℝ≥0∞
q_top : ¬q = ⊤
q_zero : q = 0
p_zero : ¬p = 0
⊢ snorm (fun x => 1) (p / 0) μ < ⊤
rw [ENNReal.div_zero p_zero]
no goals
case neg
α : Type u_2
E : Type u_1
F : Type ?u.713508
G : Type ?u.713511
m m0 : MeasurableSpace α
p : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → E
hf : Memℒp f p
q : ℝ≥0∞
q_top : ¬q = ⊤
q_zero : q = 0
p_zero : ¬p = 0
⊢ snorm (fun x => 1) ⊤ μ < ⊤
exact (memℒp_top_const (1 : ℝ)).2
no goals
case pos
α : Type u_2
E : Type u_1
F : Type ?u.713508
G : Type ?u.713511
m m0 : MeasurableSpace α
p : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → E
hf : Memℒp f p
q : ℝ≥0∞
q_top : ¬q = ⊤
q_zero : q = 0
p_zero : p = 0
⊢ snorm (fun x => 1) (p / 0) μ < ⊤
simp [p_zero]