OAI/Combinatorics/RamseyFive/Geometry/
1044 declarations, 0 contain sorry, 0 declared as axioms; 148 files
Files
- AbsModifiedPointScore.lean 3 declarations
- AmbientOriginalDomination.lean 2 declarations
- AmbientPairPublic.lean 12 declarations
- AmbientPivotPotential.lean 2 declarations
- BaseCapturedLaw.lean 10 declarations
- BaseFinitePublic.lean 17 declarations
- BasePublicFamily.lean 7 declarations
- BaseSmallLaw.lean 9 declarations
- CapturedGlobalRadialMoment.lean 3 declarations
- CardFilterContainment.lean 16 declarations
- CardIndexed.lean 2 declarations
- CardMul.lean 2 declarations
- Center.lean 5 declarations
- CommonNeighborDichotomy.lean 2 declarations
- CompressionRecurrence.lean 2 declarations
- ConcretePivot.lean 14 declarations
- CoreGeometry.lean 15 declarations
- Cores.lean 8 declarations
- DegreeStrengthCount.lean 3 declarations
- DimensionFourHighIntegrals.lean 1 declarations
- DimensionFourHighLaw.lean 4 declarations
- DimensionFourHighProtocol.lean 2 declarations
- DimensionFourHighPublic.lean 1 declarations
- DimensionFourLowAmbient.lean 5 declarations
- DimensionFourLowLaw.lean 2 declarations
- DimensionFourLowProcedure.lean 2 declarations
- DimensionFourLowTraining.lean 2 declarations
- DimensionFourLowValidation.lean 1 declarations
- DimensionThreeProcedure.lean 1 declarations
- DimensionThreePublic.lean 2 declarations
- DimensionThreeTails.lean 3 declarations
- DimensionTwo.lean 1 declarations
- DimensionTwoOriented.lean 5 declarations
- DimensionTwoPublic.lean 4 declarations
- DimensionalScale.lean 7 declarations
- DyadCount.lean 2 declarations
- EmptyVariableTree.lean 5 declarations
- ExceptionalCenters.lean 7 declarations
- Failure.lean 13 declarations
- FiniteFamily.lean 10 declarations
- FiniteNode.lean 5 declarations
- FiniteTreeFailure.lean 1 declarations
- FinrankSpanImage.lean 9 declarations
- FlagGraph.lean 18 declarations
- FlatAtlas.lean 7 declarations
- FlatPoints.lean 24 declarations
- FlatSection.lean 11 declarations
- FourFinitePredictor.lean 14 declarations
- FourHeader.lean 2 declarations
- FourSelected.lean 6 declarations
- GeneralReversedCode.lean 13 declarations
- GeometricRestriction.lean 43 declarations
- GeometryScaleOrientedLower.lean 6 declarations
- GoodCoreRanks.lean 2 declarations
- GuardedNode.lean 5 declarations
- GuardedNodeEncoder.lean 3 declarations
- GuardedNodeSent.lean 11 declarations
- HighGeometryClosure.lean 11 declarations
- HighPairVariance.lean 13 declarations
- HighPeelExceptions.lean 3 declarations
- HighPolyConstant.lean 4 declarations
- HighSampleGrowth.lean 4 declarations
- HyperplaneHigh.lean 4 declarations
- IncidencesDegrees.lean 3 declarations
- LargeCells.lean 16 declarations
- LevelTargetBounds.lean 4 declarations
- LinearForm.lean 6 declarations
- LocalLines.lean 9 declarations
- LowConflictSubsets.lean 1 declarations
- MassHyperplane.lean 5 declarations
- MemPairRank.lean 7 declarations
- ModifiedRadialSchedule.lean 6 declarations
- MomentCutoffPolynomialTail.lean 4 declarations
- MomentOrder.lean 12 declarations
- MomentPolynomialTail.lean 8 declarations
- OrderedTargetRetention.lean 2 declarations
- OrientedNodeCaps.lean 3 declarations
- OrientedNodeProcess.lean 4 declarations
- OrientedPivotTree.lean 14 declarations
- OrientedTreeDomains.lean 18 declarations
- OrientedTreePotential.lean 2 declarations
- OriginalAmbientDomination.lean 2 declarations
- OriginalReadiness.lean 3 declarations
- Outside.lean 17 declarations
- OutsideCard.lean 4 declarations
- OutsidePairCard.lean 9 declarations
- OverlapDyads.lean 15 declarations
- OwnQuery.lean 8 declarations
- Peeling.lean 5 declarations
- PeelingGeometry.lean 16 declarations
- PencilCount.lean 15 declarations
- PencilLineSum.lean 2 declarations
- PlaneAnchor.lean 7 declarations
- PlaneBranch.lean 4 declarations
- PlaneCommonNeighbors.lean 7 declarations
- PlaneExceptionScalars.lean 7 declarations
- PlaneExceptions.lean 7 declarations
- PlanePublicDefs.lean 10 declarations
- PlaneStrongExceptions.lean 7 declarations
- PointStrength.lean 6 declarations
- PowerValidation.lean 6 declarations
- PredictorReverseCap.lean 13 declarations
- ProducedPairOriginal.lean 2 declarations
- ProjectiveEquiv.lean 6 declarations
- ProjectiveExpectedLevelLoss.lean 6 declarations
- ProjectiveHighCapturedMoment.lean 5 declarations
- ProjectiveLinePairPacking.lean 1 declarations
- PublicDecoder.lean 11 declarations
- Q.lean 16 declarations
- RadialAlternatives.lean 16 declarations
- RadialLabel.lean 5 declarations
- RadialOffException.lean 9 declarations
- ReadyRefinement.lean 6 declarations
- RectangleTransport.lean 4 declarations
- ReverseAfterCapture.lean 3 declarations
- ReversedBasePublic.lean 6 declarations
- RichHyperplaneVariance.lean 11 declarations
- RowPowerTail.lean 3 declarations
- SampledPoints.lean 6 declarations
- ScoreDegreeLowNormalized.lean 9 declarations
- ScorePairCapturedNormalized.lean 4 declarations
- ScoredMessage.lean 8 declarations
- SplitEquiv.lean 12 declarations
- StreamGeometry.lean 9 declarations
- SubspacePointsEquiv.lean 38 declarations
- SurvivorRank.lean 7 declarations
- TargetCaps.lean 3 declarations
- TargetCoherence.lean 2 declarations
- TargetRetention.lean 1 declarations
- ThreeBranch.lean 9 declarations
- ThreeCoordinateCertified.lean 11 declarations
- ThreeFiniteOriented.lean 6 declarations
- ThreeFinitePredictor.lean 3 declarations
- ThreeLocal.lean 1 declarations
- ThreeOriented.lean 5 declarations
- ThreePublic.lean 7 declarations
- ThreePublicDefs.lean 16 declarations
- ThreeSelected.lean 6 declarations
- TrainingLineCard.lean 6 declarations
- TreeFailure.lean 2 declarations
- TreeShape.lean 7 declarations
- TreeTrims.lean 3 declarations
- TwoAmbientCaps.lean 6 declarations
- TwoFinitePublic.lean 7 declarations
- TwoPublic.lean 2 declarations
- TwoPublicCaps.lean 2 declarations
- UniformHighTail.lean 4 declarations
- ValidationOriginalTailWide.lean 5 declarations