Spheres and balls in pseudo-metric spaces

A sphere of positive radius r < R lies in the open ball of radius R about the same centre (Metric.sphere_abs_subset_ball); the radius is written |r|, as in circle integrals.

For R > 0 and a ratio c > 1, the annuli R c ^ k ≤ dist y x < R c ^ (k + 1), k ∈ ℤ, cover the points at positive distance from x (Metric.iUnion_ball_diff_ball_mul_zpow). With c = 2 this is the dyadic decomposition used to split singular integrals into shells.

Along l ×ˢ 𝓝 x, a radius sequence tending to zero plus the distance to x eventually stays below any positive r (Metric.eventually_add_dist_lt_of_tendsto_zero), so the closed balls of those radii about the points near x eventually lie in ball x r.

On the real line, the extended distance from b to a ≤ b is b - a (Real.edist_eq_ofReal_sub_of_le).

theorem Metric.sphere_abs_subset_ball {X : Type u_1} [PseudoMetricSpace X] {x : X} {r R : ℝ} (hr : r ∈ Set.Ioo 0 R) : sphere x |r| ⊆ ball x R

A sphere of positive radius r < R lies in the open ball of radius R about the same centre; the radius is written |r|, as in circle integrals.

theorem Metric.iUnion_ball_diff_ball_mul_zpow {X : Type u_1} [PseudoMetricSpace X] (x : X) {R c : ℝ} (hR : 0 < R) (hc : 1 < c) : ⋃ (k : ℤ), ball x (R * c ^ (k + 1)) \ ball x (R * c ^ k) = (closedBall x 0)ᶜ

For R > 0 and c > 1, the annuli R c ^ k ≤ dist y x < R c ^ (k + 1), k ∈ ℤ, cover exactly the points at positive distance from x, the complement of closedBall x 0. In a metric space that complement is {x}ᶜ (Metric.closedBall_zero).

theorem Metric.eventually_add_dist_lt_of_tendsto_zero {ι : Type u_1} {X : Type u_2} [PseudoMetricSpace X] {x : X} {l : Filter ι} {r : ℝ} (hr : 0 < r) {rho : ι → ℝ} (hrho : Filter.Tendsto rho l (nhds 0)) : ∀ᶠ (p : ι × X) in l ×ˢ nhds x, rho p.1 + dist p.2 x < r

Eventually along l ×ˢ 𝓝 x, a radius sequence tending to zero plus the distance to x stays below any positive r.

theorem Real.edist_eq_ofReal_sub_of_le {a b : ℝ} (h : a ≤ b) : edist b a = ENNReal.ofReal (b - a)

On the real line, the extended distance from b to a ≤ b is b - a.