The coordinate-free weighted bound at the small rational weights

Combining the local Gram certificates with the finite cover of second-child radii gives the weighted geometric bound for every pair of separated sibling pairs in the unit ball.

theorem LeanPool.Besicovitch.weightedPairScore_le_of_separated {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (e p₁ p₂ w₁ w₂ : E) (he : ‖e‖ = 1) (hp₁ : ‖p₁‖ ≤ 1) (hp₂ : ‖p₂‖ ≤ 1) (hw₁ : ‖w₁‖ ≤ 1) (hw₂ : ‖w₂‖ ≤ 1) (hpsep : barC ≤ ‖p₁ - p₂‖) (hwsep : barC ≤ ‖w₁ - w₂‖) : weightedPairScore e barC gramLambda gramMu p₁ p₂ w₁ w₂ ≤ -(1 / 2000)

Every separated pair of sibling pairs in the unit ball has strictly negative weighted score.

theorem LeanPool.Besicovitch.weightedGeometricBound_gram : WeightedGeometricBound gramLambda gramMu

The Gram certificates prove the weighted geometric bound at the small rational weights.