eLpNorm'_mono_measure — Mathlib

English

If ν ≤ μ and p ≥ 0, then eLpNorm' f q ν ≤ eLpNorm' f q μ.

Русский

Пусть ν меньше μ; тогда eLpNorm' по мере убывает: меньше по меньшей мере не больше по μ.

LaTeX

$$$\nu \le μ \wedge 0 \le q \rightarrow eLpNorm'(f,q,\nu) ≤ eLpNorm'(f,q,μ)$$$

Lean4

@[gcongr, mono]
theorem eLpNorm'_mono_measure (f : α → ε) (hμν : ν ≤ μ) (hq : 0 ≤ q) : eLpNorm' f q ν ≤ eLpNorm' f q μ :=
  by
  simp_rw [eLpNorm']
  gcongr

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