English
AEMeasurability with respect to a density f is equivalent to AEMeasurability of the scaled g by f on μ.
Русский
AEMeasurable g относительно μ с плотностью f эквивалентно AEMeasurable (f · g) μ.
LaTeX
$$$AEMeasurable\\ g (μ.withDensity (fun x => (f x) : ℝ≥0∞)) \\iff AEMeasurable (fun x => (f x) \\cdot g x) μ$$$
Lean4
theorem aemeasurable_withDensity_iff {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [SecondCountableTopology E]
[MeasurableSpace E] [BorelSpace E] {f : α → ℝ≥0} (hf : Measurable f) {g : α → E} :
AEMeasurable g (μ.withDensity fun x => (f x : ℝ≥0∞)) ↔ AEMeasurable (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.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']
intro 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]
intro 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.smul g'meas, ?_⟩
rw [EventuallyEq, ae_withDensity_iff hf.coe_nnreal_ennreal]
filter_upwards [hg']
intro 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
