eLpNorm_mono_measure — Mathlib

English

If ν ≤ μ and p ≠ 0, ∞, then eLpNorm f p ν ≤ eLpNorm f p μ, reducing to the finite-exponent case via eLpNorm'_mono_measure.

Русский

Если ν ≤ μ и p не равен 0 или ∞, то eLpNorm по мере ≤ по μ; в прочем случае сводится к частному случаю.

LaTeX

$$$\nu \le μ \wedge p ≠ 0,∞ \rightarrow eLpNorm(f,p,ν) ≤ eLpNorm(f,p,μ)$$$

Lean4

@[gcongr, mono]
theorem eLpNorm_mono_measure (f : α → ε) (hμν : ν ≤ μ) : eLpNorm f p ν ≤ eLpNorm f p μ :=
  by
  by_cases hp0 : p = 0
  · simp [hp0]
  by_cases hp_top : p = ∞
  · simp [hp_top, eLpNormEssSup_mono_measure f (Measure.absolutelyContinuous_of_le hμν)]
  simp_rw [eLpNorm_eq_eLpNorm' hp0 hp_top]
  exact eLpNorm'_mono_measure f hμν ENNReal.toReal_nonneg

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