eHolderNorm_const — Mathlib

English

The Hölder (Holder) norm of a constant function is zero: eHolderNorm r (Function.const X c) = 0.

Русский

Норма Холдера для константной функции равна нулю: eHolderNorm r (Function.const X c) = 0.

LaTeX

$$$eHolderNorm(r,\mathrm{const}_X c) = 0.$$$

Lean4

@[simp]
theorem eHolderNorm_const (r : ℝ≥0) (c : Y) : eHolderNorm r (Function.const X c) = 0 :=
  by
  rw [eHolderNorm, ← ENNReal.bot_eq_zero, iInf₂_eq_bot]
  exact fun C' hC' => ⟨0, .const, hC'⟩

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