Extracting separated children from density

This file isolates the measure estimate that turns a dense root ball into two well-separated points of the same set. The missing mass is charged to one common leakage set.

theorem LeanPool.Besicovitch.measure_inter_gt_of_ball_gt_of_leakage {X : Type u_1} [MeasurableSpace X] (μ : MeasureTheory.Measure X) {e other ball ambient : Set X} {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hball : ball ⊆ ambient) (hdisjoint : Disjoint ball other) (hdensity : ENNReal.ofReal (a + b) < μ ball) (hleakage : μ (ambient \ (e ∪ other)) ≤ ENNReal.ofReal b) : ENNReal.ofReal a < μ (e ∩ ball)

After paying for a leakage set, the part of a ball in its own color retains the remaining mass.

theorem LeanPool.Besicovitch.IsStraightMeasure.exists_children {μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin 2))} (hμ : IsStraightMeasure μ) {e : Set (EuclideanSpace ℝ (Fin 2))} (he : MeasurableSet e) {root : EuclideanSpace ℝ (Fin 2)} {d γ : ℝ} (hmass : ENNReal.ofReal (2 * γ * d) < μ (e ∩ Metric.ball root d)) : ∃ left ∈ e ∩ Metric.ball root d, ∃ right ∈ e ∩ Metric.ball root d, 2 * γ * d < dist left right

Straightness converts enough mass in one color of a root ball into two separated children.