norm_const_le — Mathlib

English

The Lp-norm of indicatorConstLp is bounded above by the stated product, i.e., ||indicatorConstLp(p, hs, hμs, c)|| ≤ ||c|| μ(s)^{1/p}.

Русский

Норма indicatorConstLp ограничена сверху произведением ||c|| и μ(s)^{1/p}.

LaTeX

$$||indicatorConstLp(p, hs, hμs, c)|| ≤ ||c|| * μ.real s^{1/p.toReal}.$$

Lean4

theorem norm_const_le : ‖Lp.const p μ c‖ ≤ ‖c‖ * μ.real Set.univ ^ (1 / p.toReal) :=
  by
  rw [← indicatorConstLp_univ]
  exact norm_indicatorConstLp_le

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