α : Type u_2
E : Type u_1
F : Type ?u.1271944
G : Type ?u.1271947
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
c : E
⊢ snorm (fun x => c) ⊤ μ < ⊤
α : Type u_2
E : Type u_1
F : Type ?u.1271944
G : Type ?u.1271947
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
c : E
⊢ Memℒp (fun x => c) ⊤
refine' ⟨aestronglyMeasurable_const, _⟩
case pos
α : Type u_2
E : Type u_1
F : Type ?u.1271944
G : Type ?u.1271947
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
c : E
h : μ = 0
⊢ snorm (fun x => c) ⊤ μ < ⊤

case neg
α : Type u_2
E : Type u_1
F : Type ?u.1271944
G : Type ?u.1271947
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
c : E
h : ¬μ = 0
⊢ snorm (fun x => c) ⊤ μ < ⊤
α : Type u_2
E : Type u_1
F : Type ?u.1271944
G : Type ?u.1271947
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
c : E
⊢ snorm (fun x => c) ⊤ μ < ⊤
by_cases h : μ = 0
no goals
case pos
α : Type u_2
E : Type u_1
F : Type ?u.1271944
G : Type ?u.1271947
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
c : E
h : μ = 0
⊢ snorm (fun x => c) ⊤ μ < ⊤
simp only [h, snorm_measure_zero, WithTop.zero_lt_top]
case neg
α : Type u_2
E : Type u_1
F : Type ?u.1271944
G : Type ?u.1271947
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
c : E
h : ¬μ = 0
⊢ ↑‖c‖₊ * ↑↑μ Set.univ ^ (1 / ENNReal.toReal ⊤) < ⊤
case neg
α : Type u_2
E : Type u_1
F : Type ?u.1271944
G : Type ?u.1271947
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
c : E
h : ¬μ = 0
⊢ snorm (fun x => c) ⊤ μ < ⊤
rw [snorm_const _ ENNReal.top_ne_zero h]
no goals
case neg
α : Type u_2
E : Type u_1
F : Type ?u.1271944
G : Type ?u.1271947
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
c : E
h : ¬μ = 0
⊢ ↑‖c‖₊ * ↑↑μ Set.univ ^ (1 / ENNReal.toReal ⊤) < ⊤
simp only [ENNReal.top_toReal, _root_.div_zero, ENNReal.rpow_zero, mul_one, ENNReal.coe_lt_top]