English
For finite sum, the scalar product is bounded by the product of Lp and Lq norms of real-valued sequences using absolute values.
Русский
Для конечной суммы скалярное произведение ограничено произведением норм Lp и Lq для вещественных последовательностей через моду.
LaTeX
$$$\sum_{i\in s} f_i g_i \le \left(\sum_{i\in s} |f_i|^p\right)^{1/p} \left(\sum_{i\in s} |g_i|^q\right)^{1/q}$$$
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. Version for sums over finite sets,
with real-valued functions. -/
theorem inner_le_Lp_mul_Lq (hpq : HolderConjugate p q) :
∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, |f i| ^ p) ^ (1 / p) * (∑ i ∈ s, |g i| ^ q) ^ (1 / q) :=
by
have :=
NNReal.coe_le_coe.2
(NNReal.inner_le_Lp_mul_Lq s (fun i => ⟨_, abs_nonneg (f i)⟩) (fun i => ⟨_, abs_nonneg (g i)⟩) hpq)
push_cast at this
refine le_trans (sum_le_sum fun i _ => ?_) this
simp only [← abs_mul, le_abs_self]
