funMulInvSnorm_rpow — Mathlib

English

Under Holder conjugacy, if ∫ f^p = 1 and ∫ g^q = 1, then ∫ (f g) ≤ 1.

Русский

При сопряженных значениях Холдера, если ∫ f^p = 1 и ∫ g^q = 1, то ∫ (f g) ≤ 1.

LaTeX

$$$p.HolderConjugate q \\Rightarrow \\int⁻ a, (f a · g a) ∂μ ≤ 1$ при нормировке $\\int f^p = \\int g^q = 1$$$

Lean4

theorem funMulInvSnorm_rpow {p : ℝ} (hp0 : 0 < p) {f : α → ℝ≥0∞} {a : α} :
    funMulInvSnorm f p μ a ^ p = f a ^ p * (∫⁻ c, f c ^ p ∂μ)⁻¹ :=
  by
  rw [funMulInvSnorm, mul_rpow_of_nonneg _ _ (le_of_lt hp0)]
  suffices h_inv_rpow : ((∫⁻ c : α, f c ^ p ∂μ) ^ (1 / p))⁻¹ ^ p = (∫⁻ c : α, f c ^ p ∂μ)⁻¹ by rw [h_inv_rpow]
  rw [inv_rpow, ← rpow_mul, one_div_mul_cancel hp0.ne', rpow_one]

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