antitone — Mathlib

English

If μ is a finite measure, and p ≤ q, then Lp E q μ ≤ Lp E p μ (Lp norms as q- larger exponents produce smaller spaces).

Русский

Если μ конечная, и p ≤ q, то Lp E q μ ≤ Lp E p μ.

LaTeX

$$IsFiniteMeasure μ → p ≤ q → Lp E q μ ≤ Lp E p μ$$

Lean4

protected theorem antitone [IsFiniteMeasure μ] {p q : ℝ≥0∞} (hpq : p ≤ q) : Lp E q μ ≤ Lp E p μ := fun f hf =>
  (MemLp.mono_exponent ⟨f.aestronglyMeasurable, hf⟩ hpq).2

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