English
A generalized Hölder inequality for multiple arguments where one factor plays a distinguished role. The integral of a product is bounded by the product of the distinguished factor's Lq-norm and the Lp-norms of the remaining factors.
Русский
Обобщение неравенства Хольдера для нескольких аргументов, где один фактор выделен. Интеграл произведения ограничен Lq‑нормой выделенного фактора и Lp‑нормами остальных.
LaTeX
$$$\\forall s\\,\\text{Finset},\\; g: X\\to\\mathbb{R}_{\\ge 0}^{∞},\\; f_i:X\\to\\mathbb{R}_{\\ge 0}^{∞},\\; hq: q\\in\\mathbb{R},\\; p_i:\\iota\\to\\mathbb{R},\\; \\sum_{i\\in s} p_i = 1 \\\\Rightarrow ∫ g^q \\* ∏_{i∈s} f_i^{p_i} ≤ (∫ g)^q ∏_{i∈s} (∫ f_i)^{p_i}$$$
Lean4
/-- A version of Hölder with multiple arguments, one of which plays a distinguished role. -/
theorem lintegral_mul_prod_norm_pow_le {α ι : Type*} [MeasurableSpace α] {μ : Measure α} (s : Finset ι) {g : α → ℝ≥0∞}
{f : ι → α → ℝ≥0∞} (hg : AEMeasurable g μ) (hf : ∀ i ∈ s, AEMeasurable (f i) μ) (q : ℝ) {p : ι → ℝ}
(hpq : q + ∑ i ∈ s, p i = 1) (hq : 0 ≤ q) (hp : ∀ i ∈ s, 0 ≤ p i) :
∫⁻ a, g a ^ q * ∏ i ∈ s, f i a ^ p i ∂μ ≤ (∫⁻ a, g a ∂μ) ^ q * ∏ i ∈ s, (∫⁻ a, f i a ∂μ) ^ p i :=
by
suffices
∫⁻ t, ∏ j ∈ insertNone s, Option.elim j (g t) (fun j ↦ f j t) ^ Option.elim j q p ∂μ ≤
∏ j ∈ insertNone s, (∫⁻ t, Option.elim j (g t) (fun j ↦ f j t) ∂μ) ^ Option.elim j q p
by simpa using this
refine ENNReal.lintegral_prod_norm_pow_le _ ?_ ?_ ?_
· rintro (_ | i) hi
· exact hg
· refine hf i ?_
simpa using hi
· simp_rw [sum_insertNone, Option.elim]
exact hpq
· rintro (_ | i) hi
· exact hq
· refine hp i ?_
simpa using hi
