English
Lebesgue differentiation holds for Vitali families: almost every point of a Lebesgue density point of a set S has density 1.
Русский
Лебеговская дифференциация выполняется для Vitali: почти каждая точка множества имеет плотность 1.
LaTeX
$$$\forall^{\mu}\ x\, (x\in S)\implies\lim_{a\to x} \frac{μ(S\cap a)}{μ(a)} = 1.$$$
Lean4
theorem blimsup_cthickening_ae_eq_blimsup_thickening {p : ℕ → Prop} {s : ℕ → Set α} {r : ℕ → ℝ}
(hr : Tendsto r atTop (𝓝 0)) (hr' : ∀ᶠ i in atTop, p i → 0 < r i) :
(blimsup (fun i => cthickening (r i) (s i)) atTop p : Set α) =ᵐ[μ]
(blimsup (fun i => thickening (r i) (s i)) atTop p : Set α) :=
by
refine eventuallyLE_antisymm_iff.mpr ⟨?_, HasSubset.Subset.eventuallyLE (?_ : _ ≤ _)⟩
· rw [eventuallyLE_congr (blimsup_cthickening_mul_ae_eq μ p s (one_half_pos (α := ℝ)) r hr).symm EventuallyEq.rfl]
apply HasSubset.Subset.eventuallyLE
change _ ≤ _
refine mono_blimsup' (hr'.mono fun i hi pi => cthickening_subset_thickening' (hi pi) ?_ (s i))
nlinarith [hi pi]
· exact mono_blimsup fun i _ => thickening_subset_cthickening _ _
