`ComparatorChallenges/`

11453 declarations, 539 contain sorry, 1 declared as axioms; 416 files

Files

AbhyankarSathaye.lean 1 declarations
AffineBernstein.lean 12 declarations
AlgorithmicThinTrees.lean 38 declarations
AmplitudeDamping.lean 23 declarations
ArnoldCounterexample.lean 20 declarations
ArtinCAT0.lean 14 declarations
ArtinParabolicIntersections.lean 20 declarations
AsymptoticallyMinimalLittlewood.lean 4 declarations
AtomicGaussian.lean 69 declarations
AuslanderReiten.lean 7 declarations
BackwardIntertwiners.lean 5 declarations
BalancedBoxRouting.lean 25 declarations
BalancedRyser.lean 9 declarations
BalancedThreeStack.lean 52 declarations
BallPacking.lean 9 declarations
BallPackingNecessity.lean 9 declarations
BarnetteHamiltonian.lean 6 declarations
BassTorsionFree.lean 35 declarations
BassTrace.lean 32 declarations
BenjaminiSchramm.lean 45 declarations
BernoulliNonflatInSeven.lean 13 declarations
BiholderTransport.lean 14 declarations
BinPackingGap.lean 75 declarations
BinaryEditLower.lean 10 declarations
BinaryMatching.lean 15 declarations
BinarySweep.lean 19 declarations
BipartiteCrossing.lean 12 declarations
BogomolovPopInjectivity.lean 27 declarations
BoltzmannNonuniqueness.lean 39 declarations
BooneHigman.lean 5 declarations
BorsukNine.lean 7 declarations
BoundedRecovery.lean 13 declarations
BoundedTreePotentials.lean 28 declarations
BoundedTreewidthL1.lean 6 declarations
Brenier.lean 14 declarations
Brennan.lean 9 declarations
BrennanSharp.lean 9 declarations
BufferedIsing.lean 17 declarations
C0Absorption.lean 6 declarations
C1EntropyCounterexample.lean 13 declarations
CHObstruction.lean 15 declarations
CKSBondiPenrose.lean 237 declarations
CannonGeometricAction.lean 17 declarations
CartierChartCompactnessSupport.lean 1 declarations
Catalan.lean 1 declarations
CayleyPercolation.lean 18 declarations
CharacterCriterion.lean 146 declarations
CharacterVarietiesAllSeamsSupport.lean 1 declarations
ChoicelessPolynomialTime.lean 78 declarations
CirculantHadamard.lean 6 declarations
ClassicalON.lean 13 declarations
CliqueFreeLog.lean 2 declarations
CoarseAssembly.lean 199 declarations
CoboundaryExpanders.lean 16 declarations
CommonBasesFPRAS.lean 16 declarations
CommutingDerivations.lean 18 declarations
CompactBanach.lean 3 declarations
CompleteCrossing.lean 13 declarations
CompleteCrouzeix.lean 6 declarations
ComplexCancellation.lean 11 declarations
Conductivity.lean 24 declarations
ConjugatePoints.lean 19 declarations
ContingencyTables.lean 38 declarations
ContinuousCircleWeight.lean 11 declarations
ContinuumCoulombHardness.lean 101 declarations
ContinuumTransition.lean 10 declarations
CoordinateSweeps.lean 64 declarations
CoordinateTrace.lean 64 declarations
Cotype.lean 13 declarations
CoulombCounterexample.lean 20 declarations
CoulombIonization.lean 20 declarations
CoulombRadii.lean 21 declarations
CourtadeKumar.lean 17 declarations
CoveringDensity.lean 23 declarations
CriticalPercolation.lean 11 declarations
CriticalSK.lean 31 declarations
CriticalSKMixing.lean 20 declarations
CriticalStripMass.lean 23 declarations
CriticalZ3.lean 20 declarations
CrouzeixHilbert.lean 25 declarations
CubicTorus.lean 19 declarations
CycleCliqueRamsey.lean 3 declarations
CycleDecomposition.lean 4 declarations
CylinderCovering.lean 109 declarations
DaugavetModuli.lean 17 declarations
DefocusingNLS.lean 40 declarations
DegreeRigidity.lean 9 declarations
DeligneDrinfeld.lean 39 declarations
DepthFive.lean 16 declarations
DepthThree.lean 25 declarations
DiamondDistortion.lean 37 declarations
DilutedSpin.lean 22 declarations
DimensionTenChannel.lean 10 declarations
DimensionTenPair.lean 26 declarations
DirectCrouzeix.lean 7 declarations
DirectedFeedback.lean 16 declarations
DirectionalBallisticity.lean 23 declarations
DirectionalWalk.lean 18 declarations
DirichletSevenEighths.lean 1 declarations
DiscreteLipschitzFree.lean 20 declarations
DiskMaximal.lean 10 declarations
Dixmier.lean 6 declarations
DixmierAllDiscrete.lean 6 declarations
DoublingHilbert.lean 4 declarations
DukePrimeDegree.lean 40 declarations
DuttaDomain.lean 11 declarations
DyadicAvoidance.lean 2 declarations
EditApproximation.lean 1156 declarations
EditDistance.lean 13 declarations
EgyptianFractions.lean 20 declarations
EilenbergGanea.lean 26 declarations
EinsteinFour.lean 35 declarations
ElasticityUniqueness.lean 24 declarations
ElementaryPositivity.lean 12 declarations
EntangledGames.lean 11 declarations
EntropyPhotonNumber.lean 18 declarations
ErdosReciprocal.lean 4 declarations
EuclideanFiveColor.lean 2 declarations
EuclideanRamsey.lean 11 declarations
EuclideanRamseyCircle.lean 4 declarations
EuclideanRamseyNine.lean 5 declarations
EuclideanRamseyQuadratic.lean 8 declarations
EuclideanRamseySpherical.lean 4 declarations
EuclideanRamseyTransitive.lean 4 declarations
EvenBarker.lean 4 declarations
ExactFourier.lean 11 declarations
ExactInfiniteness.lean 27 declarations
ExactQuantumFactoring.lean 28 declarations
FKCRT.lean 35 declarations
FactorGeneration.lean 6 declarations
FalconerAllDimensions.lean 1 declarations
FillingCoefficient.lean 24 declarations
FiniteCircle.lean 43 declarations
FiniteCongruenceGraph.lean 11 declarations
FiniteEntropySeparation.lean 20 declarations
FiniteFactor.lean 6 declarations
FinitisticAsymmetry.lean 4 declarations
FixedClauseThreshold.lean 9 declarations
ForcedNavierStokesComputation.lean 51 declarations
ForestSpace.lean 44 declarations
FormulaHitting.lean 11 declarations
FoulkesHowe.lean 7 declarations
FourRowPermanent.lean 10 declarations
FourierLLogL.lean 2 declarations
FreeIsing.lean 19 declarations
FreeUniformSpanningForest.lean 27 declarations
GammaPassage.lean 18 declarations
GaussianFiniteEntropy.lean 51 declarations
GaussianInformation.lean 53 declarations
GaussianMoat.lean 6 declarations
GaussianPropeller.lean 9 declarations
GaussianReplacement.lean 79 declarations
GeneralMahler.lean 4 declarations
GeneralizedStarHeight.lean 5 declarations
GotsmanLinial.lean 11 declarations
GrahamSpherical.lean 13 declarations
GrothendieckElementaryExpansion.lean 77 declarations
GroupRingDeterminant.lean 8 declarations
HadamardCubeFiber.lean 8 declarations
HadwigerCounterexample.lean 6 declarations
HalvingLines.lean 10 declarations
HardSphere.lean 31 declarations
HarmonicArtin.lean 14 declarations
HarmonicGrowth.lean 20 declarations
HeckeSevenEighths.lean 33 declarations
HeilbronnTriangle.lean 14 declarations
Heisenberg.lean 32 declarations
HenonEmden.lean 4 declarations
HilbertCrouzeix.lean 30 declarations
HoneycombBridgeFiniteness.lean 14 declarations
HoneycombBridgeMassSupport.lean 16 declarations
HoneycombFreeEnergy.lean 16 declarations
HotSpots.lean 9 declarations
HyperbolicCones.lean 16 declarations
HyperbolicObstruction.lean 24 declarations
HyperinvariantSubspaces.lean 5 declarations
IndependentProducts.lean 21 declarations
IndependentSets.lean 16 declarations
IndividualStrongInfiniteness.lean 53 declarations
InfiniteMatroid.lean 5 declarations
InfiniteMatroidCorollaries.lean 21 declarations
InterpolatedFactors.lean 42 declarations
InvariantIsing.lean 80 declarations
IrrationalRotation.lean 118 declarations
IrrationalTriangleBilliard.lean 17 declarations
IsingFiniteness.lean 14 declarations
IsometricImmersion.lean 7 declarations
Jacobsthal.lean 3 declarations
JacobsthalImproved.lean 3 declarations
JointDickman.lean 9 declarations
KLInvariance.lean 10 declarations
KMedianRecovery.lean 20 declarations
KMedianRefinedRecovery.lean 28 declarations
KMedianThreshold.lean 20 declarations
KServer.lean 10 declarations
KadisonRingrose.lean 4 declarations
KadisonSimilarity.lean 23 declarations
KahlerSplitting.lean 18 declarations
KaplanskyDirectFiniteness.lean 2 declarations
KaplanskyFinitelyPresented.lean 1 declarations
KaplanskyQuasitrace.lean 8 declarations
KaplanskyStableFiniteness.lean 33 declarations
Kervaire.lean 8 declarations
KoebeCircleDomains.lean 15 declarations
Laughlin.lean 14 declarations
LaughlinFock.lean 12 declarations
LaughlinGap.lean 14 declarations
LaughlinPlanar.lean 18 declarations
LiebThirring.lean 16 declarations
LipschitzEquivalence.lean 6 declarations
LipschitzHilbert.lean 10 declarations
ListHadwiger.lean 7 declarations
LittleFinitistic.lean 2 declarations
LittlewoodFiniteFlatness.lean 4 declarations
LogBrunnMinkowski.lean 7 declarations
LogConcaveQuery.lean 17 declarations
LogKodairaFiberNegative.lean 39 declarations
LogspaceEquality.lean 26 declarations
MUBSix.lean 17 declarations
MahlerConjecture.lean 2 declarations
MarkovType.lean 11 declarations
MassAction.lean 9 declarations
MatchingAffineLift.lean 7 declarations
MatchingEntropy.lean 14 declarations
MatchingEntropyBounds.lean 15 declarations
MatchingFPRAS.lean 19 declarations
MatchingPSD.lean 12 declarations
MatrixFields.lean 15 declarations
MatrixMultiplication.lean 21 declarations
MatrixRemoval.lean 12 declarations
MatroidProphet.lean 17 declarations
MatroidSecretary.lean 34 declarations
MaximalSeshadriConstants.lean 46 declarations
MemoryPrecision.lean 78 declarations
MetricEntropyDuality.lean 9 declarations
MetricKMedian.lean 10 declarations
MidpointLenses.lean 36 declarations
MinUncut.lean 19 declarations
Nagata.lean 48 declarations
Naimark.lean 8 declarations
NavierStokesAlternating.lean 57 declarations
NavierStokesVelocity.lean 202 declarations
NodalLength.lean 9 declarations
NoiselessRegression.lean 20 declarations
NuclearUltrapower.lean 30 declarations
OccupiedOverlap.lean 43 declarations
OddKaplansky.lean 5 declarations
OneTapeSpace.lean 55 declarations
OneWayLiveness.lean 23 declarations
OptimalMaxCut.lean 25 declarations
OrdinaryElliott.lean 7 declarations
OrdinaryTwoPointCorrelations.lean 12 declarations
OstmannComplete.lean 7 declarations
OstmannPrimes.lean 1 declarations
ParityLifts.lean 38 declarations
PartialPermutation.lean 18 declarations
PartitionConsistency.lean 48 declarations
PartitionPrinciple.lean 51 declarations
PattersonFirstMoment.lean 24 declarations
PerceptronFreeEnergy.lean 28 declarations
PerfectCompleteness.lean 31 declarations
PeriodicGroup.lean 10 declarations
PeriodicTilingThree.lean 13 declarations
PermanentCubic.lean 7 declarations
PettyProjectionVolume.lean 11 declarations
PiExponent.lean 1 declarations
PinchedKahler.lean 40 declarations
PinnedDistances.lean 7 declarations
PlanarAndersonSpectrum.lean 7 declarations
PlanarFalconer.lean 4 declarations
PlanarFirstPassage.lean 18 declarations
PlanarL1.lean 5 declarations
PlanarPacking.lean 5 declarations
PlanarUnitDistances.lean 5 declarations
PlaneColoring.lean 3 declarations
PolycyclicRecognition.lean 23 declarations
PosteriorReplicas.lean 77 declarations
PowerFreeValues.lean 8 declarations
PrimeGaps.lean 7 declarations
ProductBrown.lean 66 declarations
ProjectionCounterexample.lean 9 declarations
ProjectionMoments.lean 91 declarations
ProjectionVolume.lean 12 declarations
QACParity.lean 17 declarations
QuadricBundles.lean 35 declarations
QuantitativeVanDerWaerden.lean 5 declarations
QuasiRiemannHypothesis.lean 1 declarations
QuinticLienard.lean 6 declarations
RadialDensityInterval.lean 14 declarations
RadialTransition.lean 14 declarations
RamseyFive.lean 5 declarations
RandomizedMeanPayoff.lean 24 declarations
RationalHitting.lean 23 declarations
RealL1Renorming.lean 7 declarations
RecursivePotentials.lean 160 declarations
ReflexiveFixedPoints.lean 2 declarations
RegularParity.lean 16 declarations
RelativeGeneration.lean 12 declarations
RieszQuantitative.lean 9 declarations
Rokhlin.lean 5 declarations
RuledCovering.lean 47 declarations
RyserCovering.lean 11 declarations
RyserOddExtensions.lean 12 declarations
SATComputability.lean 9 declarations
SATSharpness.lean 17 declarations
SATVariance.lean 17 declarations
SKBarriers.lean 20 declarations
SKFullSupport.lean 17 declarations
SKHighTemperature.lean 19 declarations
SKRatio.lean 17 declarations
SKValue.lean 36 declarations
SLELowerPositivity.lean 15 declarations
Saxl.lean 15 declarations
SecondKahnKalai.lean 13 declarations
SelfSimilar.lean 13 declarations
SelfSimilarCorollaries.lean 12 declarations
SensitivitySeparation.lean 6 declarations
SeparableQuotientNegative.lean 4 declarations
SeymourSecondNeighborhood.lean 5 declarations
SharpCAT0Filling.lean 25 declarations
SharpLogRamsey.lean 5 declarations
SharpThreshold.lean 13 declarations
ShortEgyptianFractions.lean 4 declarations
SidorenkoCounterexample.lean 8 declarations
SiegelZeros.lean 2 declarations
SignedFiniteBand.lean 8 declarations
SignedSweepMoment.lean 37 declarations
SimpleAmenable.lean 2 declarations
SimpleOvergroups.lean 4 declarations
SingleFold.lean 4 declarations
SingleLatticeCovering.lean 4 declarations
SingletonLoopMatching.lean 25 declarations
SmoothInitialForm.lean 6 declarations
SmoothObstruction.lean 10 declarations
SmoothYau.lean 20 declarations
SnakyCertificate.lean 671 declarations
SnakyConditional.lean 10 declarations
SnakyTwentyOne.lean 10 declarations
SoftChannel204.lean 35 declarations
SolenoidalSheetPrograms.lean 43 declarations
SphericalField.lean 89 declarations
SpinAngle.lean 73 declarations
SplitTangentIntegrability.lean 21 declarations
SquareDifference.lean 2 declarations
SquareRootDegree.lean 13 declarations
StableCoordinateFour.lean 14 declarations
StandardMapComponents.lean 21 declarations
StandardMapEntropy.lean 13 declarations
StandardMapLyapunov.lean 23 declarations
SteinitzBergstrom.lean 4 declarations
StrictMeans.lean 8 declarations
StrongKadisonKastler.lean 7 declarations
StrongThinTree.lean 7 declarations
StronglyRayleighDPP.lean 27 declarations
StructuralCrouzeix.lean 19 declarations
SubpolynomialLp.lean 5 declarations
SubsphereCurrent.lean 62 declarations
Superstring.lean 11 declarations
SurfaceConeCandidateSupport.lean 1 declarations
SurfaceImmersion.lean 7 declarations
SwitchChain.lean 31 declarations
SymmetricDomains.lean 9 declarations
SymmetricMahlerEquality.lean 6 declarations
SymmetricPolar.lean 10 declarations
Tachikawa.lean 4 declarations
TalagrandDiscreteConvexity.lean 9 declarations
TalagrandExpectationThreshold.lean 13 declarations
TamingCompatibility.lean 14 declarations
ThomasonModelStructures.lean 112 declarations
ThompsonNonamenability.lean 13 declarations
ThorpFirstReciprocal.lean 35 declarations
ThorpRemaining.lean 99 declarations
ThorpRouting.lean 409 declarations
ThorpWeightedCompatibility.lean 8 declarations
ThreeMachine.lean 19 declarations
ThreeStateSupercritical.lean 21 declarations
ThreeStateTreeClauses.lean 20 declarations
ThreeTorus.lean 13 declarations
TingleySphereIsometry.lean 3 declarations
TorsionFreeHyperbolic.lean 5 declarations
TorsionFreeZeroDivisors.lean 4 declarations
TotientAsymptotic.lean 36 declarations
TotientCompanionZero.lean 23 declarations
TraceIdealTransportSupport.lean 47 declarations
TraceReconstruction.lean 16 declarations
TreeEdit.lean 8 declarations
TriangleFace.lean 26 declarations
TriangleRemoval.lean 12 declarations
TriangularCovering.lean 17 declarations
TriangularEnergy.lean 21 declarations
TriangularGaussian.lean 68 declarations
TriangularHilbert.lean 10 declarations
TruffetCounterexample.lean 31 declarations
TwoWayComplementation.lean 6 declarations
TwoWayDeterminization.lean 9 declarations
TypeSystemNormalization.lean 19 declarations
UniformCommutator.lean 4 declarations
UniformFourier.lean 58 declarations
UniformGamma.lean 68 declarations
UniformKServer.lean 32 declarations
UniformSparsestCut.lean 8 declarations
UniqueGamesTheorem.lean 32 declarations
UniversalFInfinity.lean 2 declarations
UniversalTensorSquares.lean 13 declarations
VariableWL.lean 28 declarations
VelocityHemisphere.lean 22 declarations
VertexAlgebraNet.lean 89 declarations
VertexCover.lean 28 declarations
VlasovMaxwell.lean 29 declarations
WLIdentification.lean 33 declarations
WeakHessian.lean 46 declarations
WeakMTWGlobalSupport.lean 11 declarations
WeightedSweepMoments.lean 54 declarations
WeisfeilerLeman.lean 53 declarations
WitnessedChoice.lean 57 declarations
YauCounterexample.lean 13 declarations