measure_norm_gt_lt_top — Mathlib

English

Let f be integrable. Then for every positive number ε, the set of points where the norm of f exceeds ε has finite measure.

Русский

Пусть f интегрируемая. Тогда для любого положительного ε множество точек, в которых модуль f превышает ε, имеет конечную меру.

LaTeX

$$$\\forall \\varepsilon>0,\\ \\mu\\{x:\\varepsilon<\\|f(x)\\|\\}<\\infty$$$

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_norm_gt_lt_top {f : α → β} (hf : Integrable f μ) {ε : ℝ} (hε : 0 < ε) : μ {x | ε < ‖f x‖} < ∞ :=
  lt_of_le_of_lt (measure_mono (fun _ h ↦ (Set.mem_setOf_eq ▸ h).le))
    (hf.measure_norm_ge_lt_top hε)
      -- TODO: try generalising all lemmas below to enorm classes

Похожие утверждения