norm_indicatorConstLp' — Mathlib

English

If p ≠ 0 and μ(s) ≠ 0, then indicatorConstLp(p, hs, hμs, c) has norm ||c|| μ(s)^{1/p} with p ≠ ∞; if p = ∞ adjust accordingly.

Русский

Если p ≠ 0 и μ(s) ≠ 0, тогда нормa indicatorConstLp(p, hs, hμs, c) равна ||c|| μ(s)^{1/p} (при p ≠ ∞).

LaTeX

$$$\|indicatorConstLp(p, hs, hμs, c)\| = \|c\| \cdot (\mu(s))^{1/p^{\mathrm{real}}} \quad \text{при } p \neq 0, \mu(s) \neq 0$.$$

Lean4

theorem norm_indicatorConstLp' (hp_pos : p ≠ 0) (hμs_pos : μ s ≠ 0) :
    ‖indicatorConstLp p hs hμs c‖ = ‖c‖ * μ.real s ^ (1 / p.toReal) :=
  by
  by_cases hp_top : p = ∞
  · rw [hp_top, ENNReal.toReal_top, _root_.div_zero, Real.rpow_zero, mul_one]
    exact norm_indicatorConstLp_top hμs_pos
  · exact norm_indicatorConstLp hp_pos hp_top

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