English
For a Vitali family v with parameter K, every closed ball centered at y with radius r lies in the setsAt x of the Vitali family whenever dist(x,y) ≤ K r.
Русский
Для семейства Vitali v с параметром K каждых замкнутый шар вокруг точки y радиуса r принадлежит множеству setsAt x семействa Vitali, если расстояние dist(x,y) ≤ K r.
LaTeX
$$$\forall x,y,r,\ dist(x,y) \le K r \implies \ \overline{B}(y,r) \in (\text{vitaliFamily } μ K).\text{setsAt } x.$$$
Lean4
/-- In the Vitali family `IsUnifLocDoublingMeasure.vitaliFamily K`, the sets based at `x`
contain all balls `closedBall y r` when `dist x y ≤ K * r`. -/
theorem closedBall_mem_vitaliFamily_of_dist_le_mul {K : ℝ} {x y : α} {r : ℝ} (h : dist x y ≤ K * r) (rpos : 0 < r) :
closedBall y r ∈ (vitaliFamily μ K).setsAt x :=
by
let R := scalingScaleOf μ (max (4 * K + 3) 3)
simp only [vitaliFamily, VitaliFamily.enlarge, Vitali.vitaliFamily, mem_union, mem_setOf_eq, isClosed_closedBall,
true_and, (nonempty_ball.2 rpos).mono ball_subset_interior_closedBall, measurableSet_closedBall]
/- The measure is doubling on scales smaller than `R`. Therefore, we treat differently small
and large balls. For large balls, this follows directly from the enlargement we used in the
definition. -/
by_cases H : closedBall y r ⊆ closedBall x (R / 4)
swap; · exact Or.inr H
left
/- For small balls, there is the difficulty that `r` could be large but still the ball could be
small, if the annulus `{y | ε ≤ dist y x ≤ R/4}` is empty. We split between the cases `r ≤ R`
and `r > R`, and use the doubling for the former and rough estimates for the latter. -/
rcases le_or_gt r R with (hr | hr)
· refine ⟨(K + 1) * r, ?_⟩
constructor
· apply closedBall_subset_closedBall'
rw [dist_comm]
linarith
· have I1 : closedBall x (3 * ((K + 1) * r)) ⊆ closedBall y ((4 * K + 3) * r) :=
by
apply closedBall_subset_closedBall'
linarith
have I2 : closedBall y ((4 * K + 3) * r) ⊆ closedBall y (max (4 * K + 3) 3 * r) :=
by
apply closedBall_subset_closedBall
exact mul_le_mul_of_nonneg_right (le_max_left _ _) rpos.le
apply (measure_mono (I1.trans I2)).trans
exact measure_mul_le_scalingConstantOf_mul _ ⟨zero_lt_three.trans_le (le_max_right _ _), le_rfl⟩ hr
· refine ⟨R / 4, H, ?_⟩
have : closedBall x (3 * (R / 4)) ⊆ closedBall y r :=
by
apply closedBall_subset_closedBall'
have A : y ∈ closedBall y r := mem_closedBall_self rpos.le
have B := mem_closedBall'.1 (H A)
linarith
apply (measure_mono this).trans _
refine le_mul_of_one_le_left (zero_le _) ?_
exact ENNReal.one_le_coe_iff.2 (le_max_right _ _)
