English
Refines the previous bounds with 2r scaling for general r, giving a similar contraction bound.
Русский
Уточнение предыдущих пределов с учётом масштаба 2r для общего радиуса r, сохранение сжатия.
LaTeX
$$∃δ>0, ∀ x,y с нормами ≤ r: ε ≤ ‖x−y‖ ⇒ ‖x+y‖ ≤ 2r − δ$$
Lean4
theorem exists_forall_closed_ball_dist_add_le_two_mul_sub (hε : 0 < ε) (r : ℝ) :
∃ δ, 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ ≤ r → ∀ ⦃y⦄, ‖y‖ ≤ r → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 * r - δ :=
by
obtain hr | hr := le_or_gt r 0
·
exact
⟨1, one_pos, fun x hx y hy h =>
(hε.not_ge <| h.trans <| (norm_sub_le _ _).trans <| add_nonpos (hx.trans hr) (hy.trans hr)).elim⟩
obtain ⟨δ, hδ, h⟩ := exists_forall_closed_ball_dist_add_le_two_sub E (div_pos hε hr)
refine ⟨δ * r, mul_pos hδ hr, fun x hx y hy hxy => ?_⟩
rw [← div_le_one hr, div_eq_inv_mul, ← norm_smul_of_nonneg (inv_nonneg.2 hr.le)] at hx hy
have := h hx hy
simp_rw [← smul_add, ← smul_sub, norm_smul_of_nonneg (inv_nonneg.2 hr.le), ← div_eq_inv_mul,
div_le_div_iff_of_pos_right hr, div_le_iff₀ hr, sub_mul] at this
exact this hxy
