English
For p<q there exist measurable supersets a,b with disjointness up to μ-null and containing the corresponding limRatio sets.
Русский
Для p<q существуют измеримые надмножества a,b, которые раздельны почти по мере μ и содержат соответствующие множества limRatio.
LaTeX
$$$\exists a,b,\ MeasurableSet a ∧ MeasurableSet b ∧ {x: v.limRatio ρ x < p} ⊆ a ∧ {x: (q) < v.limRatio ρ x} ⊆ b ∧ μ(a ∩ b)=0.$$$
Lean4
/-- A set of points `s` satisfying both `ρ a ≤ c * μ a` and `ρ a ≥ d * μ a` at arbitrarily small
sets in a Vitali family has measure `0` if `c < d`. Indeed, the first inequality should imply
that `ρ s ≤ c * μ s`, and the second one that `ρ s ≥ d * μ s`, a contradiction if `0 < μ s`. -/
theorem null_of_frequently_le_of_frequently_ge {c d : ℝ≥0} (hcd : c < d) (s : Set α)
(hc : ∀ x ∈ s, ∃ᶠ a in v.filterAt x, ρ a ≤ c * μ a) (hd : ∀ x ∈ s, ∃ᶠ a in v.filterAt x, (d : ℝ≥0∞) * μ a ≤ ρ a) :
μ s = 0 := by
apply measure_null_of_locally_null s fun x _ => ?_
obtain ⟨o, xo, o_open, μo⟩ : ∃ o : Set α, x ∈ o ∧ IsOpen o ∧ μ o < ∞ := Measure.exists_isOpen_measure_lt_top μ x
refine ⟨s ∩ o, inter_mem_nhdsWithin _ (o_open.mem_nhds xo), ?_⟩
let s' := s ∩ o
by_contra h
apply lt_irrefl (ρ s')
calc
ρ s' ≤ c * μ s' := v.measure_le_of_frequently_le (c • μ) hρ s' fun x hx => hc x hx.1
_ < d * μ s' := by
apply (ENNReal.mul_lt_mul_right h _).2 (ENNReal.coe_lt_coe.2 hcd)
exact (lt_of_le_of_lt (measure_mono inter_subset_right) μo).ne
_ ≤ ρ s' := v.measure_le_of_frequently_le ρ smul_absolutelyContinuous s' fun x hx ↦ hd x hx.1
