lintegral_mul_le_Lp_mul_Lq_of_ne_zero_of_ne_top

English

Let (X, Σ, μ) be a measure space. If p, q ∈ R form a Hölder pair (p and q are conjugate exponents), and f, g : X → ℝ≥0∞ are almost everywhere measurable with ∫ f^p dμ, ∫ g^q dμ finite and nonzero, then the integral of their product is bounded by the product of the Lp and Lq norms: ∫ f g dμ ≤ (∫ f^p dμ)^{1/p} (∫ g^q dμ)^{1/q}.

Русский

Пусть (X, Σ, μ) — мера пространства. Пусть p, q ∈ ℝ образуют пару Хольдера (1/p + 1/q = 1). Пусть f, g : X → ℝ≥0∞ являются а.е. измеримыми и такие, что ∫ f^p dμ, ∫ g^q dμ конечны и не равны нулю. Тогда ∫ f g dμ ≤ (∫ f^p dμ)^{1/p} (∫ g^q dμ)^{1/q}.

LaTeX

$$$\\text{Let } (X,\\mathcal{A},\\mu) \\text{ be a measure space. For } p,q\\in\\mathbb{R} \\text{ with } p \\text{ Holder-conjugate to } q, \\\\ \\text{and } f,g:X\\to\\mathbb{R}_{\\ge 0}^{\\infty} \\\\ \\text{which are a.e. measurable w.r.t. } \\mu, \\\\ \\int f^p\\,d\\mu \\neq \\top, \\int g^q\\,d\\mu \\neq \\top, \\int f^p\\,d\\mu \\neq 0, \\int g^q\\,d\\mu \\neq 0 \\\\ \\Rightarrow \\int f g\\,d\\mu \\le \\Big(\\int f^p\\,d\\mu\\Big)^{1/p} \\cdot \\Big(\\int g^q\\,d\\mu\\Big)^{1/q}.$$$

Lean4

/-- Hölder's inequality in case of finite non-zero integrals -/
theorem lintegral_mul_le_Lp_mul_Lq_of_ne_zero_of_ne_top {p q : ℝ} (hpq : p.HolderConjugate q) {f g : α → ℝ≥0∞}
    (hf : AEMeasurable f μ) (hf_nontop : (∫⁻ a, f a ^ p ∂μ) ≠ ⊤) (hg_nontop : (∫⁻ a, g a ^ q ∂μ) ≠ ⊤)
    (hf_nonzero : (∫⁻ a, f a ^ p ∂μ) ≠ 0) (hg_nonzero : (∫⁻ a, g a ^ q ∂μ) ≠ 0) :
    (∫⁻ a, (f * g) a ∂μ) ≤ (∫⁻ a, f a ^ p ∂μ) ^ (1 / p) * (∫⁻ a, g a ^ q ∂μ) ^ (1 / q) :=
  by
  let npf := (∫⁻ c : α, f c ^ p ∂μ) ^ (1 / p)
  let nqg := (∫⁻ c : α, g c ^ q ∂μ) ^ (1 / q)
  calc
    (∫⁻ a : α, (f * g) a ∂μ) = ∫⁻ a : α, (funMulInvSnorm f p μ * funMulInvSnorm g q μ) a * (npf * nqg) ∂μ :=
      by
      refine lintegral_congr fun a => ?_
      rw [Pi.mul_apply, fun_eq_funMulInvSnorm_mul_eLpNorm f hf_nonzero hf_nontop,
        fun_eq_funMulInvSnorm_mul_eLpNorm g hg_nonzero hg_nontop, Pi.mul_apply]
      ring
    _ ≤ npf * nqg :=
      by
      rw [lintegral_mul_const' (npf * nqg) _
          (by simp [npf, nqg, hf_nontop, hg_nontop, hf_nonzero, hg_nonzero, ENNReal.mul_eq_top])]
      refine mul_le_of_le_one_left' ?_
      have hf1 := lintegral_rpow_funMulInvSnorm_eq_one hpq.pos hf_nonzero hf_nontop
      have hg1 := lintegral_rpow_funMulInvSnorm_eq_one hpq.symm.pos hg_nonzero hg_nontop
      exact lintegral_mul_le_one_of_lintegral_rpow_eq_one hpq (hf.mul_const _) hf1 hg1

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