The endpoint packing theorem

This file assembles the finite failure tree. Its sole analytic input is the weighted geometric bound for two ordered chords in the unit disk.

def LeanPool.Besicovitch.WeightedGeometricBound (lambda mu : ℝ) : Prop

The weighted geometric inequality for two ordered sibling pairs in the unit disk.

Equations

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

theorem LeanPool.Besicovitch.sixPointFiniteProperty_barS_of_weightedGeometricBound {lambda mu : ℝ} (hlambda : 0 < lambda) (hmu : 0 < mu) (hweighted : WeightedGeometricBound lambda mu) : SixPointFiniteProperty barS

The weighted geometric bound implies the finite six-point property at the exact endpoint.