eLpNorm'_const_of_isProbabilityMeasure

English

For nonzero p and nonzero μ, eLpNorm_const' gives the same expression as eLpNorm' with q and μ under regularity assumptions; i.e., the norm of a constant is given by ∥c∥ times μ(univ)^(1/q).

Русский

Норма константы выражается через ∥c∥ и μ(univ)^(1/q) при допустимых p и μ.

LaTeX

$$eLpNorm'(c) = ∥c∥ₑ · μ(univ)^(1/q)$$

Lean4

theorem eLpNorm'_const_of_isProbabilityMeasure (c : ε) (hq_pos : 0 < q) [IsProbabilityMeasure μ] :
    eLpNorm' (fun _ : α => c) q μ = ‖c‖ₑ := by simp [eLpNorm'_const c hq_pos, measure_univ]

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