Lp_nnnorm_le — Mathlib

English

The range of the canonical toLp homomorphism equals the subgroup of Lp consisting of bounded continuous representatives.

Русский

Образ отображения toLp совпадает с подгруппой Lp, состоящей из ограниченных непрерывных представителей.

LaTeX

$$$\\mathrm{range}(\\mathrm{toLp}) = \\mathrm{Lp}_{\\text{bounded}}(E,p,μ).$$$

Lean4

/-- The `Lp`-norm of a bounded continuous function is at most a constant (depending on the measure
of the whole space) times its sup-norm. -/
theorem Lp_nnnorm_le (f : α →ᵇ E) :
    ‖(⟨f.toContinuousMap.toAEEqFun μ, mem_Lp f⟩ : Lp E p μ)‖₊ ≤ measureUnivNNReal μ ^ p.toReal⁻¹ * ‖f‖₊ :=
  by
  apply Lp.nnnorm_le_of_ae_bound
  refine (f.toContinuousMap.coeFn_toAEEqFun μ).mono ?_
  intro x hx
  rw [← NNReal.coe_le_coe, coe_nnnorm, coe_nnnorm]
  convert f.norm_coe_le_norm x using 2

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