α : Type u_2
β : Type u_1
ι : Type ?u.92822
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f ⊤
hmeas : StronglyMeasurable f
hbdd : snormEssSup f μ < ⊤
⊢ ∃ M, snormEssSup (Set.indicator {x | M ≤ ↑‖f x‖₊} f) μ = 0
α : Type u_2
β : Type u_1
ι : Type ?u.92822
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f ⊤
hmeas : StronglyMeasurable f
⊢ ∃ M, snormEssSup (Set.indicator {x | M ≤ ↑‖f x‖₊} f) μ = 0
have hbdd : snormEssSup f μ < ∞ := hf.snorm_lt_top
α : Type u_2
β : Type u_1
ι : Type ?u.92822
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f ⊤
hmeas : StronglyMeasurable f
hbdd : snormEssSup f μ < ⊤
⊢ snormEssSup (Set.indicator {x | ENNReal.toReal (snorm f ⊤ μ + 1) ≤ ↑‖f x‖₊} f) μ = 0
α : Type u_2
β : Type u_1
ι : Type ?u.92822
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f ⊤
hmeas : StronglyMeasurable f
hbdd : snormEssSup f μ < ⊤
⊢ ∃ M, snormEssSup (Set.indicator {x | M ≤ ↑‖f x‖₊} f) μ = 0
refine' ⟨(snorm f ∞ μ + 1).toReal, _⟩
α : Type u_2
β : Type u_1
ι : Type ?u.92822
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f ⊤
hmeas : StronglyMeasurable f
hbdd : snormEssSup f μ < ⊤
⊢ snormEssSup f (Measure.restrict μ {x | ENNReal.toReal (snorm f ⊤ μ + 1) ≤ ↑‖f x‖₊}) = 0

α : Type u_2
β : Type u_1
ι : Type ?u.92822
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f ⊤
hmeas : StronglyMeasurable f
hbdd : snormEssSup f μ < ⊤
⊢ MeasurableSet {x | ENNReal.toReal (snorm f ⊤ μ + 1) ≤ ↑‖f x‖₊}
α : Type u_2
β : Type u_1
ι : Type ?u.92822
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f ⊤
hmeas : StronglyMeasurable f
hbdd : snormEssSup f μ < ⊤
⊢ snormEssSup (Set.indicator {x | ENNReal.toReal (snorm f ⊤ μ + 1) ≤ ↑‖f x‖₊} f) μ = 0
rw [snormEssSup_indicator_eq_snormEssSup_restrict]
α : Type u_2
β : Type u_1
ι : Type ?u.92822
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f ⊤
hmeas : StronglyMeasurable f
hbdd : snormEssSup f μ < ⊤
⊢ MeasurableSet {x | ENNReal.toReal (snorm f ⊤ μ + 1) ≤ ↑‖f x‖₊}
α : Type u_2
β : Type u_1
ι : Type ?u.92822
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f ⊤
hmeas : StronglyMeasurable f
hbdd : snormEssSup f μ < ⊤
this : Measure.restrict μ {x | ENNReal.toReal (snorm f ⊤ μ + 1) ≤ ↑‖f x‖₊} = 0
⊢ snormEssSup f (Measure.restrict μ {x | ENNReal.toReal (snorm f ⊤ μ + 1) ≤ ↑‖f x‖₊}) = 0

