English
If f is measurable and a.e. finite, the equality between the lintegral with density f and the lintegral of f·g holds for all g measurable a.e.
Русский
Если f измерима и почти что конечна, равенство между линтегралом с плотностью f и линтегралом от f·g верно для всех g измеримых a.e.
LaTeX
$$$\int g \, d(\mu.withDensity f) = \int (f \cdot g) \, d\mu$ при условиях на f$$
Lean4
theorem lintegral_withDensity_eq_lintegral_mul_non_measurable (μ : Measure α) {f : α → ℝ≥0∞} (f_meas : Measurable f)
(hf : ∀ᵐ x ∂μ, f x < ∞) (g : α → ℝ≥0∞) : ∫⁻ a, g a ∂μ.withDensity f = ∫⁻ a, (f * g) a ∂μ :=
by
refine le_antisymm (lintegral_withDensity_le_lintegral_mul μ f_meas g) ?_
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 : (fun x => (f x)⁻¹ * i x) ≤ g := by
intro x
dsimp
rw [mul_comm, ← div_eq_mul_inv]
exact div_le_of_le_mul' (hi x)
refine le_iSup_of_le (fun x => (f x)⁻¹ * i x) (le_iSup_of_le (f_meas.inv.mul i_meas) ?_)
refine le_iSup_of_le A ?_
rw [lintegral_withDensity_eq_lintegral_mul _ f_meas (f_meas.inv.mul i_meas)]
apply lintegral_mono_ae
filter_upwards [hf]
intro x h'x
rcases eq_or_ne (f x) 0 with (hx | hx)
· have := hi x
simp only [hx, zero_mul, Pi.mul_apply, nonpos_iff_eq_zero] at this
simp [this]
· apply le_of_eq _
dsimp
rw [← mul_assoc, ENNReal.mul_inv_cancel hx h'x.ne, one_mul]
