eLpNorm'_le_eLpNorm'_of_exponent_le

English

Hölder-type bound: the Lp-norm of the bilinear form b(f,g) is ≤ c times the Lp-norms of f and g with appropriate exponents.

Русский

Неравенство Холдера для двойственной операции: нормa Lp слева не хуже произведения норм f и g с коэффициентом c.

LaTeX

$$$eLpNorm (f \\mapsto b(f,g))\\, r μ \\le c \\cdot eLpNorm f p μ \\cdot eLpNorm g q μ \\text{ under HolderTriple conditions}$$$

Lean4

theorem eLpNorm'_le_eLpNorm'_of_exponent_le {p q : ℝ} (hp0_lt : 0 < p) (hpq : p ≤ q) (μ : Measure α)
    [IsProbabilityMeasure μ] (hf : AEStronglyMeasurable f μ) : eLpNorm' f p μ ≤ eLpNorm' f q μ :=
  by
  have h_le_μ := eLpNorm'_le_eLpNorm'_mul_rpow_measure_univ hp0_lt hpq hf
  rwa [measure_univ, ENNReal.one_rpow, mul_one] at h_le_μ

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