`OAI/Combinatorics/SumProduct/Alignment/`

4685 declarations, 0 contain sorry, 0 declared as axioms; 259 files

Files

AbelianMalcev01.lean 21 declarations
AbelianMalcev02.lean 14 declarations
Admissible01.lean 24 declarations
AffineCoefficient01.lean 6 declarations
AffineOrbit01.lean 23 declarations
AlignmentMass01.lean 18 declarations
AllLevel01.lean 33 declarations
AllLevel02.lean 19 declarations
AllLevel03.lean 12 declarations
AllLevel04.lean 21 declarations
AllLevel05.lean 29 declarations
AllLevel06.lean 18 declarations
AllLevel07.lean 11 declarations
AllLevel08.lean 8 declarations
AllLevel09.lean 11 declarations
AllLevel10.lean 11 declarations
AllLevel11.lean 22 declarations
AllLevel12.lean 15 declarations
AllLevel13.lean 18 declarations
AllLevel14.lean 18 declarations
AllLevel15.lean 8 declarations
BinomialDifference01.lean 26 declarations
Blocks01.lean 41 declarations
Blocks02.lean 29 declarations
BooleanBinomial01.lean 48 declarations
BooleanRough01.lean 62 declarations
BooleanRough02.lean 11 declarations
BoxPolynomial01.lean 34 declarations
BracketDrift01.lean 8 declarations
BracketHyperplanes01.lean 12 declarations
BracketHyperplanes02.lean 7 declarations
CentralFiber01.lean 12 declarations
CentralQuotient01.lean 17 declarations
CharacterFactorization01.lean 18 declarations
CoefficientPeeling01.lean 13 declarations
CompactConvex01.lean 20 declarations
CompactFamily01.lean 17 declarations
ComparableBox01.lean 13 declarations
ComparableBox02.lean 11 declarations
ComparableBox03.lean 5 declarations
ConstantCoefficient01.lean 31 declarations
CoordinateSubspace01.lean 28 declarations
CorrectedBox01.lean 15 declarations
CorrectedBox02.lean 9 declarations
CorrectedBox03.lean 14 declarations
CorrectedBox04.lean 11 declarations
CorrectedBox05.lean 17 declarations
CorrectedBox06.lean 13 declarations
CorrectedBox07.lean 10 declarations
CoveringSubspace01.lean 10 declarations
CubeFaces01.lean 24 declarations
CubeFaces02.lean 17 declarations
CubeKernel01.lean 9 declarations
CubeLocal01.lean 20 declarations
CubeLocal02.lean 5 declarations
CubeLocal03.lean 16 declarations
CubeLocal04.lean 4 declarations
CubeLocal05.lean 7 declarations
CubeLocal06.lean 4 declarations
CubeLocal07.lean 4 declarations
CubeLocal08.lean 3 declarations
CubeLocal09.lean 8 declarations
CubeParameter01.lean 27 declarations
CubePolynomials01.lean 26 declarations
CubeRational01.lean 71 declarations
CubeRationalization01.lean 10 declarations
CubeTaylor01.lean 29 declarations
CubeTaylor02.lean 21 declarations
DenseBoolean01.lean 17 declarations
DenseBox01.lean 11 declarations
DensePolynomial01.lean 19 declarations
DenseRough01.lean 9 declarations
DyadicHarmonic01.lean 18 declarations
EmbeddedCube01.lean 29 declarations
FactorCoefficient01.lean 10 declarations
FejerDetection01.lean 9 declarations
FilteredShears01.lean 37 declarations
FiniteCover01.lean 8 declarations
FiniteMenu01.lean 34 declarations
FinitePiece01.lean 25 declarations
FourierObstruction01.lean 15 declarations
GlobalPoint01.lean 26 declarations
HarmonicExposure01.lean 7 declarations
HarmonicExposure02.lean 10 declarations
HarmonicTranslation01.lean 35 declarations
HierarchyRates01.lean 8 declarations
IntegerAlignment01.lean 19 declarations
IntegerArrays01.lean 11 declarations
IntegerArrays02.lean 23 declarations
IntegerArrays03.lean 25 declarations
IntegerArrays04.lean 4 declarations
IntegerArrays05.lean 15 declarations
IntegerArrays06.lean 13 declarations
IntegerArrays07.lean 11 declarations
IntegerArrays08.lean 6 declarations
IntegerArrays09.lean 6 declarations
IntegerArrays10.lean 21 declarations
IntegerArrays11.lean 3 declarations
IntegerArrays12.lean 28 declarations
IntegerArrays13.lean 22 declarations
IntegerArrays14.lean 20 declarations
IntegerArrays15.lean 15 declarations
IntegerHyperplane01.lean 33 declarations
IntegerHyperplane02.lean 15 declarations
LagrangeBounds01.lean 12 declarations
LeibmanSquare01.lean 38 declarations
LeibmanSquare02.lean 26 declarations
LeibmanSquare03.lean 6 declarations
LeibmanSquare04.lean 11 declarations
LeibmanSquare05.lean 10 declarations
MacroSelection01.lean 13 declarations
MacroSelection02.lean 5 declarations
Main.lean 258 imports, no declarations
MalcevCentral01.lean 19 declarations
MalcevCharacters01.lean 18 declarations
MalcevHorizontal01.lean 35 declarations
MalcevHorizontal02.lean 21 declarations
MalcevHorizontal03.lean 13 declarations
MalcevTail01.lean 21 declarations
MalcevTail02.lean 29 declarations
MalcevTail03.lean 10 declarations
MalcevWeighted01.lean 17 declarations
MalcevWeighted02.lean 12 declarations
MenuLiteral01.lean 11 declarations
MicrocellFibers01.lean 18 declarations
MicrocellHarmonic01.lean 16 declarations
MicrocellSaturation01.lean 19 declarations
MicrocellScale01.lean 25 declarations
NearLattice01.lean 8 declarations
PairTail01.lean 39 declarations
PairTail02.lean 18 declarations
PairTail03.lean 19 declarations
PairTail04.lean 17 declarations
PairTail05.lean 24 declarations
PairTail06.lean 33 declarations
ParametricSmooth01.lean 28 declarations
PhysicalDecay01.lean 9 declarations
PivotExtension01.lean 17 declarations
PivotExtension02.lean 13 declarations
PivotPaths01.lean 21 declarations
PivotPaths02.lean 18 declarations
PivotPaths03.lean 29 declarations
PointLaw01.lean 13 declarations
PointLaw02.lean 13 declarations
PolynomialArray01.lean 27 declarations
PolynomialCharacter01.lean 6 declarations
PolynomialDephasing01.lean 22 declarations
PolynomialLine01.lean 27 declarations
PolynomialWeyl01.lean 46 declarations
ProductExposure01.lean 11 declarations
ProductExposure02.lean 22 declarations
ProductExposure03.lean 16 declarations
ProductExposure04.lean 10 declarations
ProgressionPartition01.lean 13 declarations
RationalEchelon01.lean 12 declarations
RationalEchelon02.lean 52 declarations
RationalFactor01.lean 17 declarations
RationalLattice01.lean 17 declarations
RationalLattice02.lean 30 declarations
RationalLattice03.lean 22 declarations
RationalLattice04.lean 46 declarations
RationalLattice05.lean 41 declarations
RationalLattice06.lean 15 declarations
RationalLattice07.lean 23 declarations
RationalLattice08.lean 24 declarations
RationalLattice09.lean 6 declarations
RationalLattice10.lean 5 declarations
RationalLattice11.lean 42 declarations
RationalLattice12.lean 27 declarations
RationalLattice13.lean 13 declarations
RationalLattice14.lean 16 declarations
RationalLattice15.lean 26 declarations
RationalLattice16.lean 30 declarations
RationalLattice17.lean 13 declarations
RationalLattice18.lean 22 declarations
RationalLattice19.lean 26 declarations
RationalLattice20.lean 6 declarations
RationalLattice21.lean 19 declarations
RationalLattice22.lean 22 declarations
RationalLattice23.lean 7 declarations
RationalLattice24.lean 21 declarations
RationalLattice25.lean 11 declarations
RationalLattice26.lean 22 declarations
RationalLattice27.lean 18 declarations
RationalQuotient01.lean 23 declarations
RationalTail01.lean 29 declarations
RationalTail02.lean 16 declarations
RationalTriangular01.lean 25 declarations
RawHarmonic01.lean 18 declarations
RawMenu.lean 11 declarations
RegularResidue01.lean 16 declarations
ResidueAlignment01.lean 7 declarations
RoughArray01.lean 25 declarations
RoughArray02.lean 10 declarations
RoughArray03.lean 12 declarations
RoughArray04.lean 2 declarations
RoughCovered01.lean 3 declarations
RoughCovered02.lean 3 declarations
RoughCube01.lean 10 declarations
RoughCube02.lean 11 declarations
RoughDimension01.lean 11 declarations
RoughDyadic01.lean 23 declarations
RoughExtremal01.lean 18 declarations
RoughFace01.lean 10 declarations
RoughFace02.lean 15 declarations
RoughFace03.lean 4 declarations
RoughInterpolation01.lean 21 declarations
RoughJoint01.lean 21 declarations
RoughKernel01.lean 27 declarations
RoughKernel02.lean 16 declarations
RoughKernel03.lean 9 declarations
RoughKernel04.lean 6 declarations
RoughKernel05.lean 5 declarations
RoughLiteral01.lean 34 declarations
RoughLog01.lean 15 declarations
RoughPhysical01.lean 13 declarations
RoughProduct01.lean 20 declarations
RoughProduct02.lean 15 declarations
RoughProduct03.lean 14 declarations
RoughRational01.lean 20 declarations
RoughReal01.lean 15 declarations
RoughSampling01.lean 18 declarations
RoughSampling02.lean 14 declarations
RoughSplit01.lean 5 declarations
RoughTopological01.lean 8 declarations
RoughTopological02.lean 3 declarations
RoughTopological03.lean 3 declarations
ScalarDifference01.lean 35 declarations
SmoothBinomial01.lean 19 declarations
SquareHorizontal01.lean 32 declarations
SquareInduction01.lean 3 declarations
SquareInduction02.lean 6 declarations
SquareInduction03.lean 3 declarations
SquareInduction04.lean 5 declarations
SquareInduction05.lean 8 declarations
SquareInduction06.lean 3 declarations
SquareInduction07.lean 3 declarations
SquareInduction08.lean 5 declarations
SquareInduction09.lean 8 declarations
SquareInduction10.lean 3 declarations
SquareInduction11.lean 4 declarations
SquareInduction12.lean 5 declarations
SquareInduction13.lean 3 declarations
SquareInduction14.lean 6 declarations
TailCharacter01.lean 42 declarations
TorusVertical01.lean 39 declarations
TriangularDenominators01.lean 17 declarations
TriangularLattice01.lean 20 declarations
UniformSlow01.lean 9 declarations
UnitInterval01.lean 17 declarations
WeightedBoxes01.lean 30 declarations
WeightedLinear01.lean 24 declarations
WeightedPolynomial01.lean 21 declarations
WeightedPolynomial02.lean 25 declarations
WeylInverse01.lean 8 declarations
WordPlan01.lean 227 declarations
WordPlan02.lean 23 declarations
WordPlan03.lean 4 declarations
WordPlan04.lean 5 declarations