case intro
α : Type u_2
β : Type u_1
ι : Type ?u.118448
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hM : snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
⊢ ∃ M, 0 < M ∧ snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
α : Type u_2
β : Type u_1
ι : Type ?u.118448
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
⊢ ∃ M, 0 < M ∧ snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
obtain ⟨M, hM⟩ := hf.snorm_indicator_norm_ge_le μ hmeas hε
case intro
α : Type u_2
β : Type u_1
ι : Type ?u.118448
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hM : snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
x : α
⊢ ‖Set.indicator {x | max M 1 ≤ ↑‖f x‖₊} f x‖ ≤ ‖Set.indicator {x | M ≤ ↑‖f x‖₊} f x‖
case intro
α : Type u_2
β : Type u_1
ι : Type ?u.118448
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hM : snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
⊢ ∃ M, 0 < M ∧ snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
refine'
  ⟨max M 1, lt_of_lt_of_le zero_lt_one (le_max_right _ _), le_trans (snorm_mono fun x => _) hM⟩
case intro
α : Type u_2
β : Type u_1
ι : Type ?u.118448
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hM : snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
x : α
⊢ Set.indicator {x | max M 1 ≤ ↑‖f x‖₊} (fun a => ‖f a‖) x ≤ Set.indicator {x | M ≤ ↑‖f x‖₊} (fun a => ‖f a‖) x
case intro
α : Type u_2
β : Type u_1
ι : Type ?u.118448
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hM : snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
x : α
⊢ ‖Set.indicator {x | max M 1 ≤ ↑‖f x‖₊} f x‖ ≤ ‖Set.indicator {x | M ≤ ↑‖f x‖₊} f x‖
rw [norm_indicator_eq_indicator_norm, norm_indicator_eq_indicator_norm]
case intro
α : Type u_2
β : Type u_1
ι : Type ?u.118448
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hM : snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
x✝ x : α
hx : x ∈ {x | max M 1 ≤ ↑‖f x‖₊}
⊢ x ∈ {x | M ≤ ↑‖f x‖₊}
case intro
α : Type u_2
β : Type u_1
ι : Type ?u.118448
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hM : snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
x : α
⊢ Set.indicator {x | max M 1 ≤ ↑‖f x‖₊} (fun a => ‖f a‖) x ≤ Set.indicator {x | M ≤ ↑‖f x‖₊} (fun a => ‖f a‖) x
refine' Set.indicator_le_indicator_of_subset (fun x hx => _) (fun x => norm_nonneg (f x)) x
case intro
α : Type u_2
β : Type u_1
ι : Type ?u.118448
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hM : snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
x✝ x : α
hx : max M 1 ≤ ↑‖f x‖₊
⊢ x ∈ {x | M ≤ ↑‖f x‖₊}
case intro
α : Type u_2
β : Type u_1
ι : Type ?u.118448
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hM : snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
x✝ x : α
hx : x ∈ {x | max M 1 ≤ ↑‖f x‖₊}
⊢ x ∈ {x | M ≤ ↑‖f x‖₊}
rw [Set.mem_setOf_eq] at hx
no goals
case intro
α : Type u_2
β : Type u_1
ι : Type ?u.118448
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hM : snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
x✝ x : α
hx : max M 1 ≤ ↑‖f x‖₊
⊢ x ∈ {x | M ≤ ↑‖f x‖₊}
exact (max_le_iff.1 hx).1