eLpNorm_smul_le_eLpNorm_mul_eLpNorm_top

English

Hölder-type inequality for the top exponent case: the top Lp-norm of a bilinear form is bounded by the product of individual top-norms with a scalar bound.

Русский

Холдерова неравенство для верхнего показателя: верхняя норма билинейной формы ограничена произведением верхних норм каждого компонента и скалярного константы.

LaTeX

$$$eLpNorm_top (b(f,g)) ≤ c · eLpNorm_top f · eLpNorm_top g$$$

Lean4

theorem eLpNorm_smul_le_eLpNorm_mul_eLpNorm_top (p : ℝ≥0∞) (f : α → E) {φ : α → 𝕜} (hφ : AEStronglyMeasurable φ μ) :
    eLpNorm (φ • f) p μ ≤ eLpNorm φ p μ * eLpNorm f ∞ μ := by
  simpa using
    (eLpNorm_le_eLpNorm_mul_eLpNorm_top p hφ f (· • ·) 1 (.of_forall fun _ => by simpa using nnnorm_smul_le _ _) :)

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