eLpNorm_const' — Mathlib

English

If μ is a probability measure and q ≠ 0, then eLpNorm' (fun x => c) q μ = ∥c∥ₑ under the stated hypotheses.

Русский

Если μ является вероятностной мерой и q ≠ 0, то eLpNorm'(константа c) равна ∥c∥ₑ при данных предпосылках.

LaTeX

$$eLpNorm'(fun x => c) q μ = ∥c∥ₑ$$

Lean4

theorem eLpNorm_const' (c : ε) (h0 : p ≠ 0) (h_top : p ≠ ∞) :
    eLpNorm (fun _ : α => c) p μ = ‖c‖ₑ * μ Set.univ ^ (1 / ENNReal.toReal p) := by
  simp [eLpNorm_eq_eLpNorm' h0 h_top, eLpNorm'_const, ENNReal.toReal_pos h0 h_top]
    -- NB. If ‖c‖ₑ = ∞ and μ is finite, this claim is false: the right has side is true,
    -- but the left-hand side is false (as the norm is infinite).

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