`OAI/Analysis/PlanarPacking/Certificate/`

547707 declarations, 0 contain sorry, 0 declared as axioms; 446 files

Files

Amplitudes.lean 2496 declarations
AtomKernels.lean 328 declarations
Bernstein0.lean 119 declarations
Bernstein1.lean 357 declarations
Bernstein12.lean 408 declarations
Bernstein13.lean 404 declarations
Bernstein15.lean 404 declarations
Bernstein16.lean 408 declarations
Bernstein19.lean 408 declarations
Bernstein21.lean 424 declarations
Bernstein24.lean 424 declarations
Bernstein25.lean 428 declarations
Bernstein27.lean 428 declarations
Bernstein28.lean 440 declarations
Bernstein3.lean 408 declarations
Bernstein31.lean 456 declarations
Bernstein33.lean 456 declarations
Bernstein36.lean 472 declarations
Bernstein37.lean 460 declarations
Bernstein39.lean 460 declarations
Bernstein4.lean 432 declarations
Bernstein40.lean 488 declarations
Bernstein7.lean 416 declarations
Bernstein9.lean 416 declarations
CoarseBound12.lean 17 declarations
CoarseBound13.lean 18 declarations
CoarseBound15.lean 18 declarations
CoarseBound16.lean 17 declarations
CoarseBound19.lean 17 declarations
CoarseBound21.lean 17 declarations
CoarseBound24.lean 17 declarations
CoarseBound25.lean 18 declarations
CoarseBound27.lean 18 declarations
CoarseBound28.lean 17 declarations
CoarseBound3.lean 17 declarations
CoarseBound31.lean 17 declarations
CoarseBound33.lean 17 declarations
CoarseBound36.lean 17 declarations
CoarseBound37.lean 18 declarations
CoarseBound39.lean 18 declarations
CoarseBound4.lean 11 declarations
CoarseBound40.lean 17 declarations
CoarseBound7.lean 15 declarations
CoarseBound9.lean 15 declarations
Columns10.lean 2496 declarations
Columns100.lean 2496 declarations
Columns20.lean 2080 declarations
Columns30.lean 2080 declarations
Columns40.lean 2496 declarations
Columns50.lean 1664 declarations
Columns60.lean 2080 declarations
Columns70.lean 2080 declarations
Columns80.lean 2080 declarations
Columns90.lean 2080 declarations
DEntries.lean 75 declarations
DMoments1.lean 2520 declarations
DMoments3.lean 2520 declarations
DMoments4.lean 2520 declarations
HighHeaders0.lean 310 declarations
HighHeaders1.lean 310 declarations
HighHeaders12.lean 310 declarations
HighHeaders13.lean 310 declarations
HighHeaders15.lean 310 declarations
HighHeaders16.lean 310 declarations
HighHeaders19.lean 310 declarations
HighHeaders21.lean 310 declarations
HighHeaders24.lean 310 declarations
HighHeaders25.lean 310 declarations
HighHeaders27.lean 310 declarations
HighHeaders28.lean 310 declarations
HighHeaders3.lean 310 declarations
HighHeaders31.lean 310 declarations
HighHeaders33.lean 310 declarations
HighHeaders36.lean 310 declarations
HighHeaders37.lean 310 declarations
HighHeaders39.lean 310 declarations
HighHeaders4.lean 310 declarations
HighHeaders40.lean 310 declarations
HighHeaders7.lean 310 declarations
HighHeaders9.lean 310 declarations
HighMoments0_0.lean 3456 declarations
HighMoments0_1.lean 3456 declarations
HighMoments0_2.lean 3456 declarations
HighMoments0_3.lean 3024 declarations
HighMoments0_4.lean 3456 declarations
HighMoments0_5.lean 3456 declarations
HighMoments0_6.lean 3456 declarations
HighMoments0_7.lean 3024 declarations
HighMoments1_0.lean 3456 declarations
HighMoments1_1.lean 3456 declarations
HighMoments1_2.lean 3456 declarations
HighMoments1_3.lean 3024 declarations
HighMoments1_4.lean 3456 declarations
HighMoments1_5.lean 3456 declarations
HighMoments1_6.lean 3456 declarations
HighMoments1_7.lean 3024 declarations
HighMoments3_0.lean 3456 declarations
KernelValues10.lean 2496 declarations
KernelValues100.lean 2496 declarations
KernelValues20.lean 2080 declarations
KernelValues30.lean 2080 declarations
KernelValues40.lean 2496 declarations
KernelValues50.lean 1664 declarations
KernelValues60.lean 2080 declarations
KernelValues70.lean 2080 declarations
KernelValues80.lean 2080 declarations
KernelValues90.lean 2080 declarations
LEntries.lean 148 declarations
LMoments12.lean 2520 declarations
LMoments13.lean 2520 declarations
LMoments15.lean 2520 declarations
LMoments16.lean 2520 declarations
LMoments7.lean 2520 declarations
LMoments9.lean 2520 declarations
LowBlock12_0.lean 2592 declarations
LowBlock12_1.lean 2592 declarations
LowBlock12_10.lean 2592 declarations
LowBlock12_11.lean 2592 declarations
LowBlock13_0.lean 2592 declarations
LowBlock13_1.lean 2160 declarations
LowBlock13_10.lean 2592 declarations
LowBlock13_11.lean 2160 declarations
LowBlock15_0.lean 2592 declarations
LowBlock15_1.lean 2160 declarations
LowBlock15_10.lean 2592 declarations
LowBlock15_11.lean 2160 declarations
LowBlock16_0.lean 2592 declarations
LowBlock16_1.lean 2592 declarations
LowBlock16_10.lean 2592 declarations
LowBlock16_11.lean 2592 declarations
LowBlock19_0.lean 2592 declarations
LowBlock19_1.lean 2592 declarations
LowBlock19_10.lean 2592 declarations
LowBlock19_11.lean 2592 declarations
LowBlock21_0.lean 2592 declarations
LowBlock21_1.lean 2592 declarations
LowBlock21_10.lean 2592 declarations
LowBlock21_11.lean 1728 declarations
LowBlock24_0.lean 2592 declarations
LowBlock24_1.lean 2592 declarations
LowBlock24_10.lean 2592 declarations
LowBlock24_11.lean 1728 declarations
LowBlock25_0.lean 2592 declarations
LowBlock25_1.lean 2160 declarations
LowBlock25_10.lean 2592 declarations
LowBlock25_11.lean 864 declarations
LowBlock27_0.lean 2592 declarations
LowBlock27_1.lean 2160 declarations
LowBlock27_10.lean 2592 declarations
LowBlock27_11.lean 864 declarations
LowBlock28_0.lean 2592 declarations
LowBlock28_1.lean 2592 declarations
LowBlock28_10.lean 2592 declarations
LowBlock28_11.lean 864 declarations
LowBlock31_0.lean 2592 declarations
LowBlock31_1.lean 2592 declarations
LowBlock31_10.lean 2592 declarations
LowBlock33_0.lean 2592 declarations
LowBlock33_1.lean 2592 declarations
LowBlock33_10.lean 2592 declarations
LowBlock36_0.lean 2592 declarations
LowBlock36_1.lean 2592 declarations
LowBlock36_10.lean 1728 declarations
LowBlock37_0.lean 2592 declarations
LowBlock37_1.lean 2160 declarations
LowBlock37_10.lean 1728 declarations
LowBlock39_0.lean 2592 declarations
LowBlock39_1.lean 2160 declarations
LowBlock39_10.lean 1728 declarations
LowBlock3_1.lean 2592 declarations
LowBlock3_10.lean 2592 declarations
LowBlock3_11.lean 2592 declarations
LowBlock40_0.lean 2592 declarations
LowBlock40_1.lean 2592 declarations
LowBlock40_10.lean 864 declarations
LowBlock4_0.lean 2592 declarations
LowBlock4_1.lean 2592 declarations
LowBlock4_10.lean 2592 declarations
LowBlock4_11.lean 2592 declarations
LowBlock4_12.lean 2592 declarations
LowBlock4_2.lean 2592 declarations
LowBlock7_0.lean 2592 declarations
LowBlock7_1.lean 2592 declarations
LowBlock7_10.lean 2592 declarations
LowBlock7_11.lean 2592 declarations
LowBlock7_12.lean 864 declarations
LowBlock7_2.lean 864 declarations
LowBlock9_0.lean 2592 declarations
LowBlock9_1.lean 2592 declarations
LowBlock9_10.lean 2592 declarations
LowBlock9_11.lean 2592 declarations
LowBlock9_12.lean 864 declarations
LowBlock9_2.lean 864 declarations
MixedBound21.lean 2 declarations
MixedBound24.lean 2 declarations
MixedBound25.lean 3 declarations
MixedBound27.lean 3 declarations
MixedBound28.lean 4 declarations
MixedBound31.lean 6 declarations
MixedBound33.lean 6 declarations
MixedBound36.lean 8 declarations
MixedBound37.lean 7 declarations
MixedBound39.lean 7 declarations
MixedBound40.lean 10 declarations
MomentPowers10.lean 2080 declarations
MomentPowers15.lean 2080 declarations
MomentPowers20.lean 2080 declarations
MomentPowers25.lean 2080 declarations
MomentPowers30.lean 2080 declarations
MomentPowers5.lean 2084 declarations
Powers10.lean 2082 declarations
Powers100.lean 2080 declarations
Powers20.lean 2080 declarations
Powers30.lean 2080 declarations
Powers40.lean 2080 declarations
Powers50.lean 2080 declarations
Powers60.lean 2080 declarations
Powers70.lean 2080 declarations
Powers80.lean 2080 declarations
Powers90.lean 2080 declarations
Residual1.lean 13 declarations
Residual100.lean 13 declarations
Residual12.lean 13 declarations
Residual13.lean 13 declarations
Residual15.lean 13 declarations
Residual16.lean 13 declarations
Residual19.lean 13 declarations
Residual21.lean 13 declarations
Residual24.lean 13 declarations
Residual25.lean 13 declarations
Residual27.lean 13 declarations
Residual28.lean 13 declarations
Residual3.lean 13 declarations
Residual31.lean 13 declarations
Residual33.lean 13 declarations
Residual36.lean 13 declarations
Residual37.lean 13 declarations
Residual39.lean 13 declarations
Residual4.lean 13 declarations
Residual40.lean 13 declarations
Residual43.lean 13 declarations
Residual45.lean 13 declarations
Residual48.lean 13 declarations
Residual49.lean 13 declarations
Residual51.lean 13 declarations
Residual52.lean 13 declarations
Residual55.lean 13 declarations
Residual57.lean 13 declarations
Residual60.lean 13 declarations
Residual61.lean 13 declarations
Residual63.lean 13 declarations
Residual64.lean 13 declarations
Residual67.lean 13 declarations
Residual69.lean 13 declarations
Residual7.lean 13 declarations
Residual72.lean 13 declarations
Residual73.lean 13 declarations
Residual75.lean 13 declarations
Residual76.lean 13 declarations
Residual79.lean 13 declarations
Residual81.lean 13 declarations
Residual84.lean 13 declarations
Residual85.lean 13 declarations
Residual87.lean 13 declarations
Residual88.lean 13 declarations
Residual9.lean 13 declarations
Residual91.lean 13 declarations
Residual93.lean 13 declarations
Residual96.lean 13 declarations
Residual97.lean 13 declarations
Residual99.lean 13 declarations
TableData.lean 17 declarations
TableDensity0Panel0.lean 34 declarations
TableDensity0Panel1.lean 34 declarations
TableDensity0Panel2.lean 34 declarations
TableDensity0Panel3.lean 34 declarations
TableDensity0Panel4.lean 34 declarations
TableDensity0Panel5.lean 34 declarations
TableDensity1Panel0.lean 34 declarations
TableDensity1Panel1.lean 34 declarations
TableDensity1Panel2.lean 34 declarations
TableDensity1Panel3.lean 34 declarations
TableDensity1Panel4.lean 34 declarations
TableDensity1Panel5.lean 34 declarations
TableDensityExpr.lean 106 declarations
TableDensityValues.lean 6 declarations
TableList.lean 11 declarations
TableMoments1.lean 864 declarations
TableMoments100.lean 864 declarations
TableMoments12.lean 864 declarations
TableMoments13.lean 864 declarations
TableMoments15.lean 864 declarations
TableMoments16.lean 864 declarations
TableMoments19.lean 864 declarations
TableMoments21.lean 864 declarations
TableMoments24.lean 864 declarations
TableMoments25.lean 864 declarations
TableMoments27.lean 864 declarations
TableMoments28.lean 864 declarations
TableMoments3.lean 864 declarations
TableMoments31.lean 864 declarations
TableMoments33.lean 864 declarations
TableMoments36.lean 864 declarations
TableMoments37.lean 864 declarations
TableMoments39.lean 864 declarations
TableMoments4.lean 864 declarations
TableMoments40.lean 864 declarations
TableMoments43.lean 864 declarations
TableMoments45.lean 864 declarations
TableMoments48.lean 864 declarations
TableMoments49.lean 864 declarations
TableMoments51.lean 864 declarations
TableMoments52.lean 864 declarations
TableMoments55.lean 864 declarations
TableMoments57.lean 864 declarations
TableMoments60.lean 864 declarations
TableMoments61.lean 864 declarations
TableMoments63.lean 864 declarations
TableMoments64.lean 864 declarations
TableMoments67.lean 864 declarations
TableMoments69.lean 864 declarations
TableMoments7.lean 864 declarations
TableMoments72.lean 864 declarations
TableMoments73.lean 864 declarations
TableMoments75.lean 864 declarations
TableMoments76.lean 864 declarations
TableMoments79.lean 864 declarations
TableMoments81.lean 864 declarations
TableMoments84.lean 864 declarations
TableMoments85.lean 864 declarations
TableMoments87.lean 864 declarations
TableMoments88.lean 864 declarations
TableMoments9.lean 864 declarations
TableMoments91.lean 864 declarations
TableMoments93.lean 864 declarations
TableMoments96.lean 864 declarations
TableMoments97.lean 864 declarations
TableMoments99.lean 864 declarations
TailCoefficients.lean 9 declarations
TransformedPowers10.lean 2290 declarations
TransformedPowers100.lean 2080 declarations
TransformedPowers20.lean 2080 declarations
TransformedPowers30.lean 2080 declarations
TransformedPowers40.lean 2080 declarations
TransformedPowers50.lean 2080 declarations
TransformedPowers60.lean 2080 declarations
TransformedPowers70.lean 2080 declarations
TransformedPowers80.lean 2080 declarations
TransformedPowers90.lean 2080 declarations
UMoments100.lean 2520 declarations
UMoments12.lean 2520 declarations
UMoments13.lean 2520 declarations
UMoments15.lean 2520 declarations
UMoments16.lean 2520 declarations
UMoments19.lean 2520 declarations
UMoments21.lean 2520 declarations
UMoments24.lean 2520 declarations
UMoments25.lean 2520 declarations
UMoments27.lean 2520 declarations
UMoments28.lean 2520 declarations
UMoments31.lean 2520 declarations
UMoments33.lean 2520 declarations
UMoments36.lean 2520 declarations
UMoments37.lean 2520 declarations
UMoments39.lean 2520 declarations
UMoments40.lean 2520 declarations
UMoments43.lean 2520 declarations
UMoments45.lean 2520 declarations
UMoments48.lean 2520 declarations
UMoments49.lean 2520 declarations
UMoments51.lean 2520 declarations
UMoments52.lean 2520 declarations
UMoments55.lean 2520 declarations
UMoments57.lean 2520 declarations
UMoments60.lean 2520 declarations
UMoments61.lean 2520 declarations
UMoments63.lean 2520 declarations
UMoments64.lean 2520 declarations
UMoments67.lean 2520 declarations
UMoments69.lean 2520 declarations
UMoments7.lean 2520 declarations
UMoments72.lean 2520 declarations
UMoments73.lean 2520 declarations
UMoments75.lean 2520 declarations
UMoments76.lean 2520 declarations
UMoments79.lean 2520 declarations
UMoments81.lean 2520 declarations
UMoments84.lean 2520 declarations
UMoments85.lean 2520 declarations
UMoments87.lean 2520 declarations
UMoments88.lean 2520 declarations
UMoments9.lean 2520 declarations
UMoments91.lean 2520 declarations
UMoments93.lean 2520 declarations
UMoments96.lean 2520 declarations
UMoments97.lean 2520 declarations
UMoments99.lean 2520 declarations
WCertificates.lean 22 declarations
WUCert100.lean 34 declarations
WUCert12.lean 34 declarations
WUCert13.lean 34 declarations
WUCert15.lean 34 declarations
WUCert16.lean 34 declarations
WUCert19.lean 34 declarations
WUCert21.lean 34 declarations
WUCert24.lean 34 declarations
WUCert25.lean 34 declarations
WUCert27.lean 34 declarations
WUCert28.lean 34 declarations
WUCert31.lean 34 declarations
WUCert33.lean 34 declarations
WUCert36.lean 34 declarations
WUCert37.lean 34 declarations
WUCert39.lean 34 declarations
WUCert40.lean 34 declarations
WUCert43.lean 34 declarations
WUCert45.lean 34 declarations
WUCert48.lean 34 declarations
WUCert49.lean 34 declarations
WUCert51.lean 34 declarations
WUCert52.lean 34 declarations
WUCert55.lean 34 declarations
WUCert57.lean 34 declarations
WUCert60.lean 34 declarations
WUCert61.lean 34 declarations
WUCert63.lean 34 declarations
WUCert64.lean 34 declarations
WUCert67.lean 34 declarations
WUCert69.lean 34 declarations
WUCert7.lean 34 declarations
WUCert72.lean 34 declarations
WUCert73.lean 34 declarations
WUCert75.lean 34 declarations
WUCert76.lean 34 declarations
WUCert79.lean 34 declarations
WUCert81.lean 34 declarations
WUCert84.lean 34 declarations
WUCert85.lean 34 declarations
WUCert87.lean 34 declarations
WUCert88.lean 34 declarations
WUCert9.lean 34 declarations
WUCert91.lean 34 declarations
WUCert93.lean 34 declarations
WUCert96.lean 34 declarations
WUCert97.lean 34 declarations
WUCert99.lean 34 declarations