English
As a consequence, similar measurable supersets exist for piers of limRatio in the separable setting, reinforcing measurability of limRatio.
Русский
Следствие, что существуют измеримые надмножества, усиливающие свойства limRatio в разделяемой ситуации, вновь подтверждая измеримость limRatio.
LaTeX
$$Same as above with refined simplifications.$$
Lean4
/-- If a measure `ρ` is singular with respect to `μ`, then for `μ` almost every `x`, the ratio
`ρ a / μ a` tends to zero when `a` shrinks to `x` along the Vitali family. This makes sense
as `μ a` is eventually positive by `ae_eventually_measure_pos`. -/
theorem ae_eventually_measure_zero_of_singular (hρ : ρ ⟂ₘ μ) :
∀ᵐ x ∂μ, Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 0) :=
by
have A : ∀ ε > (0 : ℝ≥0), ∀ᵐ x ∂μ, ∀ᶠ a in v.filterAt x, ρ a < ε * μ a :=
by
intro ε εpos
set s := {x | ¬∀ᶠ a in v.filterAt x, ρ a < ε * μ a} with hs
change μ s = 0
obtain ⟨o, _, ρo, μo⟩ : ∃ o : Set α, MeasurableSet o ∧ ρ o = 0 ∧ μ oᶜ = 0 := hρ
apply le_antisymm _ bot_le
calc
μ s ≤ μ (s ∩ o ∪ oᶜ) := by
conv_lhs => rw [← inter_union_compl s o]
gcongr
apply inter_subset_right
_ ≤ μ (s ∩ o) + μ oᶜ := (measure_union_le _ _)
_ = μ (s ∩ o) := by rw [μo, add_zero]
_ = (ε : ℝ≥0∞)⁻¹ * (ε • μ) (s ∩ o) :=
by
simp only [coe_nnreal_smul_apply, ← mul_assoc, mul_comm _ (ε : ℝ≥0∞)]
rw [ENNReal.mul_inv_cancel (ENNReal.coe_pos.2 εpos).ne' ENNReal.coe_ne_top, one_mul]
_ ≤ (ε : ℝ≥0∞)⁻¹ * ρ (s ∩ o) := by
gcongr
refine v.measure_le_of_frequently_le ρ smul_absolutelyContinuous _ ?_
intro x hx
rw [hs] at hx
simp only [mem_inter_iff, not_lt, not_eventually, mem_setOf_eq] at hx
exact hx.1
_ ≤ (ε : ℝ≥0∞)⁻¹ * ρ o := by gcongr; apply inter_subset_right
_ = 0 := by rw [ρo, mul_zero]
obtain ⟨u, _, u_pos, u_lim⟩ : ∃ u : ℕ → ℝ≥0, StrictAnti u ∧ (∀ n : ℕ, 0 < u n) ∧ Tendsto u atTop (𝓝 0) :=
exists_seq_strictAnti_tendsto (0 : ℝ≥0)
have B : ∀ᵐ x ∂μ, ∀ n, ∀ᶠ a in v.filterAt x, ρ a < u n * μ a := ae_all_iff.2 fun n => A (u n) (u_pos n)
filter_upwards [B, v.ae_eventually_measure_pos]
intro x hx h'x
refine tendsto_order.2 ⟨fun z hz => (ENNReal.not_lt_zero hz).elim, fun z hz => ?_⟩
obtain ⟨w, w_pos, w_lt⟩ : ∃ w : ℝ≥0, (0 : ℝ≥0∞) < w ∧ (w : ℝ≥0∞) < z := ENNReal.lt_iff_exists_nnreal_btwn.1 hz
obtain ⟨n, hn⟩ : ∃ n, u n < w := ((tendsto_order.1 u_lim).2 w (ENNReal.coe_pos.1 w_pos)).exists
filter_upwards [hx n, h'x, v.eventually_measure_lt_top x]
intro a ha μa_pos μa_lt_top
rw [ENNReal.div_lt_iff (Or.inl μa_pos.ne') (Or.inl μa_lt_top.ne)]
exact ha.trans_le (mul_le_mul_right' ((ENNReal.coe_le_coe.2 hn.le).trans w_lt.le) _)
