English
Hölder-type bound: a scalar function f integrable, multiplied by a scalar g with finite essSup of ‖g‖, yields integrable g•f.
Русский
Гёделевское неравенство: если f интегрируемо, g существенно ограничено по норме, то g·f интегрируемо.
LaTeX
$$$ (Integrable\\ f\\ μ) \\Rightarrow ∀ {g}, AEStronglyMeasurable\\ g μ \\land essSup (\\|g·\\|) μ \u2260 ∞ \\Rightarrow Integrable( x \\mapsto g(x)•f(x) ) μ $$$
Lean4
/-- Hölder's inequality for integrable functions: the scalar multiplication of an integrable
scalar-valued function by a vector-value function with finite essential supremum is integrable. -/
theorem smul_essSup {𝕜 : Type*} [NormedRing 𝕜] [MulActionWithZero 𝕜 β] [IsBoundedSMul 𝕜 β] {f : α → 𝕜}
(hf : Integrable f μ) {g : α → β} (g_aestronglyMeasurable : AEStronglyMeasurable g μ)
(ess_sup_g : essSup (‖g ·‖ₑ) μ ≠ ∞) : Integrable (fun x : α => f x • g x) μ :=
by
rw [← memLp_one_iff_integrable] at *
refine ⟨hf.1.smul g_aestronglyMeasurable, ?_⟩
have hg' : eLpNorm g ∞ μ ≠ ∞ := by rwa [eLpNorm_exponent_top]
calc
eLpNorm (fun x : α => f x • g x) 1 μ ≤ _ := by
simpa using MeasureTheory.eLpNorm_smul_le_mul_eLpNorm g_aestronglyMeasurable hf.1 (p := 1) (q := ∞)
_ < ∞ := ENNReal.mul_lt_top hf.2 hg'.lt_top
