English
If ρ ≪ μ, then for almost every x, the ratio ρ a / μ a converges along the Vitali filter: there exists c with Tendsto ρ a / μ a to c at x.
Русский
Если ρ ∥ μ, то почти для каждого x существует предел отношения ρ(a)/μ(a) вдоль фильтра Vitali.
LaTeX
$$$\forall x\ a.e.,\ exists c,\ Tendsto (a \mapsto ρ a / μ a) (v.filterAt x) (𝓝 c).$$$
Lean4
/-- If `ρ` is absolutely continuous with respect to `μ`, then for almost every `x`,
the ratio `ρ a / μ a` converges as `a` shrinks to `x` along a Vitali family for `μ`. -/
theorem ae_tendsto_div : ∀ᵐ x ∂μ, ∃ c, Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 c) :=
by
obtain ⟨w, w_count, w_dense, _, w_top⟩ : ∃ w : Set ℝ≥0∞, w.Countable ∧ Dense w ∧ 0 ∉ w ∧ ∞ ∉ w :=
ENNReal.exists_countable_dense_no_zero_top
have I : ∀ x ∈ w, x ≠ ∞ := fun x xs hx => w_top (hx ▸ xs)
have A :
∀ c ∈ w, ∀ d ∈ w, c < d → ∀ᵐ x ∂μ, ¬((∃ᶠ a in v.filterAt x, ρ a / μ a < c) ∧ ∃ᶠ a in v.filterAt x, d < ρ a / μ a) :=
by
intro c hc d hd hcd
lift c to ℝ≥0 using I c hc
lift d to ℝ≥0 using I d hd
apply v.null_of_frequently_le_of_frequently_ge hρ (ENNReal.coe_lt_coe.1 hcd)
· simp only [and_imp, exists_prop, not_frequently, not_and, not_lt, not_le, not_eventually, mem_setOf_eq,
mem_compl_iff, not_forall]
intro x h1x _
apply h1x.mono fun a ha => ?_
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]
· simp only [and_imp, exists_prop, not_frequently, not_and, not_lt, not_le, not_eventually, mem_setOf_eq,
mem_compl_iff, not_forall]
intro x _ h2x
apply h2x.mono fun a ha => ?_
exact ENNReal.mul_le_of_le_div ha.le
have B :
∀ᵐ x ∂μ, ∀ c ∈ w, ∀ d ∈ w, c < d → ¬((∃ᶠ a in v.filterAt x, ρ a / μ a < c) ∧ ∃ᶠ a in v.filterAt x, d < ρ a / μ a) :=
by
#adaptation_note /-- 2024-04-23
The next two lines were previously just `simpa only [ae_ball_iff w_count, ae_all_iff]` -/
rw [ae_ball_iff w_count]; intro x hx; rw [ae_ball_iff w_count]; revert x
simpa only [ae_all_iff]
filter_upwards [B]
intro x hx
exact tendsto_of_no_upcrossings w_dense hx
