The common pair of root balls

The direct pair-condition transfer charges both child extractions to one union of root balls.

def LeanPool.Besicovitch.rootBallUnion (x y : EuclideanSpace ℝ (Fin 2)) (r : ℝ) : Set (EuclideanSpace ℝ (Fin 2))

The common open neighborhood formed by two balls of the same radius.

Equations

• LeanPool.Besicovitch.rootBallUnion x y r = Metric.ball x r ∪ Metric.ball y r

theorem LeanPool.Besicovitch.isOpen_rootBallUnion (x y : EuclideanSpace ℝ (Fin 2)) (r : ℝ) : IsOpen (rootBallUnion x y r)

The common root-ball union is open.

theorem LeanPool.Besicovitch.ediam_rootBallUnion_le (x y : EuclideanSpace ℝ (Fin 2)) (r : ℝ) : Metric.ediam (rootBallUnion x y r) ≤ ENNReal.ofReal (dist x y + 2 * r)

The diameter of the common root-ball union is bounded by root distance plus two radii.