English
An explicit characterization of zero-density on a set s via intersection with {f ≠ 0}.
Русский
Явление нулевой плотности на s через пересечение с {f ≠ 0}.
LaTeX
$$$\\mu.withDensity f (s) = 0 \\iff \\mu\\bigl(\\{x \\mid f(x) \\neq 0\\} \\cap s\\bigr) = 0$$$
Lean4
theorem withDensity_apply_eq_zero' {f : α → ℝ≥0∞} {s : Set α} (hf : AEMeasurable f μ) :
μ.withDensity f s = 0 ↔ μ ({x | f x ≠ 0} ∩ s) = 0 :=
by
constructor
· intro hs
let t := toMeasurable (μ.withDensity f) s
apply measure_mono_null (inter_subset_inter_right _ (subset_toMeasurable (μ.withDensity f) s))
have A : μ.withDensity f t = 0 := by rw [measure_toMeasurable, hs]
rw [withDensity_apply f (measurableSet_toMeasurable _ s), lintegral_eq_zero_iff' (AEMeasurable.restrict hf),
EventuallyEq, ae_restrict_iff'₀, ae_iff] at A
swap
· simp only [measurableSet_toMeasurable, MeasurableSet.nullMeasurableSet]
simp only [Pi.zero_apply] at A
convert A using 2
ext x
simp only [and_comm, exists_prop, mem_inter_iff, mem_setOf_eq, not_forall]
· intro hs
let t := toMeasurable μ ({x | f x ≠ 0} ∩ s)
have A : s ⊆ t ∪ {x | f x = 0} := by
intro x hx
rcases eq_or_ne (f x) 0 with (fx | fx)
· simp only [fx, mem_union, mem_setOf_eq, or_true]
· left
apply subset_toMeasurable _ _
exact ⟨fx, hx⟩
apply measure_mono_null A (measure_union_null _ _)
· apply withDensity_absolutelyContinuous
rwa [measure_toMeasurable]
rcases hf with ⟨g, hg, hfg⟩
have t : {x | f x = 0} =ᵐ[μ.withDensity f] {x | g x = 0} :=
by
apply withDensity_absolutelyContinuous
filter_upwards [hfg] with a ha
rw [eq_iff_iff]
exact ⟨fun h ↦ by rw [h] at ha; exact ha.symm, fun h ↦ by rw [h] at ha; exact ha⟩
rw [measure_congr t, withDensity_congr_ae hfg]
have M : MeasurableSet {x : α | g x = 0} := hg (measurableSet_singleton _)
rw [withDensity_apply _ M, lintegral_eq_zero_iff hg]
filter_upwards [ae_restrict_mem M]
simp only [imp_self, Pi.zero_apply, imp_true_iff]
