English
Continuing the measurable supersets construction, there exist measurable supersets with zero μ-intersection for the limRatio bounds.
Русский
Продолжение построения измеримых надмножеств; существуют измеримые надмножества с нулевой μ-пересечностью для границ 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
/-- If, for all `x` in a set `s`, one has frequently `ρ a / μ a < p`, then `ρ s ≤ p * μ s`, as
proved in `measure_le_of_frequently_le`. Since `ρ a / μ a` tends almost everywhere to
`v.limRatioMeas hρ x`, the same property holds for sets `s` on which `v.limRatioMeas hρ < p`. -/
theorem measure_le_mul_of_subset_limRatioMeas_lt {p : ℝ≥0} {s : Set α} (h : s ⊆ {x | v.limRatioMeas hρ x < p}) :
ρ s ≤ p * μ s :=
by
let t := {x : α | Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))}
have A : μ tᶜ = 0 := v.ae_tendsto_limRatioMeas hρ
suffices H : ρ (s ∩ t) ≤ (p • μ) (s ∩ t) by
calc
ρ s = ρ (s ∩ t ∪ s ∩ tᶜ) := by rw [inter_union_compl]
_ ≤ ρ (s ∩ t) + ρ (s ∩ tᶜ) := (measure_union_le _ _)
_ ≤ (p • μ) (s ∩ t) + ρ tᶜ := by gcongr; apply inter_subset_right
_ ≤ p * μ (s ∩ t) := by simp [(hρ A)]
_ ≤ p * μ s := by gcongr; apply inter_subset_left
refine v.measure_le_of_frequently_le (p • μ) hρ _ fun x hx => ?_
have I : ∀ᶠ b : Set α in v.filterAt x, ρ b / μ b < p := (tendsto_order.1 hx.2).2 _ (h hx.1)
apply I.frequently.mono fun a ha => ?_
rw [coe_nnreal_smul_apply]
refine (ENNReal.div_le_iff_le_mul ?_ (Or.inr (bot_le.trans_lt ha).ne')).1 ha.le
simp only [ENNReal.coe_ne_top, Ne, or_true, not_false_iff]
