OAI/Analysis/Nonexpansive/
875 declarations, 0 contain sorry, 0 declared as axioms; 86 files
Files
- AdaptiveConvexPrefix.lean 5 declarations
- AdaptiveParentReturn.lean 5 declarations
- AdaptiveRun.lean 2 declarations
- AdaptiveSelection.lean 2 declarations
- Anchor.lean 11 declarations
- AnchorAdaptiveSelection.lean 2 declarations
- Basic.lean 17 declarations
- BlockBefore.lean 13 declarations
- BlockEstimates.lean 4 declarations
- BranchContradiction.lean 2 declarations
- CandidateAncestors.lean 7 declarations
- CandidateDetectors.lean 5 declarations
- CandidateLabels.lean 14 declarations
- CandidateLedger.lean 19 declarations
- CandidateLedgerJoin.lean 26 declarations
- CandidateLevel.lean 17 declarations
- CandidateLevelHistory.lean 23 declarations
- CandidatePredictions.lean 6 declarations
- CandidatePreparation.lean 1 declarations
- CandidateRecords.lean 20 declarations
- CandidateSelection.lean 10 declarations
- CandidateStages.lean 32 declarations
- CandidateThreshold.lean 2 declarations
- CandidateTolerance.lean 4 declarations
- CandidateTreeTolerance.lean 2 declarations
- CommonTerminal.lean 2 declarations
- CompactDetector.lean 2 declarations
- CompactMapSemigroup.lean 7 declarations
- DenseDifferences.lean 4 declarations
- Diametral.lean 10 declarations
- FeasibleBranch.lean 13 declarations
- FinitePrefixEmbedding.lean 6 declarations
- FiniteWitness.lean 3 declarations
- FrontierFromGroups.lean 11 declarations
- FrontierTower.lean 25 declarations
- FunctionalVanishing.lean 2 declarations
- GeneratedMaps.lean 22 declarations
- GlobalCandidateOrdinals.lean 12 declarations
- LedgerPredictionLimits.lean 4 declarations
- ListRunPrefix.lean 5 declarations
- Main.lean 4 declarations
- MinimalInvariant.lean 2 declarations
- Model.lean 3 declarations
- NormalizedContradiction.lean 2 declarations
- OrderedGroupConcat.lean 31 declarations
- OrderedTree.lean 20 declarations
- OrderedTreeIntervals.lean 16 declarations
- OriginalNorm.lean 3 declarations
- ParentReturnHistory.lean 16 declarations
- PointwiseWeakApproximation.lean 6 declarations
- PredictionCompact.lean 24 declarations
- PredictionCutoff.lean 4 declarations
- PredictionOutputs.lean 19 declarations
- PrefixPredictionOutputs.lean 18 declarations
- PrefixPredictionReindex.lean 11 declarations
- Reduction.lean 1 declarations
- Resolvents.lean 17 declarations
- ScalarNormalization.lean 10 declarations
- SeparableInvariant.lean 2 declarations
- SequentialHistory.lean 11 declarations
- SubtreeErrors.lean 6 declarations
- SubtreeEvaluation.lean 14 declarations
- SwitchingBlocks.lean 8 declarations
- SwitchingNorm.lean 5 declarations
- SwitchingScalar.lean 8 declarations
- SwitchingStates.lean 10 declarations
- SwitchingTreeData.lean 8 declarations
- TailMapSemigroup.lean 9 declarations
- TailMaps.lean 22 declarations
- TerminalSequence.lean 9 declarations
- TransmittedSubtreeErrors.lean 14 declarations
- TreeBudget.lean 17 declarations
- TreeEvaluation.lean 16 declarations
- TreeFiniteWitness.lean 7 declarations
- TreeFrontier.lean 15 declarations
- TreeProducer.lean 2 declarations
- TreeTerminal.lean 3 declarations
- TreeTolerance.lean 23 declarations
- WeakBranchIntersection.lean 1 declarations
- WeakCommonTerminal.lean 2 declarations
- WeakCompactness.lean 20 declarations
- WeakMetric.lean 8 declarations
- WeakNestedConvexHull.lean 4 declarations
- WeakSelfMap.lean 22 declarations
- WeightedDeficit.lean 5 declarations
- WeightedTree.lean 18 declarations