English
The Lp-norm of f is the greatest value of the inner product ∑ f_i g_i over all g with Lq-norm ≤ 1.
Русский
Нормa Lp вектора f является наибольшим значением скалярного произведения над всеми g с Lq-нормой не большей единицы.
LaTeX
$$IsGreatest \big( \{ \sum_{i\in s} f_i g_i : \|g\|_{L^q} \le 1 \} \big) = (\sum_{i\in s} f_i^p)^{1/p}$$
Lean4
/-- **Hölder inequality**: the scalar product of two functions is bounded by the product of their
`L^p` and `L^q` norms when `p` and `q` are conjugate exponents. A version for `NNReal`-valued
functions. For an alternative version, convenient if the infinite sums are not already expressed as
`p`-th powers, see `inner_le_Lp_mul_Lq_tsum`. -/
theorem inner_le_Lp_mul_Lq_hasSum {f g : ι → ℝ≥0} {A B : ℝ≥0} {p q : ℝ} (hpq : p.HolderConjugate q)
(hf : HasSum (fun i => f i ^ p) (A ^ p)) (hg : HasSum (fun i => g i ^ q) (B ^ q)) :
∃ C, C ≤ A * B ∧ HasSum (fun i => f i * g i) C :=
by
obtain ⟨H₁, H₂⟩ := inner_le_Lp_mul_Lq_tsum hpq hf.summable hg.summable
have hA : A = (∑' i : ι, f i ^ p) ^ (1 / p) := by rw [hf.tsum_eq, rpow_inv_rpow_self hpq.ne_zero]
have hB : B = (∑' i : ι, g i ^ q) ^ (1 / q) := by rw [hg.tsum_eq, rpow_inv_rpow_self hpq.symm.ne_zero]
refine ⟨∑' i, f i * g i, ?_, ?_⟩
· simpa [hA, hB] using H₂
· simpa only [rpow_self_rpow_inv hpq.ne_zero] using H₁.hasSum
