Documentation

LeanPool.Besicovitch.SixPoint.FiniteProperty

The finite six-point property #

This file states the compactified finite property and removes zero-radius labels from strict witnesses.

source
def LeanPool.Besicovitch.SixPointFiniteProperty (s : ℝ) :
Prop

Every admissible configuration at s has a compactified packing of nonnegative score.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def LeanPool.Besicovitch.SixPointPacking.HasPositiveRadii {configuration : SixPointConfiguration} (packing : SixPointPacking configuration) :
    Prop

    A packing is genuine when every radius on its support is positive.

    Equations
    Instances For
      source
      noncomputable def LeanPool.Besicovitch.SixPointPacking.positiveSupport {configuration : SixPointConfiguration} (packing : SixPointPacking configuration) :
      Finset SixPointIndex

      The labels carrying positive radius in a compactified packing.

      Equations
      Instances For
        source
        theorem LeanPool.Besicovitch.SixPointPacking.mem_positiveSupport_iff {configuration : SixPointConfiguration} (packing : SixPointPacking configuration) {index : SixPointIndex} :
        index ∈ packing.positiveSupport ↔ ∃ (hindex : index ∈ packing.support), 0 < ↑(packing.radius ⟨index, hindex⟩)

        Membership in the positive support is exactly positivity of the corresponding radius.

        source
        theorem LeanPool.Besicovitch.SixPointPacking.positiveSupport_subset {configuration : SixPointConfiguration} (packing : SixPointPacking configuration) :
        packing.positiveSupport ⊆ packing.support

        The positive support is contained in the compactified support.

        source
        theorem LeanPool.Besicovitch.SixPointPacking.exists_positiveRadii_score_gt {configuration : SixPointConfiguration} (packing : SixPointPacking configuration) {beta cap a : ℝ} (hbeta : 0 < beta) (hcap_pos : 0 < cap) (hcap_one : cap ≤ 1) (hcap : ∀ (i : ↥packing.support), ↑(packing.radius i) ≤ cap) (hscore : a < packing.score beta) :
        ∃ (packing' : SixPointPacking configuration), packing'.HasPositiveRadii ∧ (∀ (i : ↥packing'.support), ↑(packing'.radius i) ≤ cap) ∧ a < packing'.score beta

        A strict compactified score has a genuine witness below the same positive radius cap.