English
There exists a finite C such that for ε small enough and every x, μ(closedBall(x,2ε)) ≤ C μ(closedBall(x,ε)).
Русский
Существует конечная константа C такая, что для малых ε и любого x выполняется μ(B(x,2ε)) ≤ C μ(B(x,ε)).
LaTeX
$$$$ \\exists C \\in \\mathbb{R}_{\\ge 0},\\ \\forall^*\\varepsilon>0,\\ \\forall x,\\mu(\\overline{B}(x,2\\varepsilon)) \\le C\\,\\mu(\\overline{B}(x,\\varepsilon)). $$$$
Lean4
theorem eventually_measure_mul_le_scalingConstantOf_mul (K : ℝ) :
∃ R : ℝ,
0 < R ∧ ∀ x t r, t ∈ Ioc 0 K → r ≤ R → μ (closedBall x (t * r)) ≤ scalingConstantOf μ K * μ (closedBall x r) :=
by
have h := Classical.choose_spec (exists_eventually_forall_measure_closedBall_le_mul μ K)
rcases mem_nhdsGT_iff_exists_Ioc_subset.1 h with ⟨R, Rpos, hR⟩
refine ⟨R, Rpos, fun x t r ht hr => ?_⟩
rcases lt_trichotomy r 0 with (rneg | rfl | rpos)
· have : t * r < 0 := mul_neg_of_pos_of_neg ht.1 rneg
simp only [closedBall_eq_empty.2 this, measure_empty, zero_le']
· simp only [mul_zero]
refine le_mul_of_one_le_of_le ?_ le_rfl
apply ENNReal.one_le_coe_iff.2 (le_max_right _ _)
· apply (hR ⟨rpos, hr⟩ x t ht.2).trans
gcongr
apply le_max_left
