English
If f is integrable and nonnegative, then for any nonnegative g, the lintegral of g with density f is at most the lintegral of f·g with respect to μ.
Русский
Пусть f неотрицательная и интегрируемая; для любого неотрицательного g выполняется неравенство: линтеграл по μ.withDensity f от g не превосходит линтеграл по μ от f·g.
LaTeX
$$$\int g \, d(\mu.withDensity f) \le\int (f \cdot g) \, d\mu$$$
Lean4
theorem lintegral_withDensity_le_lintegral_mul (μ : Measure α) {f : α → ℝ≥0∞} (f_meas : Measurable f) (g : α → ℝ≥0∞) :
(∫⁻ a, g a ∂μ.withDensity f) ≤ ∫⁻ a, (f * g) a ∂μ :=
by
rw [← iSup_lintegral_measurable_le_eq_lintegral, ← iSup_lintegral_measurable_le_eq_lintegral]
refine iSup₂_le fun i i_meas => iSup_le fun hi => ?_
have A : f * i ≤ f * g := fun x => mul_le_mul_left' (hi x) _
refine le_iSup₂_of_le (f * i) (f_meas.mul i_meas) ?_
exact le_iSup_of_le A (le_of_eq (lintegral_withDensity_eq_lintegral_mul _ f_meas i_meas))
