measure_norm_gt_lt_top_enorm — Mathlib

English

For integrable f, the measure of points where ‖f‖ > ε is finite 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_norm_gt_lt_top_enorm {E : Type*} [TopologicalSpace E] [ContinuousENorm E] {f : α → E}
    (hf : Integrable f μ) {ε : ℝ≥0∞} (hε : 0 < ε) : μ {x | ε < ‖f x‖ₑ} < ∞ :=
  by
  by_cases hε' : ε = ∞
  · simp [hε']
  exact lt_of_le_of_lt (measure_mono (fun _ h ↦ (Set.mem_setOf_eq ▸ h).le)) (hf.measure_enorm_ge_lt_top hε hε')

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