Diameter of the local attachment component #
The BPC witness prevents the component through the selected density point from remaining inside the small inner ball. Any hypothetical clopen separation would be crossed by one convex attachment.
def
LeanPool.Besicovitch.localAttachmentComponent
(F : Set (EuclideanSpace ℝ (Fin 2)))
(chosen : Set (Set (EuclideanSpace ℝ (Fin 2))))
(z : EuclideanSpace ℝ (Fin 2))
(rho : ℝ)
:
Set (EuclideanSpace ℝ (Fin 2))
The connected component through z in the attachment union localized to a closed ball.
Equations
- LeanPool.Besicovitch.localAttachmentComponent F chosen z rho = connectedComponentIn (LeanPool.Besicovitch.compactAttachmentUnion F chosen ∩ Metric.closedBall z rho) z
Instances For
theorem
LeanPool.Besicovitch.sigma_mul_radius_div_two_le_diam_localAttachmentComponent
{mu : MeasureTheory.Measure (EuclideanSpace ℝ (Fin 2))}
{F : Set (EuclideanSpace ℝ (Fin 2))}
(hF : IsCompact F)
{alpha tau sigma gamma : ℝ}
(halpha : 0 < alpha)
(halpha_tau : alpha ≤ tau)
(hsigma : 0 ≤ sigma)
(hsigma_one : sigma < 1)
(hsigma_gamma : sigma < gamma)
{m : ℕ}
(huniform : F ⊆ uniformDensitySet mu F gamma m)
{chosen : Set (Set (EuclideanSpace ℝ (Fin 2)))}
(hchosen : chosen ⊆ badConvexSets mu F alpha)
(hselect : ∀ V ∈ badConvexSets mu F alpha, ∃ W ∈ chosen, (V ∩ W).Nonempty ∧ Metric.diam V < 2 * Metric.diam W)
(hsum : ∑' (V : ↑chosen), Metric.ediam ↑V ≠ ⊤)
{z : EuclideanSpace ℝ (Fin 2)}
(hzF : z ∈ F)
{rho delta : ℝ}
(hrho : 0 < rho)
(hrho_delta : rho < delta)
(hannulus : (Metric.ball z rho \ Metric.ball z (sigma * rho / 2) ∩ F).Nonempty)
(hpair :
∀ (e₁ e₂ : Set (EuclideanSpace ℝ (Fin 2))),
MeasurableSet e₁ →
MeasurableSet e₂ →
e₁.Nonempty →
e₂.Nonempty →
0 < setEDist e₁ e₂ →
setEDist e₁ e₂ < ENNReal.ofReal delta →
(∀ x ∈ e₁ ∪ e₂,
∀ (r : ℝ), 0 < r → r < 1 / (↑m + 1) → ENNReal.ofReal (2 * sigma * r) < mu (Metric.ball x r)) →
∃ (v : Set (EuclideanSpace ℝ (Fin 2))),
IsOpen v ∧ (v ∩ e₁).Nonempty ∧ (v ∩ e₂).Nonempty ∧ ENNReal.ofReal tau * Metric.ediam v < mu (v \ (e₁ ∪ e₂)))
:
A BPC separation forces the local attachment component to have diameter at least
sigma * rho / 2.