`OAI/Analysis/CircleDomains/Selection/`

1564 declarations, 0 contain sorry, 0 declared as axioms; 475 files

Files

ActualOneEndedSplicing.lean 1 declarations
ActualScalarJump.lean 1 declarations
ActualTwoEndedSplicing.lean 1 declarations
ActualVerticalScalarJump.lean 1 declarations
AffinePhysicalRestriction.lean 7 declarations
AffineResidualBounds.lean 2 declarations
AffineResidualExposure.lean 3 declarations
AffineTagRestriction.lean 9 declarations
AllowedCountableConcatenation.lean 2 declarations
AlternatingTailCrossing.lean 1 declarations
AnalyticWordBranch.lean 7 declarations
AnchorTailAttachment.lean 1 declarations
AnchorTruncation.lean 4 declarations
AnchoredDustBlock.lean 1 declarations
AnchoredJunctionChain.lean 1 declarations
AnnularOuterNonconstant.lean 2 declarations
AnnularRadii.lean 6 declarations
AppendedScalarPairs.lean 3 declarations
AppendingPairData.lean 2 declarations
ApproximateFiniteConcatenation.lean 1 declarations
AssignedStokes.lean 1 declarations
AtomicHitTests.lean 6 declarations
AtomicLevelFiniteness.lean 1 declarations
AtomlessQuantiles.lean 5 declarations
BaireRangeSection.lean 1 declarations
BaireRightInverse.lean 1 declarations
BandContraction.lean 4 declarations
BandGraph.lean 16 declarations
BandStability.lean 6 declarations
BlockCodeInvariants.lean 12 declarations
BoundedJumpRemoval.lean 1 declarations
ChainPotentialBands.lean 2 declarations
ChordTolls.lean 4 declarations
CircuitReparametrization.lean 9 declarations
CodeBarycenterDensities.lean 5 declarations
CodeConstraints.lean 6 declarations
CodeDustMeetingBound.lean 1 declarations
CodePeriodGenericLevels.lean 1 declarations
CodeRealGenericLevels.lean 1 declarations
CodeRealIntersections.lean 1 declarations
CodeRealMeanIntersections.lean 1 declarations
CodeResidualAvoidance.lean 9 declarations
CollapseRelation.lean 1 declarations
CollapsingJunctionChain.lean 1 declarations
CompleteEmbeddingGDelta.lean 1 declarations
ConcatenatedResidualPieces.lean 3 declarations
ConcatenatedTags.lean 4 declarations
ConditionalKoebe.lean 3 declarations
ContinuousMeanIndexWitness.lean 1 declarations
ContinuousRunningMaximum.lean 6 declarations
ContinuousScalarRepresentative.lean 6 declarations
ControlledHeight.lean 3 declarations
ControlledHeightCloseness.lean 1 declarations
CoordinateExclusionTest.lean 6 declarations
CoordinateMapExclusion.lean 1 declarations
CountableConcatenationTolls.lean 4 declarations
CountableConstantPairs.lean 1 declarations
CountableConstantPieces.lean 1 declarations
CountableDeletions.lean 2 declarations
CountableGraphCover.lean 1 declarations
CountableHitTests.lean 2 declarations
CountableLocalFamily.lean 1 declarations
CountableLogarithmicCover.lean 1 declarations
CountableMarks.lean 2 declarations
CountableMeetingBound.lean 1 declarations
CountableMixedStages.lean 1 declarations
CountablePriorRecursion.lean 1 declarations
CountableSetPresentation.lean 1 declarations
CountableSmallRealTests.lean 1 declarations
CountableTagAssembly.lean 6 declarations
CountableUnavailableEndpoints.lean 1 declarations
CountableUnavailableLevelEndpoints.lean 1 declarations
CountableUncoveredSeededEnds.lean 1 declarations
CountableUncoveredTestEnds.lean 2 declarations
CrossingChords.lean 7 declarations
CyclicSelectedSubsequence.lean 1 declarations
DelayedBaseCodes.lean 8 declarations
DelayedSelection.lean 4 declarations
DenseComplementaryDust.lean 1 declarations
DiffuseDustIntersections.lean 2 declarations
DisjointDustContours.lean 1 declarations
DistinctJunctionBlock.lean 1 declarations
DomainMeetingBound.lean 1 declarations
DustBoundDiffuseIntersections.lean 2 declarations
DustCover.lean 1 declarations
DustPriorContacts.lean 5 declarations
DyadicPartition.lean 9 declarations
DyadicTimes.lean 19 declarations
EndCluster.lean 2 declarations
ExactRealSelections.lean 2 declarations
ExclusionTolls.lean 7 declarations
ExpectedWedges.lean 4 declarations
ExtendedAtomicToll.lean 8 declarations
ExteriorDecay.lean 3 declarations
ExteriorZeroAnchor.lean 1 declarations
FarRaySides.lean 2 declarations
FillRegionBands.lean 1 declarations
FillRegionPotential.lean 4 declarations
FiniteAnalyticRounding.lean 1 declarations
FiniteChainPotential.lean 16 declarations
FiniteConvexSplit.lean 1 declarations
FiniteDustCover.lean 1 declarations
FiniteFlagIntersections.lean 6 declarations
FiniteFreeCount.lean 3 declarations
FiniteGapGeometry.lean 1 declarations
FiniteGapIntegration.lean 4 declarations
FiniteGapMultiplicity.lean 2 declarations
FiniteGapTollSum.lean 1 declarations
FiniteGateObstacles.lean 4 declarations
FiniteHitSplit.lean 1 declarations
FiniteHoleSliceAssembly.lean 1 declarations
FiniteJumpFloor.lean 1 declarations
FiniteJumpPattern.lean 3 declarations
FiniteJumpSystems.lean 6 declarations
FiniteJunctionBlock.lean 1 declarations
FiniteLevelAssembly.lean 5 declarations
FiniteLineGaps.lean 10 declarations
FiniteMappedShrink.lean 1 declarations
FiniteMarkedTrapping.lean 5 declarations
FinitePaidConcatenation.lean 1 declarations
FinitePatching.lean 7 declarations
FinitePointAvoidance.lean 1 declarations
FinitePositiveMinimum.lean 1 declarations
FiniteRoundComparison.lean 3 declarations
FiniteSeededRealFamily.lean 4 declarations
FiniteSupBound.lean 1 declarations
FiniteTupleCompatibility.lean 3 declarations
FinitelySuslinian.lean 10 declarations
FirstEntryRange.lean 1 declarations
FirstEntryRestriction.lean 2 declarations
FirstExitCuts.lean 9 declarations
FirstExitFragmentArray.lean 5 declarations
FirstExitFragmentGeometry.lean 4 declarations
FirstExitFragmentProperties.lean 2 declarations
FirstUncountableRecursion.lean 4 declarations
FivePieceSplicing.lean 1 declarations
FixedCircuitExclusion.lean 4 declarations
FixedPatternJumpRemoval.lean 1 declarations
FixedRealExclusion.lean 1 declarations
FlagIntersectionCount.lean 2 declarations
FlattenedHeightError.lean 3 declarations
FourSampleBound.lean 8 declarations
FragmentReindexing.lean 2 declarations
FreeLevelSections.lean 3 declarations
FullDomainPhysicalLift.lean 6 declarations
FullHitSupport.lean 3 declarations
FullSelectedCompatibility.lean 2 declarations
GateForbiddenSet.lean 3 declarations
GatedMeanCoordinateExclusion.lean 1 declarations
GeometricGatePenalty.lean 1 declarations
GeometricIndexLocal.lean 5 declarations
GeometricIndexPeriod.lean 5 declarations
GeometricRayIndex.lean 8 declarations
GoodSample.lean 1 declarations
GradedRealSelection.lean 5 declarations
GraphCylinderCover.lean 1 declarations
GraphGeometricAssembly.lean 1 declarations
GraphHausdorffDomination.lean 2 declarations
HitConfigurations.lean 9 declarations
HorizontalMeanIndexBound.lean 2 declarations
IncreasingChainRelations.lean 3 declarations
IndependentTagLevel.lean 6 declarations
IndexAvoidance.lean 2 declarations
InitialBlockPiece.lean 4 declarations
InnerMeanCoordinateExclusion.lean 1 declarations
JumpBlockCodes.lean 9 declarations
JumpBlockCountBound.lean 5 declarations
JumpChainEdges.lean 3 declarations
JumpLevelRemoval.lean 1 declarations
JumpTollLowerBound.lean 4 declarations
LastEntryCuts.lean 7 declarations
LastEntryFragmentArray.lean 5 declarations
LastEntryFragmentProperties.lean 2 declarations
LevelFlowCoordinate.lean 2 declarations
LiftedMeanBands.lean 5 declarations
LiftedMeanContinuity.lean 5 declarations
LinkedFragmentSelection.lean 1 declarations
LocalBandPaidValues.lean 1 declarations
LocalBandTransitions.lean 3 declarations
LocalCodeMeetingBound.lean 1 declarations
LocalCrossingGeometry.lean 5 declarations
LocalFixedRealExclusion.lean 2 declarations
LocalHeightDifference.lean 4 declarations
LocalHeightFlattening.lean 1 declarations
LocalLiftBands.lean 2 declarations
LocalPlateauContour.lean 1 declarations
LocalizedContinuousCoordinate.lean 1 declarations
LocalizedMeetingUnion.lean 1 declarations
LocalizedPhysicalPlateaus.lean 1 declarations
LocalizedRealStage.lean 1 declarations
LocalizedSmallPerturbation.lean 5 declarations
LogarithmicRectangleCover.lean 2 declarations
LusinInput.lean 7 declarations
MappedGenericLevels.lean 2 declarations
MappedMeanBands.lean 2 declarations
MappedPointAvoidance.lean 1 declarations
MarkedAtomicHitTests.lean 2 declarations
MarkedConfigurations.lean 4 declarations
MarkedEndTrapping.lean 2 declarations
MarkedFiniteHitSplit.lean 1 declarations
MarkedPhysicalBranches.lean 1 declarations
MeanBranchAtlas.lean 1 declarations
MeanBranchBounds.lean 1 declarations
MeanBranchTransitions.lean 2 declarations
MeanCircuitExclusion.lean 2 declarations
MeanCoordinateData.lean 2 declarations
MeanExclusionCongruence.lean 1 declarations
MeanExclusionRadius.lean 6 declarations
MeanExclusionWitness.lean 4 declarations
MeanGeometricIndex.lean 6 declarations
MeanIndexBands.lean 2 declarations
MeanIndexContinuity.lean 3 declarations
MeanIndexHorizontalACL.lean 1 declarations
MeanIndexIntersections.lean 1 declarations
MeanLevelAssembly.lean 1 declarations
MeanMarkedBands.lean 2 declarations
MeanMarkedBranchBands.lean 2 declarations
MeanPeriodCircuit.lean 1 declarations
MeanPeriodCompatibility.lean 1 declarations
MeanPeriodFreeValues.lean 1 declarations
MeanSlicePointwise.lean 2 declarations
MeanVisits.lean 3 declarations
MixedCircuitRetention.lean 1 declarations
MixedCoordinateStage.lean 2 declarations
MixedRealCollapse.lean 1 declarations
MixedRealStage.lean 1 declarations
MixedSequenceRetention.lean 6 declarations
NarrowedResidualBounds.lean 3 declarations
NarrowedTagRules.lean 5 declarations
NarrowedTags.lean 10 declarations
NearExtremalHeight.lean 2 declarations
NearExtremalHeightCloseness.lean 1 declarations
NearMaximalHeightSelection.lean 1 declarations
NewJumpLevel.lean 1 declarations
Nonseparation.lean 2 declarations
OffsetRegions.lean 3 declarations
OrderedHoleIntegration.lean 1 declarations
OrderedProtrusionAvailability.lean 1 declarations
OrderedSelectionSlots.lean 1 declarations
OuterContours.lean 21 declarations
PaidBlockAssembly.lean 1 declarations
PaidChainJumpRemoval.lean 1 declarations
ParallelLineIntegration.lean 5 declarations
PeriodBandGraph.lean 7 declarations
PeriodDomainIntersections.lean 1 declarations
PeriodDomainValues.lean 2 declarations
PerturbedMeanBands.lean 1 declarations
PerturbedMeanPeriodGraph.lean 1 declarations
PhysicalDyadicMonotone.lean 6 declarations
PhysicalExitPenalty.lean 1 declarations
PhysicalMeanIndexHorizontal.lean 1 declarations
PhysicalMeanIndexVertical.lean 1 declarations
PhysicalMeanIndexWitness.lean 1 declarations
PhysicalRawCompatibility.lean 1 declarations
PhysicalRealCodeLevels.lean 1 declarations
PhysicalRealCoordinate.lean 2 declarations
PhysicalSubpaths.lean 10 declarations
PhysicalTerminals.lean 4 declarations
PhysicalTimeSupport.lean 3 declarations
PieceFlowCoordinate.lean 2 declarations
PointDustContourSelection.lean 2 declarations
PointFiberConcentration.lean 4 declarations
PositiveJumpCount.lean 1 declarations
PositiveTollJumpRemoval.lean 1 declarations
PotentialContinuousCoordinate.lean 1 declarations
PotentialPhysicalPlateaus.lean 1 declarations
PreparedHeightSelection.lean 1 declarations
PrependNewBlockJump.lean 5 declarations
PrependOldBlockJump.lean 6 declarations
PrescribedMarkedEnds.lean 1 declarations
PrescribedScalarSeed.lean 6 declarations
PrescribedStokesGeometry.lean 1 declarations
PresentedPriorLevels.lean 1 declarations
PresentedRealCoordinates.lean 2 declarations
PresentedRealSeed.lean 1 declarations
PreterminalTolls.lean 8 declarations
PreterminalVisits.lean 7 declarations
PrincipalExteriorGerm.lean 4 declarations
PrincipalInversionGerm.lean 3 declarations
PrincipalLeadingBounds.lean 3 declarations
PrincipalMobiusIdentity.lean 1 declarations
PrincipalQuadrantGeometry.lean 3 declarations
PrincipalQuadrantMean.lean 1 declarations
PrincipalScalarZeroSet.lean 3 declarations
PriorLevelFamily.lean 4 declarations
PriorRawCompatibility.lean 1 declarations
PriorResidualContacts.lean 1 declarations
PriorityFinite.lean 8 declarations
PriorityInterpolation.lean 6 declarations
PriorityStability.lean 1 declarations
PriorityTermination.lean 5 declarations
ProgressiveJumpSystems.lean 1 declarations
ProjectedLevelTollZero.lean 1 declarations
ProjectionEndFibers.lean 1 declarations
ProtrusionAlternatives.lean 1 declarations
ProtrusionAnchors.lean 2 declarations
ProtrusionGateGeometry.lean 9 declarations
ProtrusionGeometry.lean 4 declarations
ProtrusionMeanExclusion.lean 1 declarations
ProtrusionProjection.lean 7 declarations
ProtrusionTestAvailability.lean 1 declarations
ProtrusionTestGeometry.lean 5 declarations
PublishedAppendingPair.lean 2 declarations
PuncturedHitProduct.lean 3 declarations
RankedDiffuseIntersections.lean 2 declarations
RankedIndependentLevel.lean 3 declarations
RankedRealCodeLevels.lean 5 declarations
RankedRecursiveEndpoints.lean 4 declarations
RankedSelectedLevels.lean 3 declarations
RankedTagPairAvoidance.lean 1 declarations
RankedTupleCompatibility.lean 2 declarations
RankedTuplePairs.lean 2 declarations
RationalSliceCounts.lean 1 declarations
RayIndexCrossings.lean 4 declarations
RayProjection.lean 5 declarations
RaySideConnectivity.lean 5 declarations
RealAnchorRetention.lean 3 declarations
RealBandPaidThreshold.lean 1 declarations
RealBandPaidValues.lean 1 declarations
RealCoordinateData.lean 3 declarations
RealCoordinateFamily.lean 4 declarations
RealCoordinateSubfamily.lean 2 declarations
RealDomainIntersections.lean 3 declarations
RealEndProtrusion.lean 2 declarations
RealExclusionWitness.lean 5 declarations
RealPhysicalRepresentative.lean 1 declarations
RealPreservingBranches.lean 1 declarations
RealSeedPresentation.lean 1 declarations
RealSequenceRetention.lean 4 declarations
RealStageBands.lean 1 declarations
RealStageEstimates.lean 8 declarations
RealTestCoordinateFamily.lean 2 declarations
RealTestLevelData.lean 9 declarations
ReanchorBlockCode.lean 1 declarations
ReanchoredExclusions.lean 5 declarations
ReanchoredSelection.lean 4 declarations
RebasedLevelPresentations.lean 12 declarations
RectangleSliceData.lean 2 declarations
RecursiveEndpointCountability.lean 1 declarations
RecursiveMeanCompatibility.lean 1 declarations
RecursiveMeanExclusion.lean 2 declarations
RecursiveReductionBase.lean 9 declarations
RecursiveReductionBounds.lean 4 declarations
RecursiveTestConstruction.lean 7 declarations
RecursiveTestHistory.lean 5 declarations
RegularAssignedStokes.lean 3 declarations
RegularContours.lean 14 declarations
RegularLevelFlow.lean 3 declarations
RegularLevelFlowOrbit.lean 5 declarations
RegularLevelLeastPeriod.lean 6 declarations
RegularLevelPeriodicParametrization.lean 2 declarations
RegularLevelReturn.lean 2 declarations
RegularMapPieces.lean 4 declarations
RegularPieceFlow.lean 2 declarations
RegularPieceFlowOrbit.lean 5 declarations
RegularPieceLeastPeriod.lean 6 declarations
RegularPiecePeriodicParametrization.lean 1 declarations
RegularPieceReturn.lean 2 declarations
RelevelledExclusions.lean 5 declarations
RelevelledSelection.lean 4 declarations
RescaledBandWitness.lean 5 declarations
ResidualConstraints.lean 8 declarations
ResidualPieceAssembly.lean 7 declarations
ResidualProductAvoidance.lean 1 declarations
ResidualTagAvoidance.lean 1 declarations
ResidualTagContacts.lean 1 declarations
ResidualVisits.lean 9 declarations
RestrictedCoordinateMarks.lean 5 declarations
RestrictedFlattenedSelection.lean 1 declarations
RestrictedMeanExclusion.lean 3 declarations
RestrictedSelectedFamily.lean 1 declarations
ReversedResidualBounds.lean 3 declarations
ReversedRestrictions.lean 2 declarations
ReversedTags.lean 10 declarations
RoundHoleOffsets.lean 1 declarations
SafeDustCover.lean 1 declarations
SaturatedNonseparation.lean 3 declarations
SavedAppendingContours.lean 1 declarations
ScalarBoundedRepresentative.lean 8 declarations
ScalarEndCaps.lean 2 declarations
ScalarEndIdentification.lean 2 declarations
ScalarLocalizedRange.lean 1 declarations
ScalarRegionLowerRange.lean 1 declarations
ScalarRegionRange.lean 1 declarations
ScalarSeedCompatibility.lean 4 declarations
ScalarTerminalRange.lean 4 declarations
ScaledExteriorBounds.lean 2 declarations
ScaledGraphCover.lean 3 declarations
SeededGradedRealSelection.lean 3 declarations
SeededLevelPresentations.lean 4 declarations
SeededMixedSmallness.lean 1 declarations
SeededSmallRealTests.lean 1 declarations
SelectableProtrusionMean.lean 1 declarations
SelectableRealFamily.lean 1 declarations
SelectableRecursiveMean.lean 1 declarations
SelectedCoordinateTest.lean 2 declarations
SelectedExclusionUnion.lean 1 declarations
SelectedHeightError.lean 2 declarations
SelectedLevelPresentation.lean 4 declarations
SelectedMarkedEndEquality.lean 1 declarations
SelectedMixedMeanExclusion.lean 1 declarations
SelectedMixedSelection.lean 1 declarations
SelectedMixedSizedMeanExclusion.lean 1 declarations
SelectedMixedSmallness.lean 4 declarations
SelectedOldError.lean 1 declarations
SelectedOuterMargin.lean 3 declarations
SelectedRadiusLowerBound.lean 2 declarations
SelectedRealCollapse.lean 1 declarations
SelectedRealFamily.lean 1 declarations
SelectedRealSmallness.lean 2 declarations
ShiftedStaircase.lean 14 declarations
ShrinkingDustBlock.lean 1 declarations
ShrinkingFiberCovers.lean 1 declarations
ShrinkingJumpTolls.lean 5 declarations
SignedScalarTests.lean 7 declarations
SignedTestFamily.lean 5 declarations
SingleDustJunction.lean 1 declarations
SinglePieceBlock.lean 4 declarations
SingletonBandCrossing.lean 2 declarations
SizedMeanExclusion.lean 4 declarations
SlackRealExclusion.lean 5 declarations
SmallAnchoredCoordinateFamily.lean 1 declarations
SmallHausdorffCovers.lean 2 declarations
SmallMeanCoordinateConstruction.lean 1 declarations
SortedChordGapAvoidance.lean 2 declarations
SortedCrossingChords.lean 6 declarations
SparseBaseCodes.lean 8 declarations
SparseTags.lean 12 declarations
SquareVisitTolls.lean 3 declarations
Staircase.lean 16 declarations
StaircaseMean.lean 4 declarations
StaircaseWedge.lean 2 declarations
SubfamilyOverride.lean 3 declarations
SubordinateDustCover.lean 1 declarations
SupportedJumpTolls.lean 2 declarations
SymmetricJumpEdges.lean 1 declarations
TagCodeSpace.lean 6 declarations
TagContainment.lean 8 declarations
TagDelay.lean 14 declarations
TagLevelSingleton.lean 2 declarations
TagPairAvoidance.lean 1 declarations
TagValidity.lean 8 declarations
TaggedPhysicalRestriction.lean 5 declarations
TaggedPointContacts.lean 4 declarations
TerminalContainment.lean 1 declarations
TerminalCounts.lean 9 declarations
TerminalRemainder.lean 6 declarations
TorusProjection.lean 1 declarations
TrackedTailSequence.lean 7 declarations
TrackedTestBounds.lean 3 declarations
TrackedTestSequence.lean 7 declarations
TranslatedRayOrder.lean 4 declarations
TranslatedSideNesting.lean 5 declarations
TrueChainConcatenation.lean 1 declarations
TupleExclusions.lean 5 declarations
TuplePairCompatibility.lean 3 declarations
TupleReference.lean 11 declarations
TwoEndedFragmentGeometry.lean 7 declarations
TwoTerminalHitBound.lean 3 declarations
UncountableChoice.lean 3 declarations
UncountableHitTail.lean 2 declarations
UngatedCodes.lean 2 declarations
UnitBandWitness.lean 4 declarations
UnmarkedRealEnds.lean 3 declarations
UpperPairs.lean 7 declarations
VerticalCylinderCover.lean 1 declarations
VerticalRayAvoidance.lean 9 declarations
VerticalRealRetention.lean 1 declarations
VerticalRealSequence.lean 1 declarations
VerticalSliceCounts.lean 2 declarations
VisitCardinality.lean 1 declarations
VisitCounts.lean 16 declarations
WedgeEstimate.lean 3 declarations
WedgeMean.lean 1 declarations
ZeroRealCoordinate.lean 4 declarations