α : Type u_2
β : Type u_1
ι : Type ?u.92822
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f ⊤
hmeas : StronglyMeasurable f
hbdd : snormEssSup f μ < ⊤
⊢ MeasurableSet {x | ENNReal.toReal (snorm f ⊤ μ + 1) ≤ ↑‖f x‖₊}
rw [this, snormEssSup_measure_zero]
no goals
α : Type u_2
β : Type u_1
ι : Type ?u.92822
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f ⊤
hmeas : StronglyMeasurable f
hbdd : snormEssSup f μ < ⊤
⊢ MeasurableSet {x | ENNReal.toReal (snorm f ⊤ μ + 1) ≤ ↑‖f x‖₊}
exact measurableSet_le measurable_const hmeas.nnnorm.measurable.subtype_coe
α : Type u_2
β : Type u_1
ι : Type ?u.92822
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f ⊤
hmeas : StronglyMeasurable f
hbdd : snormEssSup f μ < ⊤
⊢ ↑↑μ {x | ENNReal.toReal (snormEssSup f μ + 1) ≤ ‖f x‖} = 0
α : Type u_2
β : Type u_1
ι : Type ?u.92822
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f ⊤
hmeas : StronglyMeasurable f
hbdd : snormEssSup f μ < ⊤
⊢ Measure.restrict μ {x | ENNReal.toReal (snorm f ⊤ μ + 1) ≤ ↑‖f x‖₊} = 0
simp only [coe_nnnorm, snorm_exponent_top, Measure.restrict_eq_zero]
α : Type u_2
β : Type u_1
ι : Type ?u.92822
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f ⊤
hmeas : StronglyMeasurable f
hbdd : snormEssSup f μ < ⊤
this : {x | ENNReal.toReal (snormEssSup f μ + 1) ≤ ‖f x‖} ⊆ {x | snormEssSup f μ < ↑‖f x‖₊}
⊢ ↑↑μ {x | ENNReal.toReal (snormEssSup f μ + 1) ≤ ‖f x‖} ≤ 0
α : Type u_2
β : Type u_1
ι : Type ?u.92822
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f ⊤
hmeas : StronglyMeasurable f
hbdd : snormEssSup f μ < ⊤
this : {x | ENNReal.toReal (snormEssSup f μ + 1) ≤ ‖f x‖} ⊆ {x | snormEssSup f μ < ↑‖f x‖₊}
⊢ ↑↑μ {x | ENNReal.toReal (snormEssSup f μ + 1) ≤ ‖f x‖} = 0
rw [← nonpos_iff_eq_zero]
α : Type u_2
β : Type u_1
ι : Type ?u.92822
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f ⊤
hmeas : StronglyMeasurable f
hbdd : snormEssSup f μ < ⊤
this : {x | ENNReal.toReal (snormEssSup f μ + 1) ≤ ‖f x‖} ⊆ {x | snormEssSup f μ < ↑‖f x‖₊}
⊢ ↑↑μ {x | snormEssSup f μ < ↑‖f x‖₊} ≤ 0
α : Type u_2
β : Type u_1
ι : Type ?u.92822
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f ⊤
hmeas : StronglyMeasurable f
hbdd : snormEssSup f μ < ⊤
this : {x | ENNReal.toReal (snormEssSup f μ + 1) ≤ ‖f x‖} ⊆ {x | snormEssSup f μ < ↑‖f x‖₊}
⊢ ↑↑μ {x | ENNReal.toReal (snormEssSup f μ + 1) ≤ ‖f x‖} ≤ 0
refine' (measure_mono this).trans _
α : Type u_2
β : Type u_1
ι : Type ?u.92822
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f ⊤
hmeas : StronglyMeasurable f
hbdd : snormEssSup f μ < ⊤
this : {x | ENNReal.toReal (snormEssSup f μ + 1) ≤ ‖f x‖} ⊆ {x | snormEssSup f μ < ↑‖f x‖₊}
hle : ∀ᵐ (x : α) ∂μ, ↑‖f x‖₊ ≤ snormEssSup f μ
⊢ ↑↑μ {x | snormEssSup f μ < ↑‖f x‖₊} ≤ 0
α : Type u_2
β : Type u_1
ι : Type ?u.92822
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f ⊤
hmeas : StronglyMeasurable f
hbdd : snormEssSup f μ < ⊤
this : {x | ENNReal.toReal (snormEssSup f μ + 1) ≤ ‖f x‖} ⊆ {x | snormEssSup f μ < ↑‖f x‖₊}
⊢ ↑↑μ {x | snormEssSup f μ < ↑‖f x‖₊} ≤ 0
have hle := coe_nnnorm_ae_le_snormEssSup f μ
α : Type u_2
β : Type u_1
ι : Type ?u.92822
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f ⊤
hmeas : StronglyMeasurable f
hbdd : snormEssSup f μ < ⊤
this : {x | ENNReal.toReal (snormEssSup f μ + 1) ≤ ‖f x‖} ⊆ {x | snormEssSup f μ < ↑‖f x‖₊}
hle : ↑↑μ {a | snormEssSup f μ < ↑‖f a‖₊} = 0
⊢ ↑↑μ {x | snormEssSup f μ < ↑‖f x‖₊} ≤ 0
α : Type u_2
β : Type u_1
ι : Type ?u.92822
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f ⊤
hmeas : StronglyMeasurable f
hbdd : snormEssSup f μ < ⊤
this : {x | ENNReal.toReal (snormEssSup f μ + 1) ≤ ‖f x‖} ⊆ {x | snormEssSup f μ < ↑‖f x‖₊}
hle : ∀ᵐ (x : α) ∂μ, ↑‖f x‖₊ ≤ snormEssSup f μ
⊢ ↑↑μ {x | snormEssSup f μ < ↑‖f x‖₊} ≤ 0
simp_rw [ae_iff, not_le] at hle
no goals
α : Type u_2
β : Type u_1
ι : Type ?u.92822
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f ⊤
hmeas : StronglyMeasurable f
hbdd : snormEssSup f μ < ⊤
this : {x | ENNReal.toReal (snormEssSup f μ + 1) ≤ ‖f x‖} ⊆ {x | snormEssSup f μ < ↑‖f x‖₊}
hle : ↑↑μ {a | snormEssSup f μ < ↑‖f a‖₊} = 0
⊢ ↑↑μ {x | snormEssSup f μ < ↑‖f x‖₊} ≤ 0
exact nonpos_iff_eq_zero.2 hle
α : Type u_2
β : Type u_1
ι : Type ?u.92822
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f ⊤
hmeas : StronglyMeasurable f
hbdd : snormEssSup f μ < ⊤
x : α
hx : x ∈ {x | ENNReal.toReal (snormEssSup f μ + 1) ≤ ‖f x‖}
⊢ x ∈ {x | snormEssSup f μ < ↑‖f x‖₊}
α : Type u_2
β : Type u_1
ι : Type ?u.92822
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f ⊤
hmeas : StronglyMeasurable f
hbdd : snormEssSup f μ < ⊤
⊢ {x | ENNReal.toReal (snormEssSup f μ + 1) ≤ ‖f x‖} ⊆ {x | snormEssSup f μ < ↑‖f x‖₊}
intro x hx
α : Type u_2
β : Type u_1
ι : Type ?u.92822
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f ⊤
hmeas : StronglyMeasurable f
hbdd : snormEssSup f μ < ⊤
x : α
hx : x ∈ {x | ENNReal.toReal (snormEssSup f μ + 1) ≤ ‖f x‖}
⊢ ENNReal.toReal (snormEssSup f μ) < ‖f x‖
α : Type u_2
β : Type u_1
ι : Type ?u.92822
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f ⊤
hmeas : StronglyMeasurable f
hbdd : snormEssSup f μ < ⊤
x : α
hx : x ∈ {x | ENNReal.toReal (snormEssSup f μ + 1) ≤ ‖f x‖}
⊢ x ∈ {x | snormEssSup f μ < ↑‖f x‖₊}
rw [Set.mem_setOf_eq, ← ENNReal.toReal_lt_toReal hbdd.ne ENNReal.coe_lt_top.ne,
  ENNReal.coe_toReal, coe_nnnorm]
