English
For a finite index set, the maximal inner product with constraints in Lq yields the Lp-norm of f, i.e., the greatest value of ∑ f_i g_i under ∑ g_i^q ≤ 1 equals (∑ f_i^p)^{1/p}.
Русский
Для конечного индекса максимизация скалярного произведения при ограничении в Lq даёт норму Lp для функции f.
LaTeX
$$$\text{IsGreatest} \Big( \{ (g_i) \}_{i\in s} : \sum g_i^q \le 1 \Big) = \left( \sum_{i\in s} f_i^p \right)^{1/p}$$$
Lean4
/-- The `L_p` seminorm of a vector `f` is the greatest value of the inner product
`∑ i ∈ s, f i * g i` over functions `g` of `L_q` seminorm less than or equal to one. -/
theorem isGreatest_Lp (f : ι → ℝ≥0) {p q : ℝ} (hpq : p.HolderConjugate q) :
IsGreatest ((fun g : ι → ℝ≥0 => ∑ i ∈ s, f i * g i) '' {g | ∑ i ∈ s, g i ^ q ≤ 1}) ((∑ i ∈ s, f i ^ p) ^ (1 / p)) :=
by
constructor
· use fun i => f i ^ p / f i / (∑ i ∈ s, f i ^ p) ^ (1 / q)
obtain hf | hf := eq_zero_or_pos (∑ i ∈ s, f i ^ p)
· simp [hf, hpq.ne_zero, hpq.symm.ne_zero]
· have A : p + q - q ≠ 0 := by simp [hpq.ne_zero]
have B : ∀ y : ℝ≥0, y * y ^ p / y = y ^ p :=
by
refine fun y => mul_div_cancel_left_of_imp fun h => ?_
simp [h, hpq.ne_zero]
simp only [Set.mem_setOf_eq, div_rpow, ← sum_div, ← rpow_mul, div_mul_cancel₀ _ hpq.symm.ne_zero, rpow_one,
div_le_iff₀ hf, one_mul, hpq.mul_eq_add, ← rpow_sub' A, add_sub_cancel_right, le_refl, true_and,
← mul_div_assoc, B]
rw [div_eq_iff, ← rpow_add hf.ne', one_div, one_div, hpq.inv_add_inv_eq_one, rpow_one]
simpa [hpq.symm.ne_zero] using hf.ne'
· rintro _ ⟨g, hg, rfl⟩
apply le_trans (inner_le_Lp_mul_Lq s f g hpq)
simpa only [mul_one] using mul_le_mul_left' (NNReal.rpow_le_one hg (le_of_lt hpq.symm.one_div_pos)) _
