English
A version of Hölder with two functions and a single exponent p: for a finite p, the product integral is bounded by the p-norm of f and q-norm of g.
Русский
Версия Хольдера для двух функций и одного показателя p: ∫ f g ≤ (∫ f^p)^{1/p} (∫ g^q)^{1/q}.
LaTeX
$$$\\forall p,q\\in\\mathbb{R}, hpq: p.HolderConjugate q, \\forall f,g: X\\to\\mathbb{R}_{\\ge 0}, AEMeasurable f μ, AEMeasurable g μ \\,\\Rightarrow \\\\ ∫ f g ≤ (∫ f^p)^{1/p}(∫ g^q)^{1/q}$$$
Lean4
/-- A version of Hölder with multiple arguments -/
theorem lintegral_prod_norm_pow_le {α ι : Type*} [MeasurableSpace α] {μ : Measure α} (s : Finset ι) {f : ι → α → ℝ≥0∞}
(hf : ∀ i ∈ s, AEMeasurable (f i) μ) {p : ι → ℝ} (hp : ∑ i ∈ s, p i = 1) (h2p : ∀ i ∈ s, 0 ≤ p i) :
∫⁻ a, ∏ i ∈ s, f i a ^ p i ∂μ ≤ ∏ i ∈ s, (∫⁻ a, f i a ∂μ) ^ p i := by
classical
induction s using Finset.induction generalizing p with
| empty => simp at hp
| insert i₀ s hi₀ ih =>
rcases eq_or_ne (p i₀) 1 with h2i₀ | h2i₀
· simp only [hi₀, not_false_eq_true, prod_insert]
have h2p : ∀ i ∈ s, p i = 0 := by
simpa [hi₀, h2i₀, sum_eq_zero_iff_of_nonneg (fun i hi ↦ h2p i <| mem_insert_of_mem hi)] using hp
calc
∫⁻ a, f i₀ a ^ p i₀ * ∏ i ∈ s, f i a ^ p i ∂μ = ∫⁻ a, f i₀ a ^ p i₀ * ∏ i ∈ s, 1 ∂μ :=
by
congr! 3 with x
apply prod_congr rfl fun i hi ↦ by rw [h2p i hi, ENNReal.rpow_zero]
_ ≤ (∫⁻ a, f i₀ a ∂μ) ^ p i₀ * ∏ i ∈ s, 1 := by simp [h2i₀]
_ = (∫⁻ a, f i₀ a ∂μ) ^ p i₀ * ∏ i ∈ s, (∫⁻ a, f i a ∂μ) ^ p i :=
by
congr 1
apply prod_congr rfl fun i hi ↦ by rw [h2p i hi, ENNReal.rpow_zero]
· have hpi₀ : 0 ≤ 1 - p i₀ := by simp_rw [sub_nonneg, ← hp, single_le_sum h2p (mem_insert_self ..)]
have h2pi₀ : 1 - p i₀ ≠ 0 := by rwa [sub_ne_zero, ne_comm]
let q := fun i ↦ p i / (1 - p i₀)
have hq : ∑ i ∈ s, q i = 1 := by rw [← Finset.sum_div, ← sum_insert_sub hi₀, hp, div_self h2pi₀]
have h2q : ∀ i ∈ s, 0 ≤ q i := fun i hi ↦ div_nonneg (h2p i <| mem_insert_of_mem hi) hpi₀
calc
∫⁻ a, ∏ i ∈ insert i₀ s, f i a ^ p i ∂μ = ∫⁻ a, f i₀ a ^ p i₀ * ∏ i ∈ s, f i a ^ p i ∂μ := by simp [hi₀]
_ = ∫⁻ a, f i₀ a ^ p i₀ * (∏ i ∈ s, f i a ^ q i) ^ (1 - p i₀) ∂μ := by
simp [q, ← ENNReal.prod_rpow_of_nonneg hpi₀, ← ENNReal.rpow_mul, div_mul_cancel₀ (h := h2pi₀)]
_ ≤ (∫⁻ a, f i₀ a ∂μ) ^ p i₀ * (∫⁻ a, ∏ i ∈ s, f i a ^ q i ∂μ) ^ (1 - p i₀) :=
by
apply ENNReal.lintegral_mul_norm_pow_le
· exact hf i₀ <| mem_insert_self ..
· exact s.aemeasurable_fun_prod fun i hi ↦ (hf i <| mem_insert_of_mem hi).pow_const _
· exact h2p i₀ <| mem_insert_self ..
· exact hpi₀
· apply add_sub_cancel
_ ≤ (∫⁻ a, f i₀ a ∂μ) ^ p i₀ * (∏ i ∈ s, (∫⁻ a, f i a ∂μ) ^ q i) ^ (1 - p i₀) :=
by
gcongr -- behavior of gcongr is heartbeat-dependent, which makes code really fragile...
exact ih (fun i hi ↦ hf i <| mem_insert_of_mem hi) hq h2q
_ = (∫⁻ a, f i₀ a ∂μ) ^ p i₀ * ∏ i ∈ s, (∫⁻ a, f i a ∂μ) ^ p i := by
simp [q, ← ENNReal.prod_rpow_of_nonneg hpi₀, ← ENNReal.rpow_mul, div_mul_cancel₀ (h := h2pi₀)]
_ = ∏ i ∈ insert i₀ s, (∫⁻ a, f i a ∂μ) ^ p i := by simp [hi₀]
