eLpNorm_le_add_measure_left — Mathlib

English

The Lp-norm does not exceed the norm after adding ν to μ: eLpNorm f p μ ≤ eLpNorm f p (μ+ν).

Русский

Норма Lp не превышает норму после суммирования measures: eLpNorm f p μ ≤ eLpNorm f p (μ+ν).

LaTeX

$$eLpNorm f p μ ≤ eLpNorm f p (μ+ν).$$

Lean4

theorem eLpNorm_le_add_measure_left (f : α → ε) (μ ν : Measure α) {p : ℝ≥0∞} : eLpNorm f p ν ≤ eLpNorm f p (μ + ν) :=
  eLpNorm_mono_measure f <| Measure.le_add_left <| le_refl _

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