α : Type u_2
β : Type u_1
ι : Type ?u.92822
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f ⊤
hmeas : StronglyMeasurable f
hbdd : snormEssSup f μ < ⊤
x : α
hx : x ∈ {x | ENNReal.toReal (snormEssSup f μ + 1) ≤ ‖f x‖}
⊢ ENNReal.toReal (snormEssSup f μ) < ENNReal.toReal (snormEssSup f μ + 1)
α : Type u_2
β : Type u_1
ι : Type ?u.92822
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f ⊤
hmeas : StronglyMeasurable f
hbdd : snormEssSup f μ < ⊤
x : α
hx : x ∈ {x | ENNReal.toReal (snormEssSup f μ + 1) ≤ ‖f x‖}
⊢ ENNReal.toReal (snormEssSup f μ) < ‖f x‖
refine' lt_of_lt_of_le _ hx
α : Type u_2
β : Type u_1
ι : Type ?u.92822
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f ⊤
hmeas : StronglyMeasurable f
hbdd : snormEssSup f μ < ⊤
x : α
hx : x ∈ {x | ENNReal.toReal (snormEssSup f μ + 1) ≤ ‖f x‖}
⊢ snormEssSup f μ < snormEssSup f μ + 1

α : Type u_2
β : Type u_1
ι : Type ?u.92822
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f ⊤
hmeas : StronglyMeasurable f
hbdd : snormEssSup f μ < ⊤
x : α
hx : x ∈ {x | ENNReal.toReal (snormEssSup f μ + 1) ≤ ‖f x‖}
⊢ snormEssSup f μ + 1 ≠ ⊤
α : Type u_2
β : Type u_1
ι : Type ?u.92822
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f ⊤
hmeas : StronglyMeasurable f
hbdd : snormEssSup f μ < ⊤
x : α
hx : x ∈ {x | ENNReal.toReal (snormEssSup f μ + 1) ≤ ‖f x‖}
⊢ ENNReal.toReal (snormEssSup f μ) < ENNReal.toReal (snormEssSup f μ + 1)
rw [ENNReal.toReal_lt_toReal hbdd.ne]
no goals
α : Type u_2
β : Type u_1
ι : Type ?u.92822
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f ⊤
hmeas : StronglyMeasurable f
hbdd : snormEssSup f μ < ⊤
x : α
hx : x ∈ {x | ENNReal.toReal (snormEssSup f μ + 1) ≤ ‖f x‖}
⊢ snormEssSup f μ < snormEssSup f μ + 1
exact ENNReal.lt_add_right hbdd.ne one_ne_zero
no goals
α : Type u_2
β : Type u_1
ι : Type ?u.92822
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f ⊤
hmeas : StronglyMeasurable f
hbdd : snormEssSup f μ < ⊤
x : α
hx : x ∈ {x | ENNReal.toReal (snormEssSup f μ + 1) ≤ ‖f x‖}
⊢ snormEssSup f μ + 1 ≠ ⊤
exact (ENNReal.add_lt_top.2 ⟨hbdd, ENNReal.one_lt_top⟩).ne