meas_ge_lt_top'_enorm — Mathlib

English

If f ∈ MemLp with p ≠ 0, ∞, then μ{x | ε ≤ ‖f x‖ₑ} < ∞ for ε ≠ 0.

Русский

Если f ∈ MemLp, p ≠ 0, ∞, тогда μ{x: ε ≤ ‖f(x)‖ₑ} < ∞ для ε ≠ 0.

LaTeX

$$$$μ\\{x \\,|\\, ε ≤ \\|f(x)\\|_e \\} < ∞.$$$$

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) (hε' : ε = ∞ → μ {x | ‖f x‖ₑ = ⊤} = 0) : μ {x | ε ≤ ‖f x‖ₑ} < ∞ :=
  by
  apply
    meas_ge_le_mul_pow_eLpNorm_enorm μ hp_ne_zero hp_ne_top hℒp.aestronglyMeasurable hε hε' |>.trans_lt
      (ENNReal.mul_lt_top ?_ ?_)
  · simp [hε, lt_top_iff_ne_top]
  · simp [hℒp.eLpNorm_lt_top.ne, lt_top_iff_ne_top]

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