case inl
α : Type u_1
E : Type ?u.648257
F : Type ?u.648260
G : Type u_2
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
c : G
⊢ snorm (Set.indicator s fun x => c) 0 μ ≤ ↑‖c‖₊ * ↑↑μ s ^ (1 / ENNReal.toReal 0)

case inr
α : Type u_1
E : Type ?u.648257
F : Type ?u.648260
G : Type u_2
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
c : G
p : ℝ≥0∞
hp : p ≠ 0
⊢ snorm (Set.indicator s fun x => c) p μ ≤ ↑‖c‖₊ * ↑↑μ s ^ (1 / ENNReal.toReal p)
α : Type u_1
E : Type ?u.648257
F : Type ?u.648260
G : Type u_2
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
c : G
p : ℝ≥0∞
⊢ snorm (Set.indicator s fun x => c) p μ ≤ ↑‖c‖₊ * ↑↑μ s ^ (1 / ENNReal.toReal p)
rcases eq_or_ne p 0 with (rfl | hp)
case inr.inl
α : Type u_1
E : Type ?u.648257
F : Type ?u.648260
G : Type u_2
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
c : G
hp : ⊤ ≠ 0
⊢ snorm (Set.indicator s fun x => c) ⊤ μ ≤ ↑‖c‖₊ * ↑↑μ s ^ (1 / ENNReal.toReal ⊤)

case inr.inr
α : Type u_1
E : Type ?u.648257
F : Type ?u.648260
G : Type u_2
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
c : G
p : ℝ≥0∞
hp : p ≠ 0
h'p : p ≠ ⊤
⊢ snorm (Set.indicator s fun x => c) p μ ≤ ↑‖c‖₊ * ↑↑μ s ^ (1 / ENNReal.toReal p)
case inr
α : Type u_1
E : Type ?u.648257
F : Type ?u.648260
G : Type u_2
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
c : G
p : ℝ≥0∞
hp : p ≠ 0
⊢ snorm (Set.indicator s fun x => c) p μ ≤ ↑‖c‖₊ * ↑↑μ s ^ (1 / ENNReal.toReal p)
rcases eq_or_ne p ∞ with (rfl | h'p)
case inr.inr
α : Type u_1
E : Type ?u.648257
F : Type ?u.648260
G : Type u_2
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
c : G
p : ℝ≥0∞
hp : p ≠ 0
h'p : p ≠ ⊤
t : Set α := toMeasurable μ s
⊢ snorm (Set.indicator s fun x => c) p μ ≤ ↑‖c‖₊ * ↑↑μ s ^ (1 / ENNReal.toReal p)
case inr.inr
α : Type u_1
E : Type ?u.648257
F : Type ?u.648260
G : Type u_2
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
c : G
p : ℝ≥0∞
hp : p ≠ 0
h'p : p ≠ ⊤
⊢ snorm (Set.indicator s fun x => c) p μ ≤ ↑‖c‖₊ * ↑↑μ s ^ (1 / ENNReal.toReal p)
let t := toMeasurable μ s
no goals
case inr.inr
α : Type u_1
E : Type ?u.648257
F : Type ?u.648260
G : Type u_2
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
c : G
p : ℝ≥0∞
hp : p ≠ 0
h'p : p ≠ ⊤
t : Set α := toMeasurable μ s
⊢ snorm (Set.indicator s fun x => c) p μ ≤ ↑‖c‖₊ * ↑↑μ s ^ (1 / ENNReal.toReal p)
calc
  snorm (s.indicator fun _ => c) p μ ≤ snorm (t.indicator fun _ => c) p μ :=
    snorm_mono (norm_indicator_le_of_subset (subset_toMeasurable _ _) _)
  _ = ‖c‖₊ * μ t ^ (1 / p.toReal) :=
    (snorm_indicator_const (measurableSet_toMeasurable _ _) hp h'p)
  _ = ‖c‖₊ * μ s ^ (1 / p.toReal) := by rw [measure_toMeasurable]
no goals
case inl
α : Type u_1
E : Type ?u.648257
F : Type ?u.648260
G : Type u_2
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
c : G
⊢ snorm (Set.indicator s fun x => c) 0 μ ≤ ↑‖c‖₊ * ↑↑μ s ^ (1 / ENNReal.toReal 0)
simp only [snorm_exponent_zero, zero_le']
case inr.inl
α : Type u_1
E : Type ?u.648257
F : Type ?u.648260
G : Type u_2
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
c : G
hp : ⊤ ≠ 0
⊢ snormEssSup (Set.indicator s fun x => c) μ ≤ ↑‖c‖₊
case inr.inl
α : Type u_1
E : Type ?u.648257
F : Type ?u.648260
G : Type u_2
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
c : G
hp : ⊤ ≠ 0
⊢ snorm (Set.indicator s fun x => c) ⊤ μ ≤ ↑‖c‖₊ * ↑↑μ s ^ (1 / ENNReal.toReal ⊤)
simp only [snorm_exponent_top, ENNReal.top_toReal, _root_.div_zero, ENNReal.rpow_zero, mul_one]
no goals
case inr.inl
α : Type u_1
E : Type ?u.648257
F : Type ?u.648260
G : Type u_2
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
c : G
hp : ⊤ ≠ 0
⊢ snormEssSup (Set.indicator s fun x => c) μ ≤ ↑‖c‖₊
exact snormEssSup_indicator_const_le _ _
no goals
α : Type u_1
E : Type ?u.648257
F : Type ?u.648260
G : Type u_2
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
c : G
p : ℝ≥0∞
hp : p ≠ 0
h'p : p ≠ ⊤
t : Set α := toMeasurable μ s
⊢ ↑‖c‖₊ * ↑↑μ t ^ (1 / ENNReal.toReal p) = ↑‖c‖₊ * ↑↑μ s ^ (1 / ENNReal.toReal p)
rw [measure_toMeasurable]