English
Another auxiliary that gives an a.e. equivalence of thickening under scaling and under original radii for a fixed p-structure.
Русский
Ещё одна вспомогательная лемма о тождестве а.е. эквивалентности утолщения под масштабированием и под исходными радиусами.
LaTeX
$$$(\blimsup (i \mapsto Metric.cthickening (r i) (s i)) atTop p) =ᵐ[μ] (\blimsup (i \mapsto Metric.cthickening (M \cdot r i) (s i)) atTop p).$$$
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
`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_cthickening_mul_ae_eq`.
NB: The `: Set α` type ascription is present because of
https://github.com/leanprover-community/mathlib/issues/16932. -/
theorem blimsup_thickening_mul_ae_eq (p : ℕ → Prop) (s : ℕ → Set α) {M : ℝ} (hM : 0 < M) (r : ℕ → ℝ)
(hr : Tendsto r atTop (𝓝 0)) :
(blimsup (fun i => thickening (M * r i) (s i)) atTop p : Set α) =ᵐ[μ]
(blimsup (fun i => thickening (r i) (s i)) atTop p : Set α) :=
by
let q : ℕ → Prop := fun i => p i ∧ 0 < r i
have h₁ : blimsup (fun i => thickening (r i) (s i)) atTop p = blimsup (fun i => thickening (r i) (s i)) atTop q :=
by
refine blimsup_congr' (Eventually.of_forall fun i h => ?_)
replace hi : 0 < r i := by contrapose! h; apply thickening_of_nonpos h
simp only [q, hi, iff_self_and, imp_true_iff]
have h₂ :
blimsup (fun i => thickening (M * r i) (s i)) atTop p = blimsup (fun i => thickening (M * r i) (s i)) atTop q :=
by
refine blimsup_congr' (Eventually.of_forall fun i h ↦ ?_)
replace h : 0 < r i := by rw [← mul_pos_iff_of_pos_left hM]; contrapose! h; apply thickening_of_nonpos h
simp only [q, h, iff_self_and, imp_true_iff]
rw [h₁, h₂]
exact blimsup_thickening_mul_ae_eq_aux μ q s hM r hr (Eventually.of_forall fun i hi => hi.2)
