English
On the real line, the Vitali family ensures that the sets of the form Icc x y sit in setsAt x and setsAt y in the appropriate limit sense.
Русский
На вещественной прямой множество Icc x y принадлежит setsAt x и setsAt y в соответствующем предельном смысле.
LaTeX
$$$Icc\,x\,y \in (vitaliFamily(volume\,1).setsAt\,x)$ и аналогично для y.$$
Lean4
/-- Given a sequence of subsets `sᵢ` of a metric space, together with a sequence of radii `rᵢ`
such that `rᵢ → 0`, the set of points which belong to infinitely many of the closed
`rᵢ`-thickenings of `sᵢ` is unchanged almost everywhere for a uniformly locally doubling measure if
the `rᵢ` are all scaled by a positive constant.
This lemma is a generalisation of Lemma 9 appearing on page 217 of
[J.W.S. Cassels, *Some metrical theorems in Diophantine approximation. I*](cassels1950).
See also `blimsup_thickening_mul_ae_eq`.
NB: The `: Set α` type ascription is present because of
https://github.com/leanprover-community/mathlib/issues/16932. -/
theorem blimsup_cthickening_mul_ae_eq (p : ℕ → Prop) (s : ℕ → Set α) {M : ℝ} (hM : 0 < M) (r : ℕ → ℝ)
(hr : Tendsto r atTop (𝓝 0)) :
(blimsup (fun i => cthickening (M * r i) (s i)) atTop p : Set α) =ᵐ[μ]
(blimsup (fun i => cthickening (r i) (s i)) atTop p : Set α) :=
by
have :
∀ (p : ℕ → Prop) {r : ℕ → ℝ} (_ : Tendsto r atTop (𝓝[>] 0)),
(blimsup (fun i => cthickening (M * r i) (s i)) atTop p : Set α) =ᵐ[μ]
(blimsup (fun i => cthickening (r i) (s i)) atTop p : Set α) :=
by
clear p hr r; intro p r hr
have hr' : Tendsto (fun i => M * r i) atTop (𝓝[>] 0) := by
convert TendstoNhdsWithinIoi.const_mul hM hr <;> simp only [mul_zero]
refine eventuallyLE_antisymm_iff.mpr ⟨?_, ?_⟩
·
exact
blimsup_cthickening_ae_le_of_eventually_mul_le μ p (inv_pos.mpr hM) hr'
(Eventually.of_forall fun i => by rw [inv_mul_cancel_left₀ hM.ne' (r i)])
· exact blimsup_cthickening_ae_le_of_eventually_mul_le μ p hM hr (Eventually.of_forall fun i => le_refl _)
let r' : ℕ → ℝ := fun i => if 0 < r i then r i else 1 / ((i : ℝ) + 1)
have hr' : Tendsto r' atTop (𝓝[>] 0) :=
by
refine
tendsto_nhdsWithin_iff.mpr
⟨Tendsto.if' hr tendsto_one_div_add_atTop_nhds_zero_nat, Eventually.of_forall fun i => ?_⟩
by_cases hi : 0 < r i
· simp [r', hi]
· simp only [r', hi, one_div, mem_Ioi, if_false, inv_pos]; positivity
have h₀ : ∀ i, p i ∧ 0 < r i → cthickening (r i) (s i) = cthickening (r' i) (s i) := by grind
have h₁ : ∀ i, p i ∧ 0 < r i → cthickening (M * r i) (s i) = cthickening (M * r' i) (s i) := by rintro i ⟨-, hi⟩;
simp only [r', hi, if_true]
have h₂ : ∀ i, p i ∧ r i ≤ 0 → cthickening (M * r i) (s i) = cthickening (r i) (s i) :=
by
rintro i ⟨-, hi⟩
have hi' : M * r i ≤ 0 := mul_nonpos_of_nonneg_of_nonpos hM.le hi
rw [cthickening_of_nonpos hi, cthickening_of_nonpos hi']
have hp : p = fun i => p i ∧ 0 < r i ∨ p i ∧ r i ≤ 0 := by ext i; simp [← and_or_left, lt_or_ge 0 (r i)]
rw [hp, blimsup_or_eq_sup, blimsup_or_eq_sup]
simp only [sup_eq_union]
rw [blimsup_congr (Eventually.of_forall h₀), blimsup_congr (Eventually.of_forall h₁),
blimsup_congr (Eventually.of_forall h₂)]
exact ae_eq_set_union (this (fun i => p i ∧ 0 < r i) hr') (ae_eq_refl _)
