lintegral_mul_le_Lp_mul_Lq_of_ne_zero_of_eq_top

English

If p > 0 and ∫ f^p dμ = ⊤ while ∫ g^q dμ ≠ 0, then the Hölder bound still holds with ∞ on the left side interpreted in the usual sense.

Русский

Если p > 0 и ∫ f^p dμ = ∞, а ∫ g^q dμ ≠ 0, то неравенство Хольдера справедливо (интерпретируем ∞ как положительную бесконечность).

LaTeX

$$$0 < p,\\; 0 \\le q,\\; \\text{f,g: }\\alpha\\to\\mathbb{R}_{\\ge 0}^{\\infty},\\; ∫ f^p dμ = ⊤,\\; (∫ g^q dμ) \\neq 0 \\Rightarrow ∫ (f g) dμ ≤ (∫ f^p dμ)^{1/p} (∫ g^q dμ)^{1/q}$$$

Lean4

theorem lintegral_mul_le_Lp_mul_Lq_of_ne_zero_of_eq_top {p q : ℝ} (hp0_lt : 0 < p) (hq0 : 0 ≤ q) {f g : α → ℝ≥0∞}
    (hf_top : ∫⁻ a, f a ^ p ∂μ = ⊤) (hg_nonzero : (∫⁻ a, g a ^ q ∂μ) ≠ 0) :
    (∫⁻ a, (f * g) a ∂μ) ≤ (∫⁻ a, f a ^ p ∂μ) ^ (1 / p) * (∫⁻ a, g a ^ q ∂μ) ^ (1 / q) := by simp [*]

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