Documentation

LeanPool.Besicovitch.SixPoint.GramCertificateCover

The finite cover of second-child radii #

Both second-child radii lie in [barC - 1, 1]. Eight bands cover that interval, and every ordered pair of bands is contained in the radius rectangle of one stored certificate, after swapping the two sibling pairs when the blue band precedes the red one.

source
def LeanPool.Besicovitch.bandLower :
Fin 8 → ℚ

Lower endpoints of the eight radius bands.

Equations
Instances For
    source
    def LeanPool.Besicovitch.bandUpper :
    Fin 8 → ℚ

    Upper endpoints of the eight radius bands.

    Equations
    Instances For
      source
      def LeanPool.Besicovitch.bandCertificate :
      Fin 8 → Fin 8 → Fin 30

      The certificate covering a given ordered pair of bands.

      Equations
      Instances For
        source
        def LeanPool.Besicovitch.bandSwapped :
        Fin 8 → Fin 8 → Bool

        Whether the covering certificate needs the two sibling pairs swapped.

        Equations
        Instances For
          source
          theorem LeanPool.Besicovitch.exists_band (x : ℝ) (h0 : barC - 1 ≤ x) (h1 : x ≤ 1) :
          ∃ (k : Fin 8), ↑(bandLower k) ≤ x ∧ x ≤ ↑(bandUpper k)

          Every radius in range lies in one of the eight bands.

          source
          theorem LeanPool.Besicovitch.bandCertificate_contains (k l : Fin 8) :
          if bandSwapped k l = true then (gramCertificates (bandCertificate k l)).pLower ≤ bandLower l ∧ bandUpper l ≤ (gramCertificates (bandCertificate k l)).pUpper ∧ (gramCertificates (bandCertificate k l)).wLower ≤ bandLower k ∧ bandUpper k ≤ (gramCertificates (bandCertificate k l)).wUpper else (gramCertificates (bandCertificate k l)).pLower ≤ bandLower k ∧ bandUpper k ≤ (gramCertificates (bandCertificate k l)).pUpper ∧ (gramCertificates (bandCertificate k l)).wLower ≤ bandLower l ∧ bandUpper l ≤ (gramCertificates (bandCertificate k l)).wUpper

          The band pair is contained in the radius rectangle of its covering certificate.