English
For a given K, there exists a finite C such that for all small ε, all x, and all t ≤ K, μ(B(x,tε)) ≤ C μ(B(x,ε)).
Русский
Для заданного K существует конечная константа C: для всех малых ε, всех x и всех t ≤ K выполняется μ(B(x,tε)) ≤ C μ(B(x,ε)).
LaTeX
$$$$ \\exists C\\in \\mathbb{R}_{\\ge 0},\\ \\forall^*\\varepsilon>0,\\ \\forall x,\\ \\forall t\\le K,\\ \\mu(\\overline{B}(x,t\\varepsilon)) \\le C\\,\\mu(\\overline{B}(x,\\varepsilon)). $$$$
Lean4
theorem exists_eventually_forall_measure_closedBall_le_mul (K : ℝ) :
∃ C : ℝ≥0, ∀ᶠ ε in 𝓝[>] 0, ∀ x, ∀ t ≤ K, μ (closedBall x (t * ε)) ≤ C * μ (closedBall x ε) :=
by
let C := doublingConstant μ
have hμ : ∀ n : ℕ, ∀ᶠ ε in 𝓝[>] 0, ∀ x, μ (closedBall x ((2 : ℝ) ^ n * ε)) ≤ ↑(C ^ n) * μ (closedBall x ε) := fun n ↦
by
induction n with
| zero => simp
| succ n ih =>
replace ih := eventually_nhdsGT_zero_mul_left (two_pos : 0 < (2 : ℝ)) ih
refine (ih.and (exists_measure_closedBall_le_mul' μ)).mono fun ε hε x => ?_
calc
μ (closedBall x ((2 : ℝ) ^ (n + 1) * ε)) = μ (closedBall x ((2 : ℝ) ^ n * (2 * ε))) := by
rw [pow_succ, mul_assoc]
_ ≤ ↑(C ^ n) * μ (closedBall x (2 * ε)) := (hε.1 x)
_ ≤ ↑(C ^ n) * (C * μ (closedBall x ε)) := by gcongr; exact hε.2 x
_ = ↑(C ^ (n + 1)) * μ (closedBall x ε) := by rw [← mul_assoc, pow_succ, ENNReal.coe_mul]
rcases lt_or_ge K 1 with (hK | hK)
· refine ⟨1, ?_⟩
simp only [ENNReal.coe_one, one_mul]
refine eventually_mem_nhdsWithin.mono fun ε hε x t ht ↦ ?_
gcongr
nlinarith [mem_Ioi.mp hε]
· use C ^ ⌈Real.logb 2 K⌉₊
filter_upwards [hμ ⌈Real.logb 2 K⌉₊, eventually_mem_nhdsWithin] with ε hε hε₀ x t ht
refine le_trans ?_ (hε x)
gcongr
· exact (mem_Ioi.mp hε₀).le
· refine ht.trans ?_
rw [← Real.rpow_natCast, ← Real.logb_le_iff_le_rpow]
exacts [Nat.le_ceil _, by simp, by linarith]
