The Besicovitch pair condition

This file defines straight measures and the pair condition in the Euclidean plane.

noncomputable def LeanPool.Besicovitch.setEDist {X : Type u_1} [PseudoEMetricSpace X] (s t : Set X) : ENNReal

The extended distance between two sets; it is infinite when either set is empty.

Equations

• LeanPool.Besicovitch.setEDist s t = ⨅ x ∈ s, ⨅ y ∈ t, edist x y

def LeanPool.Besicovitch.IsStraightMeasure (μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin 2))) : Prop

A measure is straight if every measurable set has mass at most its extended diameter.

Equations

• LeanPool.Besicovitch.IsStraightMeasure μ = ∀ (s : Set (EuclideanSpace ℝ (Fin 2))), MeasurableSet s → μ s ≤ Metric.ediam s

def LeanPool.Besicovitch.BesicovitchPairCondition (β : ℝ) : Prop

The Besicovitch pair condition at density parameter β.

Equations

• One or more equations did not get rendered due to their size.