Documentation

LeanPool.Besicovitch.Geometry.BallUnion

Finite unions of metric balls #

This file collects the finite-ball estimates used in the packing-to-measure transfer.

source
def LeanPool.Besicovitch.finiteBallUnion {X : Type u_1} {ι : Type u_2} [PseudoMetricSpace X] (support : Finset ι) (center : ↥support → X) (radius : ↥support → ℝ) :
Set X

The union of open balls indexed by a finite support.

Equations
Instances For
    source
    @[simp]
    theorem LeanPool.Besicovitch.mem_finiteBallUnion {X : Type u_1} {ι : Type u_2} [PseudoMetricSpace X] {support : Finset ι} {center : ↥support → X} {radius : ↥support → ℝ} {x : X} :
    x ∈ finiteBallUnion support center radius ↔ ∃ (i : ↥support), x ∈ Metric.ball (center i) (radius i)

    Membership in a finite ball union is witnessed by one supported ball.

    source
    theorem LeanPool.Besicovitch.ball_subset_finiteBallUnion {X : Type u_1} {ι : Type u_2} [PseudoMetricSpace X] {support : Finset ι} (center : ↥support → X) (radius : ↥support → ℝ) (i : ↥support) :
    Metric.ball (center i) (radius i) ⊆ finiteBallUnion support center radius

    Every supported ball lies in the corresponding finite ball union.

    source
    theorem LeanPool.Besicovitch.isOpen_finiteBallUnion {X : Type u_1} {ι : Type u_2} [PseudoMetricSpace X] {support : Finset ι} (center : ↥support → X) (radius : ↥support → ℝ) :
    IsOpen (finiteBallUnion support center radius)

    A finite ball union is open.

    source
    @[simp]
    theorem LeanPool.Besicovitch.finiteBallUnion_nonempty {X : Type u_1} {ι : Type u_2} [PseudoMetricSpace X] {support : Finset ι} {center : ↥support → X} {radius : ↥support → ℝ} :
    (finiteBallUnion support center radius).Nonempty ↔ ∃ (i : ↥support), 0 < radius i

    A finite ball union is nonempty exactly when one supported radius is positive.

    source
    theorem LeanPool.Besicovitch.pairwise_disjoint_ball_of_add_le_dist {X : Type u_1} {ι : Type u_2} [PseudoMetricSpace X] {support : Finset ι} (center : ↥support → X) (radius : ↥support → ℝ) (hsep : ∀ (i j : ↥support), i ≠ j → radius i + radius j ≤ dist (center i) (center j)) :
    Pairwise fun (i j : ↥support) => Disjoint (Metric.ball (center i) (radius i)) (Metric.ball (center j) (radius j))

    Open balls satisfying the pairwise separation inequalities are pairwise disjoint.

    source
    theorem LeanPool.Besicovitch.ediam_finiteBallUnion_le {X : Type u_1} {ι : Type u_2} [PseudoMetricSpace X] {support : Finset ι} (hsupport : support.Nonempty) (center : ↥support → X) (radius : ↥support → ℝ) :
    Metric.ediam (finiteBallUnion support center radius) ≤ ENNReal.ofReal (support.attach.sup' ⋯ fun (i : ↥support) => support.attach.sup' ⋯ fun (j : ↥support) => dist (center i) (center j) + radius i + radius j)

    The extended diameter of a finite ball union is bounded by its center-radius maximum.

    source
    theorem LeanPool.Besicovitch.measurableSet_finiteBallUnion {X : Type u_1} {ι : Type u_2} [PseudoMetricSpace X] {support : Finset ι} [MeasurableSpace X] [OpensMeasurableSpace X] (center : ↥support → X) (radius : ↥support → ℝ) :
    MeasurableSet (finiteBallUnion support center radius)

    A finite ball union is measurable in the Borel measurable structure.