measure_norm_ge_lt_top — Mathlib

English

A nonquantitative Markov-type bound: for integrable f and ε>0, the set where ‖f‖ ≥ ε has finite measure.

Русский

Неформальная граница Маркова: для интегрируемой f множество, где ‖f‖≥ε, имеет конечную меру.

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_norm_ge_lt_top {f : α → β} (hf : Integrable f μ) {ε : ℝ} (hε : 0 < ε) : μ {x | ε ≤ ‖f x‖} < ∞ :=
  by
  convert Integrable.measure_enorm_ge_lt_top hf (ofReal_pos.mpr hε) ofReal_ne_top with x
  rw [← Real.enorm_of_nonneg hε.le, enorm_le_iff_norm_le, Real.norm_of_nonneg hε.le]

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