eLpNormEssSup_le_nnreal_smul_eLpNormEssSup_of_ae_le_mul

English

If g is Lp with respect to μ, and f is ae-bounded by c|g|, then f is also Lp with respect to μ, with controlled norm.

Русский

Если g ∈ Lp по μ, а f почти повсеместно ограничено на c|g|, то и f ∈ Lp по μ с контролируемой нормой.

LaTeX

$$$\\operatorname{MemLp}(g,p,μ) \\Rightarrow \\operatorname{AEStronglyMeasurable} f \\land \\forall^{\\ast} x, \\|f(x)\\|_{ε} \\le c \\|g(x)\\|_{ε} \\Rightarrow \\operatorname{MemLp}(f,p,μ)$$$

Lean4

theorem eLpNormEssSup_le_nnreal_smul_eLpNormEssSup_of_ae_le_mul {f : α → F} {g : α → G} {c : ℝ≥0}
    (h : ∀ᵐ x ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊) : eLpNormEssSup f μ ≤ c • eLpNormEssSup g μ :=
  calc
    essSup (‖f ·‖ₑ) μ ≤ essSup (fun x => (↑(c * ‖g x‖₊) : ℝ≥0∞)) μ :=
      essSup_mono_ae <| h.mono fun _ hx => ENNReal.coe_le_coe.mpr hx
    _ = essSup (c * ‖g ·‖ₑ) μ := by simp_rw [ENNReal.coe_mul, enorm]
    _ = c • essSup (‖g ·‖ₑ) μ := ENNReal.essSup_const_mul

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