α : Type u_2
β : Type u_1
γ : Type ?u.989928
δ : Type ?u.989931
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hf : Integrable f
ε : ℝ
hε : 0 < ε
⊢ ↑↑μ {x | ENNReal.ofReal ε ≤ ↑‖f x‖₊} < ⊤
α : Type u_2
β : Type u_1
γ : Type ?u.989928
δ : Type ?u.989931
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hf : Integrable f
ε : ℝ
hε : 0 < ε
⊢ ↑↑μ {x | ε ≤ ‖f x‖} < ⊤
rw [show { x | ε ≤ ‖f x‖ } = { x | ENNReal.ofReal ε ≤ ‖f x‖₊ } by
    simp only [ENNReal.ofReal, Real.toNNReal_le_iff_le_coe, ENNReal.coe_le_coe, coe_nnnorm]]
case refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.989928
δ : Type ?u.989931
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hf : Integrable f
ε : ℝ
hε : 0 < ε
⊢ ENNReal.ofReal ε ≠ 0

case refine'_2
α : Type u_2
β : Type u_1
γ : Type ?u.989928
δ : Type ?u.989931
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hf : Integrable f
ε : ℝ
hε : 0 < ε
⊢ (ENNReal.ofReal ε)⁻¹ ^ ENNReal.toReal 1 * snorm f 1 μ ^ ENNReal.toReal 1 < ⊤
α : Type u_2
β : Type u_1
γ : Type ?u.989928
δ : Type ?u.989931
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hf : Integrable f
ε : ℝ
hε : 0 < ε
⊢ ↑↑μ {x | ENNReal.ofReal ε ≤ ↑‖f x‖₊} < ⊤
refine' (meas_ge_le_mul_pow_snorm μ one_ne_zero ENNReal.one_ne_top hf.1 _).trans_lt _
case refine'_2.a
α : Type u_2
β : Type u_1
γ : Type ?u.989928
δ : Type ?u.989931
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hf : Integrable f
ε : ℝ
hε : 0 < ε
⊢ (ENNReal.ofReal ε)⁻¹ ^ ENNReal.toReal 1 ≠ ⊤

case refine'_2.a
α : Type u_2
β : Type u_1
γ : Type ?u.989928
δ : Type ?u.989931
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hf : Integrable f
ε : ℝ
hε : 0 < ε
⊢ snorm f 1 μ ^ ENNReal.toReal 1 ≠ ⊤
case refine'_2
α : Type u_2
β : Type u_1
γ : Type ?u.989928
δ : Type ?u.989931
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hf : Integrable f
ε : ℝ
hε : 0 < ε
⊢ (ENNReal.ofReal ε)⁻¹ ^ ENNReal.toReal 1 * snorm f 1 μ ^ ENNReal.toReal 1 < ⊤
apply ENNReal.mul_lt_top
no goals
case refine'_2.a
α : Type u_2
β : Type u_1
γ : Type ?u.989928
δ : Type ?u.989931
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hf : Integrable f
ε : ℝ
hε : 0 < ε
⊢ snorm f 1 μ ^ ENNReal.toReal 1 ≠ ⊤
simpa only [ENNReal.one_toReal, ENNReal.rpow_one] using
  (memℒp_one_iff_integrable.2 hf).snorm_ne_top
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.989928
δ : Type ?u.989931
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hf : Integrable f
ε : ℝ
hε : 0 < ε
⊢ {x | ε ≤ ‖f x‖} = {x | ENNReal.ofReal ε ≤ ↑‖f x‖₊}
simp only [ENNReal.ofReal, Real.toNNReal_le_iff_le_coe, ENNReal.coe_le_coe, coe_nnnorm]
no goals
case refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.989928
δ : Type ?u.989931
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hf : Integrable f
ε : ℝ
hε : 0 < ε
⊢ ENNReal.ofReal ε ≠ 0
simpa only [Ne.def, ENNReal.ofReal_eq_zero, not_le] using hε
no goals
case refine'_2.a
α : Type u_2
β : Type u_1
γ : Type ?u.989928
δ : Type ?u.989931
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hf : Integrable f
ε : ℝ
hε : 0 < ε
⊢ (ENNReal.ofReal ε)⁻¹ ^ ENNReal.toReal 1 ≠ ⊤
simpa only [ENNReal.one_toReal, ENNReal.rpow_one, Ne.def, ENNReal.inv_eq_top,
  ENNReal.ofReal_eq_zero, not_le] using hε