norm_indicatorConstLp_le — Mathlib

English

If p ≠ ∞, and μ(s) ≠ 0, then the norm equality holds with p ≠ ∞; otherwise the top-case applies.

Русский

Если p не бесконечно большое и μ(s) ≠ 0, то выполняется соответствующее равенство нормы; иначе применим верхний случай.

LaTeX

$$$\|indicatorConstLp(p, hs, hμs, c)\| = \|c\| \cdot μ(s)^{1/p^{real}}$ под соответствующими условиями.$$

Lean4

theorem norm_indicatorConstLp_le : ‖indicatorConstLp p hs hμs c‖ ≤ ‖c‖ * μ.real s ^ (1 / p.toReal) :=
  by
  rw [indicatorConstLp, Lp.norm_toLp]
  refine ENNReal.toReal_le_of_le_ofReal (by positivity) ?_
  refine (eLpNorm_indicator_const_le _ _).trans_eq ?_
  rw [ENNReal.ofReal_mul (norm_nonneg _), ofReal_norm, measureReal_def, ENNReal.toReal_rpow, ENNReal.ofReal_toReal]
  finiteness

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