English
For an integrable f, the set of points where ‖f‖ ≥ ε has finite measure for any ε>0.
Русский
Для интегрируемой f множество точек, где ‖f‖ ≥ ε, имеет конечную меру для любого ε>0.
LaTeX
$$$ (Integrable\\ f μ) \\Rightarrow ∀ ε>0, μ\\{x : ε ≤ ‖f(x)‖⟂ μ\\} < ∞ $$$
Lean4
/-- A non-quantitative version of Markov inequality for integrable functions: the measure of points
where `‖f x‖ₑ ≥ ε` is finite for all positive `ε`. -/
theorem measure_enorm_ge_lt_top {E : Type*} [TopologicalSpace E] [ContinuousENorm E] {f : α → E} (hf : Integrable f μ)
{ε : ℝ≥0∞} (hε : 0 < ε) (hε' : ε ≠ ∞) : μ {x | ε ≤ ‖f x‖ₑ} < ∞ :=
by
refine meas_ge_le_mul_pow_eLpNorm_enorm μ one_ne_zero one_ne_top hf.1 hε.ne' (by simp [hε']) |>.trans_lt ?_
apply ENNReal.mul_lt_top
· simpa only [ENNReal.toReal_one, ENNReal.rpow_one, ENNReal.inv_lt_top, ENNReal.ofReal_pos] using hε
· simpa only [ENNReal.toReal_one, ENNReal.rpow_one] using (memLp_one_iff_integrable.2 hf).eLpNorm_lt_top
