meas_ge_lt_top — Mathlib

English

If f ∈ MemLp with finite, nonzero p, then for every ε > 0, the set {x : ε ≤ ‖f(x)‖_+} has finite measure.

Русский

Если f ∈ MemLp с конечным ненулевым p, то для каждого ε > 0 множество {x : ε ≤ ‖f(x)‖_+} имеет конечную меру.

LaTeX

$$$MemLp f p μ \\land 0 < p < ∞ \\Rightarrow μ\\{x : ε \\le \\|f(x)\\|_+\\} < ∞$$$

Lean4

theorem meas_ge_lt_top {μ : Measure α} {f : α → E} (hℒp : MemLp f p μ) (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ∞)
    {ε : ℝ≥0} (hε : ε ≠ 0) : μ {x | ε ≤ ‖f x‖₊} < ∞ :=
  by
  simp_rw [← ENNReal.coe_le_coe]
  apply hℒp.meas_ge_lt_top' hp_ne_zero hp_ne_top (by simp [hε])

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