English
If ρ is absolutely continuous with respect to μ, then for any measurable set s and for every moving threshold p, the measure ρ(s) is bounded by p times μ(s) whenever s is contained in the set where the ratio ρ/μ is less than p.
Русский
Если ρ абсолютно непрерывна по отношению к μ, то для любого измеримого множества s и каждого порога p мера ρ(s) не превышает p μ(s) при условии, что s лежит внутри области, где отношение ρ/μ меньше p.
LaTeX
$$$\rho(s) ≤ p \cdot μ(s)$ whenever $s \subseteq \{x : \limRatio(x) < p\}$.$$
Lean4
/-- If two measures `ρ` and `ν` have, at every point of a set `s`, arbitrarily small sets in a
Vitali family satisfying `ρ a ≤ ν a`, then `ρ s ≤ ν s` if `ρ ≪ μ`. -/
theorem measure_le_of_frequently_le [SecondCountableTopology α] [BorelSpace α] {ρ : Measure α} (ν : Measure α)
[IsLocallyFiniteMeasure ν] (hρ : ρ ≪ μ) (s : Set α) (hs : ∀ x ∈ s, ∃ᶠ a in v.filterAt x, ρ a ≤ ν a) : ρ s ≤ ν s :=
by
-- this follows from a covering argument using the sets satisfying `ρ a ≤ ν a`.
apply ENNReal.le_of_forall_pos_le_add fun ε εpos _ => ?_
obtain ⟨U, sU, U_open, νU⟩ : ∃ (U : Set α), s ⊆ U ∧ IsOpen U ∧ ν U ≤ ν s + ε :=
exists_isOpen_le_add s ν (ENNReal.coe_pos.2 εpos).ne'
let f : α → Set (Set α) := fun _ => {a | ρ a ≤ ν a ∧ a ⊆ U}
have h : v.FineSubfamilyOn f s :=
by
apply v.fineSubfamilyOn_of_frequently f s fun x hx => ?_
have :=
(hs x hx).and_eventually
((v.eventually_filterAt_mem_setsAt x).and (v.eventually_filterAt_subset_of_nhds (U_open.mem_nhds (sU hx))))
apply Frequently.mono this
rintro a ⟨ρa, _, aU⟩
exact ⟨ρa, aU⟩
haveI : Encodable h.index := h.index_countable.toEncodable
calc
ρ s ≤ ∑' x : h.index, ρ (h.covering x) := h.measure_le_tsum_of_absolutelyContinuous hρ
_ ≤ ∑' x : h.index, ν (h.covering x) := (ENNReal.tsum_le_tsum fun x => (h.covering_mem x.2).1)
_ = ν (⋃ x : h.index, h.covering x) := by
rw [measure_iUnion h.covering_disjoint_subtype fun i => h.measurableSet_u i.2]
_ ≤ ν U := (measure_mono (iUnion_subset fun i => (h.covering_mem i.2).2))
_ ≤ ν s + ε := νU
