of_bound — Mathlib

English

If f,g are AES-measurable and ‖f‖ = ‖g‖ μ-a.e., then MemLp f p μ iff MemLp g p μ.

Русский

Если f,g AES-измеримы и их нормы равны μ-почти везде, тогда MemLp f p μ эквивалично MemLp g p μ.

LaTeX

$$$\text{AEStronglyMeasurable}(f,\mu) \wedge \text{AEStronglyMeasurable}(g,\mu) \wedge (\forall^{\mathrm{a}} x, \|f(x)\|_ε = \|g(x)\|_ε) \rightarrow (\text{MemLp}(f,p,\mu) \leftrightarrow \text{MemLp}(g,p,\mu))$$$

Lean4

theorem of_bound [IsFiniteMeasure μ] {f : α → E} (hf : AEStronglyMeasurable f μ) (C : ℝ) (hfC : ∀ᵐ x ∂μ, ‖f x‖ ≤ C) :
    MemLp f p μ :=
  (memLp_const C).of_le hf (hfC.mono fun _x hx => le_trans hx (le_abs_self _))

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