Documentation

LeanPool.Besicovitch.SixPoint.GramCertificateData

The thirty local Gram certificates #

The two second-child radii both lie in [barC - 1, 1]. Seven intervals cover that range, the score is symmetric in the two sibling pairs, and the middle square is split once more, leaving thirty ordered rectangles. This file records one certificate for each and checks its arithmetic.

The tangent parameters, separation multipliers and factor entries were found numerically and are stored as exact rationals with denominator 10000; every inequality below is recomputed here.

source
def LeanPool.Besicovitch.gramCertificates :
Fin 30 → GramCertificate

One local Gram certificate for each of the thirty radius rectangles.

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

    Radius rectangles #

    The four box endpoints of each stored certificate, for the cover argument.

    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_pLower_0 :
    (gramCertificates 0).pLower = 967 / 2500
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_pUpper_0 :
    (gramCertificates 0).pUpper = 1 / 2
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_wLower_0 :
    (gramCertificates 0).wLower = 967 / 2500
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_wUpper_0 :
    (gramCertificates 0).wUpper = 1 / 2
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_pLower_1 :
    (gramCertificates 1).pLower = 967 / 2500
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_pUpper_1 :
    (gramCertificates 1).pUpper = 1 / 2
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_wLower_1 :
    (gramCertificates 1).wLower = 1 / 2
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_wUpper_1 :
    (gramCertificates 1).wUpper = 3 / 5
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_pLower_2 :
    (gramCertificates 2).pLower = 967 / 2500
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_pUpper_2 :
    (gramCertificates 2).pUpper = 1 / 2
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_wLower_2 :
    (gramCertificates 2).wLower = 3 / 5
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_wUpper_2 :
    (gramCertificates 2).wUpper = 7 / 10
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_pLower_3 :
    (gramCertificates 3).pLower = 967 / 2500
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_pUpper_3 :
    (gramCertificates 3).pUpper = 1 / 2
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_wLower_3 :
    (gramCertificates 3).wLower = 7 / 10
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_wUpper_3 :
    (gramCertificates 3).wUpper = 3 / 4
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_pLower_4 :
    (gramCertificates 4).pLower = 967 / 2500
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_pUpper_4 :
    (gramCertificates 4).pUpper = 1 / 2
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_wLower_4 :
    (gramCertificates 4).wLower = 3 / 4
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_wUpper_4 :
    (gramCertificates 4).wUpper = 4 / 5
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_pLower_5 :
    (gramCertificates 5).pLower = 967 / 2500
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_pUpper_5 :
    (gramCertificates 5).pUpper = 1 / 2
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_wLower_5 :
    (gramCertificates 5).wLower = 4 / 5
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_wUpper_5 :
    (gramCertificates 5).wUpper = 9 / 10
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_pLower_6 :
    (gramCertificates 6).pLower = 967 / 2500
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_pUpper_6 :
    (gramCertificates 6).pUpper = 1 / 2
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_wLower_6 :
    (gramCertificates 6).wLower = 9 / 10
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_wUpper_6 :
    (gramCertificates 6).wUpper = 1
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_pLower_7 :
    (gramCertificates 7).pLower = 1 / 2
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_pUpper_7 :
    (gramCertificates 7).pUpper = 3 / 5
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_wLower_7 :
    (gramCertificates 7).wLower = 1 / 2
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_wUpper_7 :
    (gramCertificates 7).wUpper = 3 / 5
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_pLower_8 :
    (gramCertificates 8).pLower = 1 / 2
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_pUpper_8 :
    (gramCertificates 8).pUpper = 3 / 5
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_wLower_8 :
    (gramCertificates 8).wLower = 3 / 5
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_wUpper_8 :
    (gramCertificates 8).wUpper = 7 / 10
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_pLower_9 :
    (gramCertificates 9).pLower = 1 / 2
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_pUpper_9 :
    (gramCertificates 9).pUpper = 3 / 5
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_wLower_9 :
    (gramCertificates 9).wLower = 7 / 10
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_wUpper_9 :
    (gramCertificates 9).wUpper = 3 / 4
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_pLower_10 :
    (gramCertificates 10).pLower = 1 / 2
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_pUpper_10 :
    (gramCertificates 10).pUpper = 3 / 5
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_wLower_10 :
    (gramCertificates 10).wLower = 3 / 4
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_wUpper_10 :
    (gramCertificates 10).wUpper = 4 / 5
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_pLower_11 :
    (gramCertificates 11).pLower = 1 / 2
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_pUpper_11 :
    (gramCertificates 11).pUpper = 3 / 5
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_wLower_11 :
    (gramCertificates 11).wLower = 4 / 5
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_wUpper_11 :
    (gramCertificates 11).wUpper = 9 / 10
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_pLower_12 :
    (gramCertificates 12).pLower = 1 / 2
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_pUpper_12 :
    (gramCertificates 12).pUpper = 3 / 5
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_wLower_12 :
    (gramCertificates 12).wLower = 9 / 10
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_wUpper_12 :
    (gramCertificates 12).wUpper = 1
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_pLower_13 :
    (gramCertificates 13).pLower = 3 / 5
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_pUpper_13 :
    (gramCertificates 13).pUpper = 7 / 10
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_wLower_13 :
    (gramCertificates 13).wLower = 7 / 10
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_wUpper_13 :
    (gramCertificates 13).wUpper = 3 / 4
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_pLower_14 :
    (gramCertificates 14).pLower = 3 / 5
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_pUpper_14 :
    (gramCertificates 14).pUpper = 7 / 10
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_wLower_14 :
    (gramCertificates 14).wLower = 3 / 4
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_wUpper_14 :
    (gramCertificates 14).wUpper = 4 / 5
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_pLower_15 :
    (gramCertificates 15).pLower = 3 / 5
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_pUpper_15 :
    (gramCertificates 15).pUpper = 7 / 10
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_wLower_15 :
    (gramCertificates 15).wLower = 4 / 5
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_wUpper_15 :
    (gramCertificates 15).wUpper = 9 / 10
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_pLower_16 :
    (gramCertificates 16).pLower = 3 / 5
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_pUpper_16 :
    (gramCertificates 16).pUpper = 7 / 10
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_wLower_16 :
    (gramCertificates 16).wLower = 9 / 10
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_wUpper_16 :
    (gramCertificates 16).wUpper = 1
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_pLower_17 :
    (gramCertificates 17).pLower = 7 / 10
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_pUpper_17 :
    (gramCertificates 17).pUpper = 3 / 4
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_wLower_17 :
    (gramCertificates 17).wLower = 7 / 10
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_wUpper_17 :
    (gramCertificates 17).wUpper = 3 / 4
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_pLower_18 :
    (gramCertificates 18).pLower = 7 / 10
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_pUpper_18 :
    (gramCertificates 18).pUpper = 3 / 4
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_wLower_18 :
    (gramCertificates 18).wLower = 3 / 4
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_wUpper_18 :
    (gramCertificates 18).wUpper = 4 / 5
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_pLower_19 :
    (gramCertificates 19).pLower = 7 / 10
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_pUpper_19 :
    (gramCertificates 19).pUpper = 3 / 4
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_wLower_19 :
    (gramCertificates 19).wLower = 4 / 5
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_wUpper_19 :
    (gramCertificates 19).wUpper = 9 / 10
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_pLower_20 :
    (gramCertificates 20).pLower = 7 / 10
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_pUpper_20 :
    (gramCertificates 20).pUpper = 3 / 4
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_wLower_20 :
    (gramCertificates 20).wLower = 9 / 10
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_wUpper_20 :
    (gramCertificates 20).wUpper = 1
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_pLower_21 :
    (gramCertificates 21).pLower = 3 / 4
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_pUpper_21 :
    (gramCertificates 21).pUpper = 4 / 5
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_wLower_21 :
    (gramCertificates 21).wLower = 3 / 4
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_wUpper_21 :
    (gramCertificates 21).wUpper = 4 / 5
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_pLower_22 :
    (gramCertificates 22).pLower = 3 / 4
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_pUpper_22 :
    (gramCertificates 22).pUpper = 4 / 5
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_wLower_22 :
    (gramCertificates 22).wLower = 4 / 5
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_wUpper_22 :
    (gramCertificates 22).wUpper = 9 / 10
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_pLower_23 :
    (gramCertificates 23).pLower = 3 / 4
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_pUpper_23 :
    (gramCertificates 23).pUpper = 4 / 5
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_wLower_23 :
    (gramCertificates 23).wLower = 9 / 10
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_wUpper_23 :
    (gramCertificates 23).wUpper = 1
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_pLower_24 :
    (gramCertificates 24).pLower = 4 / 5
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_pUpper_24 :
    (gramCertificates 24).pUpper = 9 / 10
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_wLower_24 :
    (gramCertificates 24).wLower = 4 / 5
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_wUpper_24 :
    (gramCertificates 24).wUpper = 9 / 10
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_pLower_25 :
    (gramCertificates 25).pLower = 4 / 5
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_pUpper_25 :
    (gramCertificates 25).pUpper = 9 / 10
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_wLower_25 :
    (gramCertificates 25).wLower = 9 / 10
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_wUpper_25 :
    (gramCertificates 25).wUpper = 1
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_pLower_26 :
    (gramCertificates 26).pLower = 9 / 10
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_pUpper_26 :
    (gramCertificates 26).pUpper = 1
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_wLower_26 :
    (gramCertificates 26).wLower = 9 / 10
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_wUpper_26 :
    (gramCertificates 26).wUpper = 1
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_pLower_27 :
    (gramCertificates 27).pLower = 3 / 5
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_pUpper_27 :
    (gramCertificates 27).pUpper = 13 / 20
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_wLower_27 :
    (gramCertificates 27).wLower = 3 / 5
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_wUpper_27 :
    (gramCertificates 27).wUpper = 13 / 20
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_pLower_28 :
    (gramCertificates 28).pLower = 3 / 5
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_pUpper_28 :
    (gramCertificates 28).pUpper = 13 / 20
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_wLower_28 :
    (gramCertificates 28).wLower = 13 / 20
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_wUpper_28 :
    (gramCertificates 28).wUpper = 7 / 10
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_pLower_29 :
    (gramCertificates 29).pLower = 13 / 20
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_pUpper_29 :
    (gramCertificates 29).pUpper = 7 / 10
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_wLower_29 :
    (gramCertificates 29).wLower = 13 / 20
    source
    @[simp]
    theorem LeanPool.Besicovitch.gramCertificates_wUpper_29 :
    (gramCertificates 29).wUpper = 7 / 10
    source
    theorem LeanPool.Besicovitch.gramCertificates_valid_0 :
    (gramCertificates 0).Valid

    Arithmetic validation for certificate 0.

    source
    theorem LeanPool.Besicovitch.gramCertificates_valid_1 :
    (gramCertificates 1).Valid

    Arithmetic validation for certificate 1.

    source
    theorem LeanPool.Besicovitch.gramCertificates_valid_2 :
    (gramCertificates 2).Valid

    Arithmetic validation for certificate 2.

    source
    theorem LeanPool.Besicovitch.gramCertificates_valid_3 :
    (gramCertificates 3).Valid

    Arithmetic validation for certificate 3.

    source
    theorem LeanPool.Besicovitch.gramCertificates_valid_4 :
    (gramCertificates 4).Valid

    Arithmetic validation for certificate 4.

    source
    theorem LeanPool.Besicovitch.gramCertificates_valid_5 :
    (gramCertificates 5).Valid

    Arithmetic validation for certificate 5.

    source
    theorem LeanPool.Besicovitch.gramCertificates_valid_6 :
    (gramCertificates 6).Valid

    Arithmetic validation for certificate 6.

    source
    theorem LeanPool.Besicovitch.gramCertificates_valid_7 :
    (gramCertificates 7).Valid

    Arithmetic validation for certificate 7.

    source
    theorem LeanPool.Besicovitch.gramCertificates_valid_8 :
    (gramCertificates 8).Valid

    Arithmetic validation for certificate 8.

    source
    theorem LeanPool.Besicovitch.gramCertificates_valid_9 :
    (gramCertificates 9).Valid

    Arithmetic validation for certificate 9.

    source
    theorem LeanPool.Besicovitch.gramCertificates_valid_10 :
    (gramCertificates 10).Valid

    Arithmetic validation for certificate 10.

    source
    theorem LeanPool.Besicovitch.gramCertificates_valid_11 :
    (gramCertificates 11).Valid

    Arithmetic validation for certificate 11.

    source
    theorem LeanPool.Besicovitch.gramCertificates_valid_12 :
    (gramCertificates 12).Valid

    Arithmetic validation for certificate 12.

    source
    theorem LeanPool.Besicovitch.gramCertificates_valid_13 :
    (gramCertificates 13).Valid

    Arithmetic validation for certificate 13.

    source
    theorem LeanPool.Besicovitch.gramCertificates_valid_14 :
    (gramCertificates 14).Valid

    Arithmetic validation for certificate 14.

    source
    theorem LeanPool.Besicovitch.gramCertificates_valid_15 :
    (gramCertificates 15).Valid

    Arithmetic validation for certificate 15.

    source
    theorem LeanPool.Besicovitch.gramCertificates_valid_16 :
    (gramCertificates 16).Valid

    Arithmetic validation for certificate 16.

    source
    theorem LeanPool.Besicovitch.gramCertificates_valid_17 :
    (gramCertificates 17).Valid

    Arithmetic validation for certificate 17.

    source
    theorem LeanPool.Besicovitch.gramCertificates_valid_18 :
    (gramCertificates 18).Valid

    Arithmetic validation for certificate 18.

    source
    theorem LeanPool.Besicovitch.gramCertificates_valid_19 :
    (gramCertificates 19).Valid

    Arithmetic validation for certificate 19.

    source
    theorem LeanPool.Besicovitch.gramCertificates_valid_20 :
    (gramCertificates 20).Valid

    Arithmetic validation for certificate 20.

    source
    theorem LeanPool.Besicovitch.gramCertificates_valid_21 :
    (gramCertificates 21).Valid

    Arithmetic validation for certificate 21.

    source
    theorem LeanPool.Besicovitch.gramCertificates_valid_22 :
    (gramCertificates 22).Valid

    Arithmetic validation for certificate 22.

    source
    theorem LeanPool.Besicovitch.gramCertificates_valid_23 :
    (gramCertificates 23).Valid

    Arithmetic validation for certificate 23.

    source
    theorem LeanPool.Besicovitch.gramCertificates_valid_24 :
    (gramCertificates 24).Valid

    Arithmetic validation for certificate 24.

    source
    theorem LeanPool.Besicovitch.gramCertificates_valid_25 :
    (gramCertificates 25).Valid

    Arithmetic validation for certificate 25.

    source
    theorem LeanPool.Besicovitch.gramCertificates_valid_26 :
    (gramCertificates 26).Valid

    Arithmetic validation for certificate 26.

    source
    theorem LeanPool.Besicovitch.gramCertificates_valid_27 :
    (gramCertificates 27).Valid

    Arithmetic validation for certificate 27.

    source
    theorem LeanPool.Besicovitch.gramCertificates_valid_28 :
    (gramCertificates 28).Valid

    Arithmetic validation for certificate 28.

    source
    theorem LeanPool.Besicovitch.gramCertificates_valid_29 :
    (gramCertificates 29).Valid

    Arithmetic validation for certificate 29.

    source
    theorem LeanPool.Besicovitch.gramCertificates_valid (i : Fin 30) :
    (gramCertificates i).Valid

    Every stored certificate satisfies its arithmetic side conditions.