`OAI/Combinatorics/HadwigerCounterexample/`

2995 declarations, 0 contain sorry, 0 declared as axioms; 276 files

Files

AdaptiveProjectionBounds.lean 4 declarations
AdaptiveRecordBounds.lean 3 declarations
AdditionalProbeBounds.lean 16 declarations
AffineFrames.lean 34 declarations
AggregateCostBounds.lean 6 declarations
AmbientBatchSlots.lean 28 declarations
AnalyticParameters.lean 9 declarations
AtomFlavors.lean 33 declarations
AttackCutDecomposition.lean 16 declarations
BaselineExtension.lean 3 declarations
BaselineForms.lean 12 declarations
BasisConditioning.lean 7 declarations
BatchCharacters.lean 10 declarations
BiasedRotationBounds.lean 2 declarations
BilinearBlockCorrelation.lean 5 declarations
BilinearCompression.lean 7 declarations
BinaryEvaluationForms.lean 10 declarations
BinaryMatrices.lean 19 declarations
BinaryMixingBounds.lean 8 declarations
BinaryPrescriptions.lean 11 declarations
BinaryStatusComparison.lean 14 declarations
BooleanLabels.lean 16 declarations
BoundedQueryTemplates.lean 19 declarations
CellPositivityScales.lean 7 declarations
CellPruning.lean 6 declarations
ChannelFactorization.lean 3 declarations
ChannelFrameLaws.lean 20 declarations
CollisionInequality.lean 7 declarations
CommonPartitionRefinement.lean 11 declarations
CommonPartitions.lean 2 declarations
CommonPredictions.lean 12 declarations
CompatibleOptionRealization.lean 15 declarations
CompatiblePairTests.lean 1 declarations
CompatibleTableEvents.lean 4 declarations
ComponentIndices.lean 17 declarations
ConcentrationScales.lean 11 declarations
ConditionalCellEntropy.lean 12 declarations
ConditionalFlags.lean 11 declarations
ConditionalFourCorners.lean 4 declarations
ConditionalLargeSetHits.lean 5 declarations
ConditionalProductLaws.lean 11 declarations
ConditionalProjection.lean 12 declarations
ConditionalSignaturePositivity.lean 7 declarations
ConditionedBatchLaws.lean 14 declarations
ConditionedCorrelations.lean 3 declarations
ConstructionScales.lean 6 declarations
CoordinateBlocks.lean 15 declarations
CoordinateDuality.lean 12 declarations
CoordinateEmbeddings.lean 12 declarations
CoverAlternatives.lean 3 declarations
CoverSpaces.lean 26 declarations
CrossForms.lean 16 declarations
CrossPatternCorrelation.lean 11 declarations
CrossPatternCounting.lean 17 declarations
CutIntegralBounds.lean 11 declarations
DependentPairConcentration.lean 5 declarations
DerivativeCompression.lean 10 declarations
EmpiricalInformation.lean 8 declarations
EndpointEvaluations.lean 19 declarations
EndpointGramRanks.lean 5 declarations
EndpointTemplateConcentration.lean 10 declarations
EntropyContainers.lean 3 declarations
ExplicitStatusEquations.lean 7 declarations
ExponentialGraphTransfer.lean 4 declarations
ExponentialRates.lean 24 declarations
FinalContradiction.lean 6 declarations
FiniteAffineLaws.lean 7 declarations
FiniteComparisonBounds.lean 13 declarations
FiniteConditioning.lean 19 declarations
FiniteDualSystems.lean 23 declarations
FiniteEntropy.lean 16 declarations
FiniteGraphTransfer.lean 6 declarations
FiniteLaws.lean 94 declarations
FiniteOptionLabels.lean 9 declarations
FinitePhaseAlternative.lean 6 declarations
FinitePredictions.lean 7 declarations
FiniteProjectionCenters.lean 5 declarations
FiniteTableEnumeration.lean 8 declarations
FixedPositionTests.lean 9 declarations
FlatLevelShifts.lean 1 declarations
FlatRankLevels.lean 8 declarations
ForbiddenPredictions.lean 3 declarations
FourCornerMasks.lean 18 declarations
FourCornerTrials.lean 6 declarations
FourCornerViews.lean 9 declarations
FourEdgeFamilies.lean 3 declarations
FourPhaseBits.lean 20 declarations
FrameIntersectionBounds.lean 8 declarations
FrameIntersectionCosts.lean 12 declarations
FrameOrbitLaws.lean 18 declarations
FrameRotations.lean 12 declarations
FreeBlockFourier.lean 11 declarations
FreeBlockLinearAction.lean 11 declarations
FreshGeneratorCorrection.lean 9 declarations
FrozenProjections.lean 19 declarations
FullTemplateComparison.lean 4 declarations
GradientRankBounds.lean 13 declarations
GradientRealization.lean 17 declarations
GramArrayConcentration.lean 2 declarations
GramCharacterExpansion.lean 17 declarations
GramCharacterQuotients.lean 8 declarations
GramConditionedLaws.lean 8 declarations
GramProbabilities.lean 14 declarations
GreedyExposures.lean 9 declarations
GroupedQueryIndependence.lean 15 declarations
HeadPartitionComparison.lean 3 declarations
HistogramBounds.lean 3 declarations
HistogramEnergyScales.lean 4 declarations
ImageCharacterBounds.lean 11 declarations
ImagePartitions.lean 11 declarations
IncompatibleMassBounds.lean 5 declarations
IndependentColumnBatches.lean 13 declarations
IndependentPhaseBounds.lean 17 declarations
IndependentTestWitnesses.lean 1 declarations
IndependentWeightCorrelation.lean 7 declarations
InformationSmallSetBounds.lean 10 declarations
InitialPartitionExistence.lean 3 declarations
InjectionWitnesses.lean 6 declarations
KeyDirections.lean 22 declarations
KeyProjectionBounds.lean 5 declarations
KeyReferenceLaws.lean 15 declarations
KeyTestCorrespondence.lean 7 declarations
LabeledGenerators.lean 21 declarations
LargeSetHits.lean 5 declarations
LeafMixtures.lean 22 declarations
LeafSurrogateExperiments.lean 8 declarations
LinearExtension.lean 6 declarations
LinearResponse.lean 14 declarations
LowRankKernelAlternative.lean 7 declarations
Main.lean 5 declarations
MatrixFactorization.lean 6 declarations
MatrixQuotients.lean 19 declarations
MatrixRankCounting.lean 12 declarations
MatrixRanks.lean 22 declarations
MixedImageBounds.lean 11 declarations
MixerConditions.lean 16 declarations
MixerExistence.lean 2 declarations
MixerProductVariables.lean 11 declarations
MomentCoordinates.lean 43 declarations
MomentLabelSupport.lean 5 declarations
MutualInformation.lean 8 declarations
NominalPointArrays.lean 12 declarations
NominalSpaces.lean 34 declarations
NumericalGradientTests.lean 12 declarations
NumericalGramPrescriptions.lean 6 declarations
OffsetEnergy.lean 16 declarations
OffsetFourierBounds.lean 8 declarations
OffsetLifting.lean 12 declarations
OffsetRecords.lean 28 declarations
OppositeEndpointForms.lean 8 declarations
OppositePredictions.lean 5 declarations
OrientationRankBounds.lean 5 declarations
OrthogonalSpectrumBounds.lean 6 declarations
PairIndexedTests.lean 6 declarations
PairedCollisionBounds.lean 6 declarations
PairedEventBounds.lean 2 declarations
PairedMassIdentities.lean 11 declarations
PairedOptions.lean 32 declarations
PairedRankBounds.lean 3 declarations
PairedTemplateConcentration.lean 6 declarations
ParameterExistence.lean 9 declarations
PartitionDeletionBounds.lean 3 declarations
PartitionSelection.lean 8 declarations
PhaseAlternativeSupport.lean 16 declarations
PhaseClassCompatibility.lean 13 declarations
PhaseMomentBounds.lean 9 declarations
PhaseParameters.lean 25 declarations
PhasePreparedOutcomes.lean 7 declarations
PinInjectionTests.lean 9 declarations
PointAtomVanishing.lean 3 declarations
PolarRankBounds.lean 7 declarations
PolynomialCompatibility.lean 3 declarations
PolynomialRankBounds.lean 4 declarations
PolynomialZeroTests.lean 11 declarations
PositiveTestMass.lean 12 declarations
PredictedDualCoefficients.lean 9 declarations
PredictedDualEvaluation.lean 4 declarations
PredictionClassBounds.lean 5 declarations
PredictionClasses.lean 19 declarations
PredictionDichotomy.lean 12 declarations
PredictionExactification.lean 6 declarations
PredictionExtraction.lean 15 declarations
PreliminaryRestrictions.lean 9 declarations
PreparationConditions.lean 35 declarations
PreparedOutcomes.lean 7 declarations
PreparedPopulationTrimming.lean 10 declarations
PrimalChannelDecomposition.lean 17 declarations
PrimalChannelTests.lean 9 declarations
PrimalSpaceCompression.lean 23 declarations
ProbePointMasses.lean 15 declarations
ProductCharacterTests.lean 6 declarations
ProductComparisonScales.lean 4 declarations
ProductCoordinateReplacement.lean 2 declarations
ProductLaws.lean 10 declarations
ProjectedSurrogates.lean 11 declarations
ProjectionEnergy.lean 18 declarations
ProjectionError.lean 12 declarations
ProjectionNets.lean 5 declarations
QuadraticFourier.lean 5 declarations
QuadraticTesters.lean 25 declarations
QueryConcentration.lean 11 declarations
RandomBinaryMixing.lean 9 declarations
RandomLinearTransforms.lean 12 declarations
RankEfficientDecomposition.lean 5 declarations
RankSubrectangles.lean 4 declarations
RareLeafEvents.lean 6 declarations
RareTestEvents.lean 11 declarations
RawFrameLaws.lean 25 declarations
RealizationConditions.lean 14 declarations
RectangleComparisons.lean 6 declarations
RectangleRegularity.lean 8 declarations
RecursiveComparisonErrors.lean 6 declarations
ReferenceProductTests.lean 5 declarations
RefinedPinImages.lean 17 declarations
RefinementEnergy.lean 9 declarations
ReindexedFourierSupport.lean 6 declarations
RelationMismatchBounds.lean 13 declarations
RelativeEntropy.lean 10 declarations
RelativeInjectionBounds.lean 5 declarations
RepeatedBatchLaws.lean 8 declarations
RepeatedQueryBounds.lean 6 declarations
RepeatedQueryEnergy.lean 4 declarations
ReservedLabels.lean 9 declarations
ResidualCutPairs.lean 8 declarations
ResidualRegularity.lean 7 declarations
ResponseAnnihilators.lean 7 declarations
ResponseSolvability.lean 21 declarations
RestrictedComparisonLaws.lean 8 declarations
RoundedRefinements.lean 4 declarations
SampledGraphs.lean 7 declarations
ScalarStatusAlgebra.lean 31 declarations
ScriptGramCorrespondence.lean 9 declarations
SimultaneousProjection.lean 6 declarations
SinglePositionExpansion.lean 12 declarations
SingletonPhaseTests.lean 7 declarations
SmallCoverBounds.lean 13 declarations
SpanDeficits.lean 16 declarations
SparseCutProfiles.lean 11 declarations
SparseLabelBounds.lean 10 declarations
StatusCharts.lean 24 declarations
StatusRecipes.lean 6 declarations
SumRankBounds.lean 7 declarations
SuperlevelBounds.lean 4 declarations
SupportedPhaseLaws.lean 14 declarations
SurrogateAggregation.lean 9 declarations
SurrogateProductBounds.lean 9 declarations
SurrogateQueryScores.lean 14 declarations
SurrogateStatusLaws.lean 21 declarations
SyntheticArraySlices.lean 10 declarations
SyntheticFailureBounds.lean 9 declarations
SyntheticParity.lean 14 declarations
SyntheticSliceComparison.lean 11 declarations
SyntheticSliceExperiments.lean 17 declarations
SyntheticTolerances.lean 1 declarations
TableInjectionTransfer.lean 10 declarations
TemplateTypicality.lean 12 declarations
TensorIntersections.lean 11 declarations
TerminalCut.lean 10 declarations
TesterFourierSupport.lean 11 declarations
TesterSummaryMass.lean 9 declarations
UltrafilterRates.lean 15 declarations
UnaryCellComparisons.lean 17 declarations
UnaryPositivityBounds.lean 5 declarations
UnaryQueryComparison.lean 7 declarations
UnaryQueryFrequencies.lean 3 declarations
UnaryRecords.lean 10 declarations
UnfilteredHistogramEnergy.lean 7 declarations
UniformLeafComparisons.lean 6 declarations
UniformSideComparisons.lean 6 declarations
UniqueStatusCoefficients.lean 3 declarations
UnseenCrossingFactorization.lean 6 declarations
WalshBounds.lean 14 declarations
WeakProductComparison.lean 2 declarations
WeightedPartitions.lean 15 declarations
ZeroDiscrepancyLemma.lean 3 declarations
ZeroDiscrepancyPrediction.lean 7 declarations