`OAI/Analysis/PlanarPacking/`

556684 declarations, 0 contain sorry, 0 declared as axioms; 562 files

Folders

Certificate/ 446 files, 547707 declarations

Files

AtomTail.lean 21 declarations
Barrier.lean 5 declarations
BarrierEndpoints.lean 9 declarations
BarrierProduct.lean 21 declarations
Basic.lean 3 declarations
BasisIntervals.lean 418 declarations
BasisQuadrature.lean 3 declarations
BernsteinBoxes.lean 5 declarations
BernsteinSign.lean 8 declarations
CanonicalRows.lean 109 declarations
Cardinal.lean 133 declarations
CoarseTaylor.lean 6 declarations
CoefficientClose.lean 3 declarations
ContactData.lean 10 declarations
CoupledFull.lean 8 declarations
DataSplit.lean 7 declarations
DataTail.lean 4 declarations
DerivativeEnvelope.lean 1 declarations
Dilation.lean 10 declarations
DirectBounds.lean 3 declarations
Entire.lean 101 declarations
Entries.lean 6 declarations
Envelopes.lean 13 declarations
ExactJets.lean 10 declarations
ExactPair.lean 15 declarations
Fejer.lean 635 declarations
FiniteCoordinates.lean 14 declarations
FiniteFull.lean 27 declarations
FiniteInverse.lean 12 declarations
FiniteLift.lean 8 declarations
FiniteProjection.lean 9 declarations
FiniteSplit.lean 8 declarations
FiniteTail.lean 13 declarations
FiniteU.lean 7 declarations
FixedRHS.lean 4 declarations
FourierPairSupport.lean 36 declarations
FullMomentBridge.lean 8 declarations
GaussianSeries.lean 5 declarations
GlobalSign.lean 4 declarations
Grid.lean 3282 declarations
HalfGapAnalytic.lean 4 declarations
HalfGapCore.lean 12 declarations
HalfGapSmall.lean 8 declarations
HalfGapTypes.lean 4 declarations
HalfSign0.lean 1 declarations
HalfSign1.lean 3 declarations
HalfSign12.lean 4 declarations
HalfSign13.lean 4 declarations
HalfSign15.lean 4 declarations
HalfSign16.lean 4 declarations
HalfSign19.lean 4 declarations
HalfSign21.lean 4 declarations
HalfSign24.lean 4 declarations
HalfSign25.lean 4 declarations
HalfSign27.lean 4 declarations
HalfSign28.lean 4 declarations
HalfSign3.lean 4 declarations
HalfSign31.lean 4 declarations
HalfSign33.lean 4 declarations
HalfSign36.lean 4 declarations
HalfSign37.lean 4 declarations
HalfSign39.lean 4 declarations
HalfSign4.lean 4 declarations
HalfSign40.lean 4 declarations
HalfSign7.lean 4 declarations
HalfSign9.lean 4 declarations
HexLattice.lean 15 declarations
HighFactorBase.lean 9 declarations
HighMomentsBase.lean 9 declarations
HighRuleBridge.lean 6 declarations
Indices.lean 33 declarations
InterpolationError.lean 8 declarations
Intervals.lean 129 declarations
JetError.lean 11 declarations
KernelDerivative.lean 4 declarations
LatticeGaussian.lean 17 declarations
LatticeIntegration.lean 4 declarations
LatticePoisson.lean 11 declarations
Main.lean 4 declarations
MatrixIntervals.lean 5 declarations
MatrixInverse.lean 4 declarations
MatrixL1.lean 11 declarations
MixedTaylor.lean 3 declarations
MomentRecurrence.lean 7 declarations
NodeIntervals.lean 24 declarations
Nodes.lean 38 declarations
NormalizedCandidate.lean 11 declarations
OriginIdentity.lean 8 declarations
OriginPositive.lean 5 declarations
Quadrature.lean 52 declarations
RationalBounds.lean 26 declarations
RationalEnvelopes.lean 1 declarations
ResidualBase.lean 5 declarations
ResidualFinite.lean 6 declarations
ResidualTail.lean 2 declarations
Roots.lean 3269 declarations
Schur.lean 7 declarations
SignBounds.lean 12 declarations
SignCaps.lean 4 declarations
TableDensityBase.lean 7 declarations
TableDensityBridge.lean 4 declarations
TableEnvelopes.lean 2 declarations
TableKBridge.lean 2 declarations
TableMomentsBase.lean 10 declarations
TableNorms.lean 5 declarations
TableRuleBridge.lean 1 declarations
TailBarrier.lean 3 declarations
TailEnvelope.lean 6 declarations
TailHead.lean 14 declarations
TailHeadBounds.lean 7 declarations
TailHeadClose.lean 7 declarations
TailRationalBase.lean 3 declarations
TailSign.lean 3 declarations
TailSplit.lean 6 declarations
TaylorControl.lean 14 declarations
Theta.lean 7 declarations