Basic facts about the Besicovitch pair condition

This file develops the elementary set-distance API needed by the six-point transfer.

theorem LeanPool.Besicovitch.setEDist_le_edist_of_mem {X : Type u_1} [PseudoEMetricSpace X] {s t : Set X} {x y : X} (hx : x ∈ s) (hy : y ∈ t) : setEDist s t ≤ edist x y

The set distance is bounded by the distance between any selected pair of points.

theorem LeanPool.Besicovitch.setEDist_comm {X : Type u_1} [PseudoEMetricSpace X] (s t : Set X) : setEDist s t = setEDist t s

Extended set distance is symmetric.

@[simp]

theorem LeanPool.Besicovitch.setEDist_empty_left {X : Type u_1} [PseudoEMetricSpace X] (t : Set X) : setEDist ∅ t = ⊤

theorem LeanPool.Besicovitch.setEDist_ne_top {Y : Type u_2} [PseudoMetricSpace Y] {u v : Set Y} (hu : u.Nonempty) (hv : v.Nonempty) : setEDist u v ≠ ⊤

Two nonempty sets in a metric space have finite extended distance.

theorem LeanPool.Besicovitch.setEDist_toReal_pos {Y : Type u_2} [PseudoMetricSpace Y] {u v : Set Y} (hu : u.Nonempty) (hv : v.Nonempty) (hpos : 0 < setEDist u v) : 0 < (setEDist u v).toReal

A positive finite set distance has a positive real value.

theorem LeanPool.Besicovitch.setEDist_toReal_le_dist {Y : Type u_2} [PseudoMetricSpace Y] {u v : Set Y} (hu : u.Nonempty) (hv : v.Nonempty) {x y : Y} (hx : x ∈ u) (hy : y ∈ v) : (setEDist u v).toReal ≤ dist x y

The real set distance is no larger than any distance between the two sets.

theorem LeanPool.Besicovitch.ball_disjoint_of_le_setEDist_toReal {Y : Type u_2} [PseudoMetricSpace Y] {u v : Set Y} (hu : u.Nonempty) (hv : v.Nonempty) {x : Y} (hx : x ∈ u) {r : ℝ} (hr : r ≤ (setEDist u v).toReal) : Disjoint (Metric.ball x r) v

A ball whose radius is at most the set distance misses the opposite set.

theorem LeanPool.Besicovitch.exists_edist_lt_of_setEDist_lt {X : Type u_1} [PseudoEMetricSpace X] {s t : Set X} {r : ENNReal} (h : setEDist s t < r) : ∃ x ∈ s, ∃ y ∈ t, edist x y < r

A strict upper bound on set distance is witnessed by an actual pair of points.

theorem LeanPool.Besicovitch.exists_dist_lt_of_setEDist_toReal_lt {Y : Type u_2} [PseudoMetricSpace Y] {u v : Set Y} (hu : u.Nonempty) (hv : v.Nonempty) {r : ℝ} (h : (setEDist u v).toReal < r) : ∃ x ∈ u, ∃ y ∈ v, dist x y < r

A real number above the finite set distance bounds some actual pair distance.

theorem LeanPool.Besicovitch.BesicovitchPairCondition.mono {β γ : ℝ} (hβγ : β ≤ γ) (hβ : BesicovitchPairCondition β) : BesicovitchPairCondition γ

Raising the density parameter preserves the Besicovitch pair condition.

theorem LeanPool.Besicovitch.IsStraightMeasure.exists_dist_gt {μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin 2))} (hμ : IsStraightMeasure μ) {s : Set (EuclideanSpace ℝ (Fin 2))} (hs : MeasurableSet s) {a : ℝ} (ha : ENNReal.ofReal a < μ s) : ∃ x ∈ s, ∃ y ∈ s, a < dist x y

A straight set whose mass exceeds a contains two points more than a apart.