Documentation

LeanPool.Besicovitch.BesicovitchPairCondition.PackingMeasure

Measure estimates for two-color ball packings #

This file bounds the mass of a finite two-color ball packing by its union and leakage.

source
def LeanPool.Besicovitch.colorBallUnion (support : Finset SixPointIndex) (center : ↥support → EuclideanSpace ℝ (Fin 2)) (radius : ↥support → ℝ) (color : SixPointColor) :
Set (EuclideanSpace ℝ (Fin 2))

The union of the supported balls of one color.

Equations
Instances For
    source
    @[simp]
    theorem LeanPool.Besicovitch.mem_colorBallUnion {support : Finset SixPointIndex} {center : ↥support → EuclideanSpace ℝ (Fin 2)} {radius : ↥support → ℝ} {color : SixPointColor} {x : EuclideanSpace ℝ (Fin 2)} :
    x ∈ colorBallUnion support center radius color ↔ ∃ (i : ↥support), (↑i).1 = color ∧ x ∈ Metric.ball (center i) (radius i)

    Membership in a color ball union is witnessed by a supported index of that color.

    source
    theorem LeanPool.Besicovitch.finiteBallUnion_eq_union_colorBallUnion (support : Finset SixPointIndex) (center : ↥support → EuclideanSpace ℝ (Fin 2)) (radius : ↥support → ℝ) :
    finiteBallUnion support center radius = colorBallUnion support center radius SixPointColor.red ∪ colorBallUnion support center radius SixPointColor.blue

    The full ball union is the union of its red and blue parts.

    source
    theorem LeanPool.Besicovitch.isOpen_colorBallUnion (support : Finset SixPointIndex) (center : ↥support → EuclideanSpace ℝ (Fin 2)) (radius : ↥support → ℝ) (color : SixPointColor) :
    IsOpen (colorBallUnion support center radius color)

    A single-color finite ball union is open.

    source
    theorem LeanPool.Besicovitch.measurableSet_colorBallUnion (support : Finset SixPointIndex) (center : ↥support → EuclideanSpace ℝ (Fin 2)) (radius : ↥support → ℝ) (color : SixPointColor) :
    MeasurableSet (colorBallUnion support center radius color)

    A single-color finite ball union is measurable.

    source
    theorem LeanPool.Besicovitch.measure_colorBallUnion {support : Finset SixPointIndex} (center : ↥support → EuclideanSpace ℝ (Fin 2)) (radius : ↥support → ℝ) (color : SixPointColor) (μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin 2))) (hdisjoint : ∀ (i j : ↥support), i ≠ j → (↑i).1 = (↑j).1 → Disjoint (Metric.ball (center i) (radius i)) (Metric.ball (center j) (radius j))) :
    μ (colorBallUnion support center radius color) = ∑ i : { i : ↥support // (↑i).1 = color }, μ (Metric.ball (center ↑i) (radius ↑i))

    The measure of a disjoint single-color ball union is the sum of its ball measures.

    source
    theorem LeanPool.Besicovitch.inter_colorBallUnion_subset_sdiff {support : Finset SixPointIndex} (center : ↥support → EuclideanSpace ℝ (Fin 2)) (radius : ↥support → ℝ) (e : SixPointColor → Set (EuclideanSpace ℝ (Fin 2))) (he : ∀ (color : SixPointColor), (e color).Nonempty) (hcenter : ∀ (i : ↥support), center i ∈ e (↑i).1) (hradius : ∀ (i : ↥support), radius i ≤ (setEDist (e SixPointColor.red) (e SixPointColor.blue)).toReal) :
    colorBallUnion support center radius SixPointColor.red ∩ colorBallUnion support center radius SixPointColor.blue ⊆ finiteBallUnion support center radius \ (e SixPointColor.red ∪ e SixPointColor.blue)

    Red-blue ball overlap lies outside both center sets.

    source
    theorem LeanPool.Besicovitch.sum_measure_ball_le_union_add_leakage {support : Finset SixPointIndex} (center : ↥support → EuclideanSpace ℝ (Fin 2)) (radius : ↥support → ℝ) (e : SixPointColor → Set (EuclideanSpace ℝ (Fin 2))) (μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin 2))) (he : ∀ (color : SixPointColor), (e color).Nonempty) (hcenter : ∀ (i : ↥support), center i ∈ e (↑i).1) (hradius : ∀ (i : ↥support), radius i ≤ (setEDist (e SixPointColor.red) (e SixPointColor.blue)).toReal) (hdisjoint : ∀ (i j : ↥support), i ≠ j → (↑i).1 = (↑j).1 → Disjoint (Metric.ball (center i) (radius i)) (Metric.ball (center j) (radius j))) :
    ∑ i : ↥support, μ (Metric.ball (center i) (radius i)) ≤ μ (finiteBallUnion support center radius) + μ (finiteBallUnion support center radius \ (e SixPointColor.red ∪ e SixPointColor.blue))

    The total ball mass is bounded by the union mass plus the mass outside both center sets.

    source
    theorem LeanPool.Besicovitch.density_sum_lt_one_add_leakage_mul_ediam {support : Finset SixPointIndex} (hsupport : support.Nonempty) (center : ↥support → EuclideanSpace ℝ (Fin 2)) (radius : ↥support → ℝ) (e : SixPointColor → Set (EuclideanSpace ℝ (Fin 2))) (μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin 2))) {β scale : ℝ} {leakage : ENNReal} (hβ : 0 ≤ β) (he : ∀ (color : SixPointColor), (e color).Nonempty) (hcenter : ∀ (i : ↥support), center i ∈ e (↑i).1) (hradius_pos : ∀ (i : ↥support), 0 < radius i) (hradius_lt : ∀ (i : ↥support), radius i < scale) (hradius_le : ∀ (i : ↥support), radius i ≤ (setEDist (e SixPointColor.red) (e SixPointColor.blue)).toReal) (hdisjoint : ∀ (i j : ↥support), i ≠ j → (↑i).1 = (↑j).1 → Disjoint (Metric.ball (center i) (radius i)) (Metric.ball (center j) (radius j))) (hdensity : ∀ x ∈ e SixPointColor.red ∪ e SixPointColor.blue, ∀ (r : ℝ), 0 < r → r < scale → ENNReal.ofReal (2 * β * r) < μ (Metric.ball x r)) (hμ : IsStraightMeasure μ) (hleakage : μ (finiteBallUnion support center radius \ (e SixPointColor.red ∪ e SixPointColor.blue)) ≤ leakage * Metric.ediam (finiteBallUnion support center radius)) :
    ENNReal.ofReal (2 * β * ∑ i : ↥support, radius i) < (1 + leakage) * Metric.ediam (finiteBallUnion support center radius)

    Density, straightness, and a leakage bound control the total supported radius.