English
As above for finite sums with ENNReal values; same bound holds.
Русский
Аналогично для ENNReal на конечном наборе индексов.
LaTeX
$$$\sum_{i\in s} f_i g_i \le (\sum_{i\in s} f_i^p)^{1/p} (\sum_{i\in s} g_i^q)^{1/q}$$$
Lean4
/-- **Minkowski inequality**: the `L_p` seminorm of the sum of two vectors is less than or equal
to the sum of the `L_p`-seminorms of the summands. A version for `ℝ≥0∞`-valued nonnegative
functions. -/
theorem Lp_add_le (hp : 1 ≤ p) :
(∑ i ∈ s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) + (∑ i ∈ s, g i ^ p) ^ (1 / p) :=
by
by_cases H' : (∑ i ∈ s, f i ^ p) ^ (1 / p) = ⊤ ∨ (∑ i ∈ s, g i ^ p) ^ (1 / p) = ⊤
· rcases H' with H' | H' <;> simp [H', -one_div]
have pos : 0 < p := lt_of_lt_of_le zero_lt_one hp
replace H' : (∀ i ∈ s, f i ≠ ⊤) ∧ ∀ i ∈ s, g i ≠ ⊤ := by
simpa [ENNReal.rpow_eq_top_iff, asymm pos, pos, ENNReal.sum_eq_top, not_or] using H'
have :=
ENNReal.coe_le_coe.2
(@NNReal.Lp_add_le _ s (fun i => ENNReal.toNNReal (f i)) (fun i => ENNReal.toNNReal (g i)) _ hp)
push_cast [ENNReal.coe_rpow_of_nonneg, le_of_lt pos, le_of_lt (one_div_pos.2 pos)] at this
convert this using 2 <;> [skip; congr 1; congr 1] <;>
· refine Finset.sum_congr rfl fun i hi => ?_
simp [H'.1 i hi, H'.2 i hi]
