English
For finite measure μ, ∫(c + f) finite iff ∫f finite.
Русский
Для конечной меры μ: интегрируемость c + f эквивалентна интегрируемости f.
LaTeX
$$$ [IsFiniteMeasure\\ μ] \\Rightarrow Integrable(c+f) μ \\iff Integrable(f) μ $$$
Lean4
/-- **Hölder's inequality for integrable functions**: the scalar multiplication of an integrable
vector-valued function by a scalar function with finite essential supremum is integrable. -/
theorem essSup_smul {R : Type*} [NormedRing R] [Module R β] [IsBoundedSMul R β] {f : α → β} (hf : Integrable f μ)
{g : α → R} (g_aestronglyMeasurable : AEStronglyMeasurable g μ) (ess_sup_g : essSup (‖g ·‖ₑ) μ ≠ ∞) :
Integrable (fun x : α => g x • f x) μ :=
by
rw [← memLp_one_iff_integrable] at *
refine ⟨g_aestronglyMeasurable.smul hf.1, ?_⟩
have hg' : eLpNorm g ∞ μ ≠ ∞ := by rwa [eLpNorm_exponent_top]
calc
eLpNorm (fun x : α => g x • f x) 1 μ ≤ _ := by
simpa using MeasureTheory.eLpNorm_smul_le_mul_eLpNorm hf.1 g_aestronglyMeasurable (p := ∞) (q := 1)
_ < ∞ := ENNReal.mul_lt_top hg'.lt_top hf.2
