Lp_norm_le — Mathlib

English

The a.e. equality of functions agrees with their representations in Lp via toLp; i.e., the a.e. equivalence class constructed from a bounded continuous function equals its Lp image.

Русский

Практически эквивалентность функций через toLp совпадает с их эквивалентностью в Lp.

LaTeX

$$$f: \\alpha \\to^b E \\Rightarrow (toLp(f) =^{\\mathrm{a.e.}} f).$$$

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_norm_le (f : α →ᵇ E) :
    ‖(⟨f.toContinuousMap.toAEEqFun μ, mem_Lp f⟩ : Lp E p μ)‖ ≤ measureUnivNNReal μ ^ p.toReal⁻¹ * ‖f‖ :=
  Lp_nnnorm_le f

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