English
If f is NNReal-valued and measurable, then AEStronglyMeasurable g with density μ.withDensity f equals AEStronglyMeasurable (f.toReal) • g with respect to μ.
Русский
Если f неотрицательная ненегативная величина, измерима, тогда AEStronglyMeasurable g с плотностью μ.withDensity f эквивалентно AEStronglyMeasurable ((f.toReal) • g) относительно μ.
LaTeX
$$$ AEStronglyMeasurable\\, g (μ.withDensity f) \\iff AEStronglyMeasurable\\, ((f)_{\\mathbb{R}} \\cdot g) \\ μ $$$
Lean4
theorem aestronglyMeasurable_withDensity_iff {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : α → ℝ≥0}
(hf : Measurable f) {g : α → E} :
AEStronglyMeasurable g (μ.withDensity fun x => (f x : ℝ≥0∞)) ↔ AEStronglyMeasurable (fun x => (f x : ℝ) • g x) μ :=
by
constructor
· rintro ⟨g', g'meas, hg'⟩
have A : MeasurableSet {x : α | f x ≠ 0} := (hf (measurableSet_singleton 0)).compl
refine ⟨fun x => (f x : ℝ) • g' x, hf.coe_nnreal_real.stronglyMeasurable.smul g'meas, ?_⟩
apply @ae_of_ae_restrict_of_ae_restrict_compl _ _ _ {x | f x ≠ 0}
· rw [EventuallyEq, ae_withDensity_iff hf.coe_nnreal_ennreal] at hg'
rw [ae_restrict_iff' A]
filter_upwards [hg'] with a ha h'a
have : (f a : ℝ≥0∞) ≠ 0 := by simpa only [Ne, ENNReal.coe_eq_zero] using h'a
rw [ha this]
· filter_upwards [ae_restrict_mem A.compl] with x hx
simp only [Classical.not_not, mem_setOf_eq, mem_compl_iff] at hx
simp [hx]
· rintro ⟨g', g'meas, hg'⟩
refine ⟨fun x => (f x : ℝ)⁻¹ • g' x, hf.coe_nnreal_real.inv.stronglyMeasurable.smul g'meas, ?_⟩
rw [EventuallyEq, ae_withDensity_iff hf.coe_nnreal_ennreal]
filter_upwards [hg'] with x hx h'x
rw [← hx, smul_smul, inv_mul_cancel₀, one_smul]
simp only [Ne, ENNReal.coe_eq_zero] at h'x
simpa only [NNReal.coe_eq_zero, Ne] using h'x
