eLpNorm_le_eLpNorm_mul_eLpNorm'_of_norm

English

A Holder-type inequality for bilinear operations with two functions f and g and their eLpNorms.

Русский

Неравенство Холдера для билинейной операции над двумя функциями f и g.

LaTeX

$$$eLpNorm (b(f,g)) r μ ≤ c · eLpNorm f p μ · eLpNorm g q μ$ under HolderTriple with appropriate b and h$$

Lean4

/-- Hölder's inequality, as an inequality on the `ℒp` seminorm of an elementwise operation
`fun x => b (f x) (g x)`. -/
theorem eLpNorm_le_eLpNorm_mul_eLpNorm'_of_norm {p q r : ℝ≥0∞} (hf : AEStronglyMeasurable f μ)
    (hg : AEStronglyMeasurable g μ) (b : E → F → G) (c : ℝ≥0) (h : ∀ᵐ x ∂μ, ‖b (f x) (g x)‖ ≤ c * ‖f x‖ * ‖g x‖)
    [hpqr : HolderTriple p q r] : eLpNorm (fun x => b (f x) (g x)) r μ ≤ c * eLpNorm f p μ * eLpNorm g q μ :=
  eLpNorm_le_eLpNorm_mul_eLpNorm_of_nnnorm hf hg b c h

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