meas_ge_lt_top_enorm — Mathlib

English

Let f be in Lp(μ) for some finite, nonzero p, and ε > 0. Then the μ-measure of the set {x : ε ≤ ‖f(x)‖_ε} is finite.

Русский

Пусть f ∈ Lp(μ) для некоторого конечного ненулевого p. Тогда мера множества {x : ε ≤ ‖f(x)‖_ε} конечна для каждого ε > 0.

LaTeX

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

Lean4

theorem meas_ge_lt_top_enorm {μ : Measure α} {f : α → ε'} (hℒp : MemLp f p μ) (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ∞)
    {ε : ℝ≥0} (hε : ε ≠ 0) : μ {x | ε ≤ ‖f x‖ₑ} < ∞ :=
  hℒp.meas_ge_lt_top'_enorm hp_ne_zero hp_ne_top (by simp [hε]) (by simp)

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