`OAI/NumberTheory/Ostmann/Construction/`

5341 declarations, 0 contain sorry, 0 declared as axioms; 1285 files

Files

ActiveNonbulkCount.lean 4 declarations
ActualAmplitude.lean 11 declarations
ActualEnergySplit.lean 6 declarations
ActualFavorableGiant.lean 1 declarations
ActualHistoryPairExpansion.lean 6 declarations
ActualHistoryPairXi.lean 3 declarations
ActualIntegerTransfer.lean 6 declarations
ActualLocalL2.lean 3 declarations
ActualOffDiagonal.lean 1 declarations
ActualRowExtraction.lean 2 declarations
ActualRows.lean 7 declarations
ActualSmallEndpointBudget.lean 1 declarations
ActualTestBounds.lean 7 declarations
ActualTests.lean 13 declarations
ActualTransfer.lean 2 declarations
AdaptivePivotCoefficients.lean 9 declarations
AdaptivePivotSupport.lean 6 declarations
AllMultipleTupleWeight.lean 6 declarations
AmbientTailGiantEndpoint.lean 1 declarations
AmplifiedRepeatRemoval.lean 2 declarations
AncestorPivotPrecision.lean 8 declarations
ArrangementBoundary.lean 5 declarations
ArrangementBulkComparison.lean 1 declarations
ArrangementProductImage.lean 4 declarations
ArrangementProducts.lean 3 declarations
ArrangementUniformLaw.lean 8 declarations
AssignmentAppend.lean 3 declarations
AssignmentCons.lean 4 declarations
AssignmentExpectations.lean 3 declarations
AssignmentReinsert.lean 5 declarations
AssignmentRestoration.lean 2 declarations
AssignmentSlots.lean 2 declarations
AssignmentSplit.lean 6 declarations
AtomAncestorSources.lean 10 declarations
AtomSourceDescent.lean 10 declarations
AtomTopSupport.lean 8 declarations
BackwardTargets.lean 9 declarations
BadDiagonalNormalization.lean 1 declarations
BadLogCellCount.lean 7 declarations
BadMatchingHarmonicBudget.lean 2 declarations
BadPrimeLogCells.lean 4 declarations
BalancedCellScale.lean 8 declarations
BalancedCenterSelection.lean 4 declarations
BalancedEndpointRate.lean 1 declarations
BalancedHalfInitialAmplitude.lean 1 declarations
BalancedHalfInitialStatistic.lean 1 declarations
BaseFactors.lean 6 declarations
BiasedAffineContradiction.lean 1 declarations
BiasedPrimeBlock.lean 1 declarations
BiasedTailSelection.lean 4 declarations
BinExponential.lean 3 declarations
BinScale.lean 3 declarations
BinnedWordNorm.lean 2 declarations
BoundedWordStatistic.lean 3 declarations
BranchingHistoryIntegrality.lean 3 declarations
BranchingHistoryReplay.lean 16 declarations
BroadBandBalance.lean 3 declarations
CRTCancellation.lean 3 declarations
CRTCharacters.lean 3 declarations
CRTDFT.lean 3 declarations
CRTInterpolation.lean 8 declarations
CRTResidueMean.lean 1 declarations
CRTRow.lean 5 declarations
CanonicalEnumeration.lean 7 declarations
CanonicalFrame.lean 5 declarations
CanonicalHistory.lean 9 declarations
CanonicalHistoryProductChoices.lean 5 declarations
CanonicalHistoryProductChoicesDefs.lean 8 declarations
CanonicalHistoryProductChoicesMass.lean 5 declarations
CanonicalHistoryProductChoicesPair.lean 8 declarations
CanonicalHistoryProductChoicesValues.lean 2 declarations
CanonicalLabels.lean 2 declarations
CanonicalNode.lean 4 declarations
CanonicalOccurrenceTransport.lean 2 declarations
CanonicalOccurrenceTransportCode.lean 18 declarations
CanonicalOccurrenceTransportCoefficients.lean 4 declarations
CanonicalOccurrenceTransportDecodedData.lean 6 declarations
CanonicalOccurrenceTransportKeys.lean 16 declarations
CanonicalOccurrenceTransportNormalized.lean 8 declarations
CanonicalOccurrenceTransportPair.lean 12 declarations
CanonicalOccurrenceTransportPairMaps.lean 7 declarations
CanonicalOccurrenceTransportPairRows.lean 8 declarations
CanonicalOccurrenceTransportPlan.lean 1 declarations
CanonicalOccurrenceTransportRename.lean 8 declarations
CanonicalOccurrenceTransportRows.lean 7 declarations
CanonicalOccurrenceTransportRowsCoefficients.lean 4 declarations
CanonicalOccurrenceTransportRowsDecoded.lean 3 declarations
CanonicalOccurrenceTransportScalar.lean 3 declarations
CanonicalOccurrenceTransportScalarPair.lean 2 declarations
CanonicalOccurrenceTransportScalarRename.lean 10 declarations
CanonicalOccurrenceTransportScalarState.lean 5 declarations
CanonicalOccurrenceTransportScalarTree.lean 1 declarations
CanonicalOccurrenceTransportScalarTreeBasic.lean 7 declarations
CanonicalOccurrenceTransportSources.lean 9 declarations
CanonicalOccurrenceTransportSupport.lean 3 declarations
CanonicalPrimeRecurrence.lean 2 declarations
CanonicalRecurrence.lean 3 declarations
CanonicalSourceLabels.lean 1 declarations
CellRoleBudget.lean 9 declarations
Coefficient.lean 10 declarations
CoefficientRootSupport.lean 2 declarations
CoefficientSupport.lean 4 declarations
CollisionBalancedPrior.lean 3 declarations
CollisionCellChoice.lean 1 declarations
CollisionTestTransfer.lean 5 declarations
CommonAnchorCells.lean 2 declarations
CompensatedAdaptiveCoefficients.lean 4 declarations
CompensatedAdaptiveSupport.lean 5 declarations
CompensationCellSeparation.lean 3 declarations
CompleteTailGiantMean.lean 4 declarations
ComplexCellMeans.lean 3 declarations
ConditionalMain.lean 1 declarations
ConstituentAmplitudeEnergy.lean 5 declarations
ConstituentArithmeticStep.lean 1 declarations
ConstituentAtomProductBounds.lean 1 declarations
ConstituentAtomSupport.lean 3 declarations
ConstituentBlockProducts.lean 5 declarations
ConstituentCharacterCoefficient.lean 3 declarations
ConstituentCharacterCore.lean 3 declarations
ConstituentCopiedAmplitude.lean 2 declarations
ConstituentCopiedAssignment.lean 8 declarations
ConstituentCopiedSupport.lean 3 declarations
ConstituentCopiedWeight.lean 2 declarations
ConstituentCopyEntries.lean 4 declarations
ConstituentCoreEnergy.lean 5 declarations
ConstituentCoreFrequencySupport.lean 1 declarations
ConstituentDiagonal.lean 2 declarations
ConstituentDiagonalMatching.lean 5 declarations
ConstituentDiagonalSupport.lean 6 declarations
ConstituentEnergyMarginal.lean 1 declarations
ConstituentEnergyRate.lean 2 declarations
ConstituentEnergyTransport.lean 4 declarations
ConstituentFamilyEnergy.lean 3 declarations
ConstituentFinalComparison.lean 1 declarations
ConstituentFinalComplexity.lean 3 declarations
ConstituentFinalCostData.lean 3 declarations
ConstituentFinalPair.lean 1 declarations
ConstituentFinalPairBound.lean 1 declarations
ConstituentFinalPairDecay.lean 1 declarations
ConstituentFinalSymmetrization.lean 1 declarations
ConstituentFourierBridge.lean 3 declarations
ConstituentFrequencySupport.lean 2 declarations
ConstituentGuardCost.lean 1 declarations
ConstituentGuardedCopiedAmplitude.lean 1 declarations
ConstituentGuardedNext.lean 2 declarations
ConstituentGuardedProduct.lean 1 declarations
ConstituentHProductLower.lean 2 declarations
ConstituentInitialAmplitude.lean 5 declarations
ConstituentIntervalSupport.lean 2 declarations
ConstituentInvariantCharacter.lean 2 declarations
ConstituentInvariantFourier.lean 1 declarations
ConstituentInvariantPairFactors.lean 3 declarations
ConstituentMatchedCharacter.lean 3 declarations
ConstituentMatchedCostData.lean 4 declarations
ConstituentMatchedFourier.lean 1 declarations
ConstituentMatchedPairDecay.lean 1 declarations
ConstituentMatchedSizeDecay.lean 1 declarations
ConstituentMatchingAverage.lean 1 declarations
ConstituentMatchingEnergy.lean 2 declarations
ConstituentMatchingError.lean 2 declarations
ConstituentMatchingExpansion.lean 4 declarations
ConstituentMatchingPairSum.lean 2 declarations
ConstituentMatchingRate.lean 1 declarations
ConstituentNextSupport.lean 1 declarations
ConstituentOriginalAmplitude.lean 3 declarations
ConstituentOriginalPair.lean 1 declarations
ConstituentPairComplexity.lean 4 declarations
ConstituentPairFactors.lean 11 declarations
ConstituentPairRatio.lean 1 declarations
ConstituentPartitionAssignment.lean 3 declarations
ConstituentPivotEnumeration.lean 4 declarations
ConstituentPrimeFrequencySupport.lean 2 declarations
ConstituentPrimeGuardedAmplitude.lean 3 declarations
ConstituentPriorAssembly.lean 2 declarations
ConstituentPriorBounds.lean 3 declarations
ConstituentRangeCounts.lean 4 declarations
ConstituentReconstructedProduct.lean 1 declarations
ConstituentRootCoefficient.lean 7 declarations
ConstituentScheduleEquiv.lean 4 declarations
ConstituentScheduleMap.lean 6 declarations
ConstituentScheduledEnergy.lean 1 declarations
ConstituentScheduledNext.lean 1 declarations
ConstituentSelectedFinalSymmetrization.lean 1 declarations
ConstituentSelectedProducts.lean 5 declarations
ConstituentSignedOriginalPair.lean 1 declarations
ConstituentSignedPairRatio.lean 1 declarations
ConstituentSignedSupportedPair.lean 1 declarations
ConstituentSupportedFamilyEnergy.lean 2 declarations
ConstituentSupportedMatchingAverage.lean 1 declarations
ConstituentSupportedMatchingEnergy.lean 1 declarations
ConstituentSupportedPairDecay.lean 1 declarations
ConstituentSupportedPairSum.lean 1 declarations
ConstituentSupportedSizeDecay.lean 1 declarations
ConstituentTransferWeight.lean 2 declarations
ConstituentUniqueRootEnergy.lean 6 declarations
ConstituentUnweighted.lean 2 declarations
ConstituentWords.lean 8 declarations
ConstructedBinnedCharacterPriors.lean 1 declarations
ConstructedCharacterCells.lean 5 declarations
ConstructedEndpointCharacterPriors.lean 1 declarations
ConstructedFixedCharacterPriors.lean 1 declarations
ConstructedHistoryGuards.lean 9 declarations
ConstructedInitialAmplitude.lean 1 declarations
ConstructedInitialNongiantPriors.lean 1 declarations
CopiedAmplitudeFubini.lean 2 declarations
CopiedDirectedPhase.lean 3 declarations
CopiedPriorFubini.lean 7 declarations
CopyScheduleSupport.lean 17 declarations
CopyScheduleUnary.lean 3 declarations
CountedRows.lean 6 declarations
CounterpartCutoff.lean 5 declarations
CounterpartNormalization.lean 7 declarations
CounterpartNormalizationBound.lean 5 declarations
CounterpartNormalizationBoundPriors.lean 3 declarations
CounterpartNormalizationBoundProduct.lean 2 declarations
CounterpartNormalizationBoundTemplates.lean 8 declarations
CutoffPoisson.lean 2 declarations
DecompositionAmplitude.lean 3 declarations
Diagonal.lean 10 declarations
DiagonalBadPair.lean 2 declarations
DiagonalBadPairCount.lean 1 declarations
DiagonalBadPairExpansion.lean 2 declarations
DiagonalBadPairExpansionBasic.lean 2 declarations
DiagonalBadPairExpansionSmall.lean 2 declarations
DiagonalBadPairInverse.lean 7 declarations
DiagonalBadPairInversion.lean 6 declarations
DiagonalBadPairInversionComponents.lean 6 declarations
DiagonalBadPairQuadratic.lean 2 declarations
DiagonalBadPairSmall.lean 3 declarations
DiagonalCountBudget.lean 2 declarations
DiagonalCounterpartReindex.lean 3 declarations
DiagonalCounterpartReindexBands.lean 8 declarations
DiagonalCounterpartReindexBijection.lean 7 declarations
DiagonalCounterpartReindexBound.lean 6 declarations
DiagonalCounterpartReindexCoefficient.lean 2 declarations
DiagonalCounterpartReindexCoordinates.lean 14 declarations
DiagonalCounterpartReindexExpansion.lean 3 declarations
DiagonalCounterpartReindexFinal.lean 4 declarations
DiagonalCounterpartReindexFixed.lean 4 declarations
DiagonalCounterpartReindexPairing.lean 2 declarations
DiagonalCounterpartReindexSupport.lean 4 declarations
DiagonalEndpointCancellation.lean 3 declarations
DiagonalEnvironment.lean 3 declarations
DiagonalEnvironmentAverage.lean 2 declarations
DiagonalEnvironmentTerms.lean 4 declarations
DiagonalExternalMeasure.lean 4 declarations
DiagonalFactorialBudget.lean 4 declarations
DiagonalFixedOverhead.lean 6 declarations
DiagonalGapBudget.lean 6 declarations
DiagonalHistoryCovariance.lean 3 declarations
DiagonalHistoryExpansion.lean 5 declarations
DiagonalHistoryXi.lean 3 declarations
DiagonalPermutationCount.lean 7 declarations
DiagonalPermutationCountBasic.lean 11 declarations
DiagonalPermutationCountPositions.lean 12 declarations
DiagonalPermutationCountTotal.lean 4 declarations
DiagonalRegrouping.lean 4 declarations
DiagonalRegroupingActualMatching.lean 3 declarations
DiagonalRegroupingCounterpart.lean 7 declarations
DiagonalRegroupingMatching.lean 9 declarations
DiagonalRegroupingRootCorrection.lean 7 declarations
DiagonalRegularLift.lean 1 declarations
DiagonalRegularMultiplier.lean 4 declarations
DiagonalSingleEnergy.lean 4 declarations
DiagonalSingleHistory.lean 2 declarations
DiagonalSingleHistoryComplex.lean 3 declarations
DiagonalSingleHistoryEnergy.lean 4 declarations
DiagonalTransfer.lean 4 declarations
DiagonalTransform.lean 4 declarations
DiagonalTransformBasic.lean 7 declarations
DiagonalTransformFiber.lean 6 declarations
DiagonalTransformSmall.lean 3 declarations
DiagonalTransformTags.lean 4 declarations
DirectedPhaseQuotient.lean 1 declarations
DirectedPhaseReindex.lean 1 declarations
DirectedPrimePhase.lean 6 declarations
DistinctMomentAverage.lean 2 declarations
DistinctProductError.lean 2 declarations
DistinctTupleProducts.lean 4 declarations
DistinctValueWeights.lean 6 declarations
DoubledWordExpansion.lean 8 declarations
DyadicGraphHistory.lean 1 declarations
DyadicGuardedGraph.lean 1 declarations
DyadicGuardedHistory.lean 1 declarations
DyadicHarmonicBias.lean 7 declarations
DyadicPrimePopulation.lean 1 declarations
DyadicPrimeRange.lean 2 declarations
DyadicPrimeSelection.lean 5 declarations
DyadicShellBudget.lean 2 declarations
DyadicSupportedHistory.lean 4 declarations
DyadicTwoTailContradiction.lean 1 declarations
EarlyDiagonalBudget.lean 2 declarations
EndpointBaseScale.lean 5 declarations
EndpointKernelPairCount.lean 2 declarations
EndpointTestScale.lean 10 declarations
EnumeratedSchedulePhase.lean 4 declarations
EventualTailGiant.lean 1 declarations
ExactGroupScalar.lean 10 declarations
ExactSourceValue.lean 5 declarations
ExpandedHistoryFormula.lean 8 declarations
ExpandedOutsideCoordinates.lean 5 declarations
ExpandedOutsideWords.lean 7 declarations
ExpandedPrimeCount.lean 3 declarations
ExpandedPrimeReplay.lean 5 declarations
ExpandedRangeReplay.lean 3 declarations
ExpandedRangedWeight.lean 4 declarations
ExpandedScheduleCoordinates.lean 10 declarations
ExpandedScheduleHistory.lean 2 declarations
ExpandedScheduleRanges.lean 8 declarations
ExpandedScheduleState.lean 5 declarations
ExpandedScheduleWeight.lean 5 declarations
ExpandedScheduledTemplate.lean 8 declarations
ExpandedUnitReplay.lean 3 declarations
ExpandedWordPairBound.lean 8 declarations
ExponentialSampling.lean 4 declarations
ExternalResidueReduction.lean 6 declarations
ExternalSquareCoordinates.lean 3 declarations
ExternalSquareFibers.lean 3 declarations
FactorialExponential.lean 3 declarations
FavorableBlock.lean 2 declarations
FavorableBlockEndpoint.lean 1 declarations
FavorableBlockScale.lean 6 declarations
FavorableBlockSelection.lean 1 declarations
FavorableGiant.lean 7 declarations
FavorableGiantCutoff.lean 1 declarations
FavorableHalfRows.lean 7 declarations
FavorableInterior.lean 3 declarations
FillerTargetScale.lean 4 declarations
FinalActualPrior.lean 9 declarations
FinalArithmeticContradiction.lean 2 declarations
FinalAsymptoticComparison.lean 1 declarations
FinalEnergyCutoff.lean 1 declarations
FinalExponentialContradiction.lean 1 declarations
FinalFactorialBudget.lean 2 declarations
FinalGraphIdentification.lean 6 declarations
FinalHistoryComparison.lean 1 declarations
FinalHistoryCorrelations.lean 5 declarations
FinalHistoryCount.lean 3 declarations
FinalOneSidedFactor.lean 1 declarations
FinalPairPeriodScale.lean 1 declarations
FinalParityPaths.lean 8 declarations
FinalPermutationComparison.lean 1 declarations
FinalReassignmentInteraction.lean 4 declarations
FinalReassignments.lean 9 declarations
FiniteBiasPopulation.lean 5 declarations
FiniteCRTPoisson.lean 4 declarations
FiniteCellMeans.lean 8 declarations
FiniteCellPrior.lean 10 declarations
FiniteCoordinatePrior.lean 8 declarations
FiniteEmbeddingPrior.lean 7 declarations
FiniteEnumeration.lean 2 declarations
FiniteFormulaRenaming.lean 8 declarations
FiniteFrequencyExpansion.lean 8 declarations
FiniteIntervalPacking.lean 2 declarations
FiniteIntervalPartition.lean 2 declarations
FiniteLogBlockMass.lean 3 declarations
FiniteMatchedFubini.lean 2 declarations
FiniteMatchedPrior.lean 4 declarations
FiniteMatchedSupportedWindow.lean 2 declarations
FiniteMatchedWindow.lean 6 declarations
FinitePairCells.lean 5 declarations
FinitePivotSchedule.lean 3 declarations
FinitePriorComparison.lean 5 declarations
FiniteProductBins.lean 4 declarations
FiniteProductPrior.lean 5 declarations
FiniteReconstructedCoprimality.lean 1 declarations
FiniteScheduledPhase.lean 3 declarations
FiniteScheduledTemplate.lean 10 declarations
FiniteStatistic.lean 10 declarations
FiniteTailSpectators.lean 1 declarations
FiniteTopSupport.lean 1 declarations
FiniteTransfer.lean 7 declarations
FixedBinEndpointRate.lean 1 declarations
FixedCharacterPriors.lean 1 declarations
FixedCharacterTargetCells.lean 5 declarations
FixedInitialCutoffMass.lean 1 declarations
FixedPivotCoefficientPair.lean 1 declarations
FixedPivotCoordinates.lean 12 declarations
FixedPivotEnergyTransport.lean 4 declarations
FixedPivotFormulas.lean 12 declarations
FixedPivotFullPair.lean 1 declarations
FixedPivotGraphEmbedding.lean 5 declarations
FixedPivotHYEnergy.lean 1 declarations
FixedPivotPairSupport.lean 1 declarations
FixedPivotPrimeChecks.lean 2 declarations
FixedPivotPrimeOriginal.lean 1 declarations
FixedPivotPrior.lean 2 declarations
FixedPivotRatioPair.lean 1 declarations
FixedPivotScheduledEnergy.lean 2 declarations
FixedPivotTopConditions.lean 13 declarations
FixedPivotTopSupport.lean 1 declarations
FixedPivotTwoCoordinates.lean 3 declarations
FixedPivotUnitPair.lean 1 declarations
FormulaCoprimality.lean 1 declarations
FormulaHistoryGraphBound.lean 1 declarations
FourierScale.lean 4 declarations
FrozenInitialSmallAmplitude.lean 4 declarations
FrozenInitialSpectatorData.lean 7 declarations
FrozenNonbulkPrior.lean 3 declarations
FrozenOriginalBulk.lean 4 declarations
FrozenPrimeDeletions.lean 4 declarations
FullAtomFourierEnergy.lean 3 declarations
FullAtomProductBounds.lean 1 declarations
FullAtomRangeSupport.lean 3 declarations
FullAtomTransferWeight.lean 7 declarations
FullAtomWeightSupport.lean 3 declarations
FullCopiedWeight.lean 3 declarations
FullHistoryGuards.lean 6 declarations
FullPrimeOriginalPair.lean 1 declarations
FullPrimeRatioPair.lean 1 declarations
FullWeightForcedNode.lean 1 declarations
FullWeightFrequencies.lean 3 declarations
GeneralPeriodicPoisson.lean 2 declarations
GiantBlockError.lean 1 declarations
GiantBlockScales.lean 1 declarations
GiantCellPriorIdentity.lean 4 declarations
GiantCellSelection.lean 1 declarations
GiantCoprimeIntervals.lean 7 declarations
GiantCoprimeRates.lean 3 declarations
GiantCoprimeRemoval.lean 4 declarations
GiantDiscreteTransport.lean 7 declarations
GiantEmpirical.lean 7 declarations
GiantHaarIntegral.lean 2 declarations
GiantLogMeasures.lean 15 declarations
GiantMean.lean 5 declarations
GiantMeanBounds.lean 2 declarations
GiantMeanGap.lean 3 declarations
GiantModulusCutoff.lean 1 declarations
GiantNormalizationReserve.lean 2 declarations
GiantNormalizationReserveBasic.lean 5 declarations
GiantNormalizerSharp.lean 1 declarations
GiantOuterFactors.lean 6 declarations
GiantPhase.lean 13 declarations
GiantPositiveMean.lean 1 declarations
GiantPriorProducer.lean 1 declarations
GiantReciprocalFactor.lean 4 declarations
GiantResidueSumBound.lean 1 declarations
GiantReversalRows.lean 13 declarations
GiantRobustMean.lean 2 declarations
GiantSourceProducer.lean 1 declarations
GiantTransformProduct.lean 3 declarations
GiantWeightedError.lean 3 declarations
GiantWindowScale.lean 6 declarations
GoodCellSelection.lean 4 declarations
GoodCellSums.lean 1 declarations
GoodCellTargets.lean 4 declarations
GoodLogCellBalance.lean 4 declarations
GoodPrimeLogCells.lean 2 declarations
GraphCopySchedule.lean 18 declarations
GroupedCoprimeCoefficient.lean 2 declarations
GroupedFixedPivotPair.lean 1 declarations
GroupedFullCoprime.lean 4 declarations
GroupedFullPair.lean 1 declarations
GroupedPhaseFactorization.lean 2 declarations
GroupedPivotPhase.lean 4 declarations
GroupedPrimePair.lean 1 declarations
GroupedResidueRow.lean 3 declarations
GroupedRows.lean 4 declarations
GroupedScheduleCoefficient.lean 5 declarations
GroupedUnitCoefficient.lean 2 declarations
HalfListBounds.lean 8 declarations
HalfListMean.lean 5 declarations
HalfListStatistic.lean 2 declarations
HalfListTest.lean 15 declarations
HalfPrimeEndpoint.lean 6 declarations
HalfPrimeFactorization.lean 4 declarations
HalfPrimeInitialAmplitude.lean 5 declarations
HalfPrimeStatistic.lean 10 declarations
HalfRows.lean 10 declarations
HalfSupport.lean 3 declarations
HalfTransform.lean 7 declarations
HarmonicBlockRecombination.lean 2 declarations
HarmonicBoxMass.lean 6 declarations
HarmonicFamilyBounds.lean 3 declarations
HarmonicInitialAmplitude.lean 2 declarations
HarmonicInitialStatistic.lean 1 declarations
HarmonicMatchedEnergy.lean 2 declarations
HarmonicPriorAtomDecay.lean 2 declarations
HarmonicPriorCost.lean 2 declarations
HarmonicPriorEvent.lean 2 declarations
HarmonicProductDomination.lean 4 declarations
HarmonicRepeatRemoval.lean 1 declarations
HarmonicRepeatedMass.lean 5 declarations
HarmonicResidueDomination.lean 3 declarations
HarmonicTuplePointBound.lean 2 declarations
HarmonicTupleProductBound.lean 2 declarations
HarmonicUnitPriors.lean 2 declarations
HarmonicWordPriors.lean 10 declarations
History.lean 38 declarations
HistoryCoefficientData.lean 11 declarations
HistoryCoprimalityRemoval.lean 3 declarations
HistoryFactorization.lean 7 declarations
HistoryFormula.lean 12 declarations
HistoryFormulaFourier.lean 7 declarations
HistoryFourierConjugation.lean 4 declarations
HistoryFourierPolynomial.lean 4 declarations
HistoryGiantGuard.lean 4 declarations
HistoryGiantSources.lean 16 declarations
HistoryLineComparison.lean 1 declarations
HistoryPolynomialSpecialization.lean 6 declarations
HistoryRealEvaluation.lean 6 declarations
HistoryReplacementList.lean 8 declarations
HistoryResidueData.lean 4 declarations
HistoryResidueGate.lean 7 declarations
HistorySmoothBound.lean 5 declarations
HistorySmoothFactor.lean 7 declarations
HistorySubstitution.lean 14 declarations
HistorySupportSplit.lean 7 declarations
InfiniteSplitMass.lean 10 declarations
InitialAlphabetCutoff.lean 3 declarations
InitialAmbientPrimeRange.lean 2 declarations
InitialAmplitudeAlphabet.lean 2 declarations
InitialAmplitudeErrorBudget.lean 1 declarations
InitialAmplitudePermutation.lean 5 declarations
InitialAmplitudeReindex.lean 5 declarations
InitialAtomGuards.lean 5 declarations
InitialBalancedCellWeights.lean 2 declarations
InitialCellPriors.lean 8 declarations
InitialCellRoundingBudget.lean 1 declarations
InitialCellSchedule.lean 8 declarations
InitialCellScheduleEquiv.lean 3 declarations
InitialConstituentPoisson.lean 2 declarations
InitialCoordinatesTemplate.lean 14 declarations
InitialCoordinatesTemplateCells.lean 4 declarations
InitialCoordinatesTemplateIndex.lean 14 declarations
InitialCoordinatesTemplateLabels.lean 5 declarations
InitialCoordinatesTemplateState.lean 8 declarations
InitialCutoffProduct.lean 4 declarations
InitialDoubledCutoffProduct.lean 1 declarations
InitialEndpointRate.lean 1 declarations
InitialEtaCRT.lean 1 declarations
InitialEtaCRTBasic.lean 12 declarations
InitialEtaCRTGuard.lean 3 declarations
InitialEtaCRTLeaf.lean 3 declarations
InitialEtaCRTPoisson.lean 2 declarations
InitialEtaCRTSelected.lean 2 declarations
InitialEtaCRTSupport.lean 3 declarations
InitialEtaCRTTransform.lean 4 declarations
InitialEtaConstruction.lean 1 declarations
InitialEtaConstructionActual.lean 1 declarations
InitialEtaConstructionInterface.lean 1 declarations
InitialEtaCoordinates.lean 6 declarations
InitialEtaDefs.lean 16 declarations
InitialEtaExpansion.lean 5 declarations
InitialEtaLower.lean 2 declarations
InitialEtaMinPrime.lean 1 declarations
InitialEtaPeriod.lean 2 declarations
InitialEtaPhysical.lean 15 declarations
InitialEtaPrior.lean 3 declarations
InitialEtaRepeatedCutoff.lean 1 declarations
InitialEtaRepeatedError.lean 1 declarations
InitialEtaRepeatedEstimate.lean 3 declarations
InitialEtaRepeatedPhysical.lean 4 declarations
InitialEtaState.lean 12 declarations
InitialEtaStateIndex.lean 11 declarations
InitialEtaStatePhysical.lean 2 declarations
InitialEtaStatePrior.lean 8 declarations
InitialEtaStateProducts.lean 9 declarations
InitialFrozenAmplitude.lean 5 declarations
InitialGapRate.lean 6 declarations
InitialGaussMultipliers.lean 3 declarations
InitialGroupedWordAmplitude.lean 1 declarations
InitialGuardedExpectation.lean 1 declarations
InitialHalfBulkProduct.lean 2 declarations
InitialHalfListWeights.lean 5 declarations
InitialHalfLogMap.lean 3 declarations
InitialHalfLogSlots.lean 9 declarations
InitialLogGeometry.lean 8 declarations
InitialLogSumBins.lean 5 declarations
InitialLogSumRate.lean 3 declarations
InitialLogSumScale.lean 2 declarations
InitialMixedNormalizer.lean 7 declarations
InitialMovingAmplitude.lean 1 declarations
InitialMovingAverage.lean 8 declarations
InitialMovingBulkLists.lean 3 declarations
InitialMovingBulkTree.lean 5 declarations
InitialMovingCoefficient.lean 2 declarations
InitialMovingCoefficientFactor.lean 3 declarations
InitialMovingCoefficientPair.lean 1 declarations
InitialMovingCutoff.lean 4 declarations
InitialMovingData.lean 7 declarations
InitialMovingEarlyCost.lean 1 declarations
InitialMovingEarlyEnergy.lean 1 declarations
InitialMovingFrequency.lean 1 declarations
InitialMovingHarmonicCost.lean 1 declarations
InitialMovingKernel.lean 1 declarations
InitialMovingLogCorrelation.lean 1 declarations
InitialMovingNorm.lean 3 declarations
InitialMovingOriginalFactor.lean 3 declarations
InitialMovingPrior.lean 3 declarations
InitialMovingRecursiveWeight.lean 1 declarations
InitialMovingSlots.lean 8 declarations
InitialMovingSmallPermutation.lean 4 declarations
InitialMovingSupport.lean 9 declarations
InitialMovingSymmetrizedEnergy.lean 1 declarations
InitialMovingTemplateProduct.lean 5 declarations
InitialMovingTests.lean 6 declarations
InitialMovingTreeWeight.lean 8 declarations
InitialMovingWeight.lean 6 declarations
InitialMovingWindow.lean 2 declarations
InitialNominalGeometry.lean 1 declarations
InitialOutsideTransform.lean 3 declarations
InitialPrimePrior.lean 3 declarations
InitialPrimeWindow.lean 1 declarations
InitialProductSize.lean 1 declarations
InitialProtectedTarget.lean 4 declarations
InitialRepeatRate.lean 1 declarations
InitialRepeatedErrorRate.lean 1 declarations
InitialSampledProductWindow.lean 3 declarations
InitialScheduleRangeAmplitude.lean 1 declarations
InitialScheduleWordAmplitude.lean 1 declarations
InitialScheduledAmplitude.lean 1 declarations
InitialScheduledPrior.lean 3 declarations
InitialSelectedPrior.lean 3 declarations
InitialSmallCellList.lean 3 declarations
InitialSourceChoice.lean 12 declarations
InitialSourceConstruction.lean 1 declarations
InitialSourceFamily.lean 5 declarations
InitialSpectatorFourier.lean 6 declarations
InitialSpectatorProduct.lean 3 declarations
InitialSpectatorSplit.lean 9 declarations
InitialSpectatorWitness.lean 1 declarations
InitialTailEndpoint.lean 1 declarations
InitialTupleFrequencies.lean 2 declarations
InitialWordAtomIntervals.lean 5 declarations
InitialWordBinIdentification.lean 4 declarations
InitialWordCoordinates.lean 12 declarations
InitialWordExpectation.lean 5 declarations
InitialWordLowerBound.lean 1 declarations
InitialWordPriorIntervals.lean 3 declarations
InitialWordRanges.lean 4 declarations
InitialWordSupport.lean 3 declarations
InjectiveCoefficientTransport.lean 6 declarations
InsertedAtomAssignment.lean 5 declarations
InsertedAtomSupport.lean 3 declarations
InsertedConstituentFourier.lean 6 declarations
InsertedConstituentWords.lean 7 declarations
IntegerCellPriors.lean 8 declarations
IntegerCenterSelection.lean 6 declarations
IntegerGridSupport.lean 13 declarations
IntegerIntervalCoordinates.lean 8 declarations
IntegerIntervalDistribution.lean 6 declarations
IntegerPivotExtension.lean 7 declarations
JoinedFrame.lean 2 declarations
JoinedRemaining.lean 5 declarations
LargeCellTargets.lean 1 declarations
LevelZeroFrequencyReserve.lean 5 declarations
LevelZeroFrequencyReserveGrowth.lean 2 declarations
LevelZeroFrequencySupport.lean 3 declarations
LocalSmoothGiantSelection.lean 6 declarations
LogBlocks.lean 7 declarations
LogCellAbel.lean 1 declarations
LogCellBounds.lean 10 declarations
LogCellCalculus.lean 7 declarations
LogCellDefs.lean 4 declarations
LogCellErrorBound.lean 1 declarations
LogCellEvent.lean 1 declarations
LogCellFamilyWindow.lean 6 declarations
LogCellFinitePartition.lean 6 declarations
LogCellLimit.lean 6 declarations
LogCellPNT.lean 3 declarations
LogCellPNTUniform.lean 1 declarations
LogCellPrimePrior.lean 4 declarations
LogCellPrior.lean 7 declarations
LogCellReindex.lean 3 declarations
LogCellSelection.lean 3 declarations
LogCellVariation.lean 1 declarations
LogCellWeightedLimit.lean 3 declarations
LogLogPrimeBandSupport.lean 3 declarations
LogLogPrimeBands.lean 8 declarations
LogWindowDiameter.lean 3 declarations
MaskedPhaseGiantMean.lean 5 declarations
MatchedCellSupport.lean 5 declarations
MatchedDiagonalEnergy.lean 3 declarations
MatchedDirectedPhase.lean 2 declarations
MatchedGraphQuotient.lean 6 declarations
MatchedHarmonicPrior.lean 5 declarations
MatchedRetainedPhase.lean 6 declarations
ModularAdaptiveCoefficients.lean 4 declarations
ModularAdaptiveSupport.lean 5 declarations
ModularCompensatedPrecision.lean 3 declarations
NaturalBadDiagonal.lean 1 declarations
NaturalConstituentEnergy.lean 1 declarations
NaturalFixedPivotEnergy.lean 2 declarations
NestedPrimePrior.lean 2 declarations
NominalCenterSelection.lean 1 declarations
NominalCenterSelectionBasic.lean 8 declarations
NominalCenterSelectionRanges.lean 8 declarations
NominalTotals.lean 12 declarations
NominalTotalsBounds.lean 2 declarations
NominalTotalsError.lean 7 declarations
NominalTotalsScale.lean 3 declarations
NormalizedCRTPoisson.lean 3 declarations
NormalizedSpectatorComparison.lean 2 declarations
OffDiagonalCoprime.lean 3 declarations
OffDiagonalExpectations.lean 5 declarations
OffDiagonalFrequency.lean 1 declarations
OffDiagonalFrequencyBulk.lean 7 declarations
OffDiagonalFrequencyEstimate.lean 6 declarations
OffDiagonalFrequencyWindows.lean 7 declarations
OffDiagonalNode.lean 2 declarations
OffDiagonalPair.lean 2 declarations
OffDiagonalParent.lean 3 declarations
OffDiagonalParentCoprime.lean 3 declarations
OffDiagonalParentFrame.lean 2 declarations
OffDiagonalReindex.lean 4 declarations
OffDiagonalSumExchange.lean 2 declarations
OneSidedCauchy.lean 4 declarations
OneSidedDecayBudget.lean 6 declarations
OppositeBiasTransfer.lean 6 declarations
OriginalAbsoluteBulkBound.lean 1 declarations
OriginalAmplifiedMoment.lean 2 declarations
OriginalAveragedTransfer.lean 2 declarations
OriginalBulkExpectation.lean 4 declarations
OriginalBulkResidues.lean 2 declarations
OriginalCommonCenter.lean 1 declarations
OriginalDirectedTransfer.lean 2 declarations
OriginalEndpointTransfer.lean 5 declarations
OriginalFourierCoefficients.lean 3 declarations
OriginalHarmonicMass.lean 3 declarations
OriginalHarmonicPair.lean 3 declarations
OriginalHarmonicRate.lean 3 declarations
OriginalKernelComparison.lean 1 declarations
OriginalKernelDecomposition.lean 9 declarations
OriginalLargeMoment.lean 1 declarations
OriginalLiftProbability.lean 1 declarations
OriginalLocalScaleBudget.lean 2 declarations
OriginalMomentBudget.lean 3 declarations
OriginalOffWitnessMoment.lean 2 declarations
OriginalOuterMoment.lean 1 declarations
OriginalParameterChoice.lean 7 declarations
OriginalPivotTransfer.lean 4 declarations
OriginalPositiveFirstMoment.lean 4 declarations
OriginalPrimeCellExpansion.lean 3 declarations
OriginalPrimeCellExpectation.lean 4 declarations
OriginalPrimeRestoration.lean 3 declarations
OriginalPriorOneSidedBound.lean 1 declarations
OriginalPriorPeriodicBound.lean 1 declarations
OriginalProductRange.lean 3 declarations
OriginalProductScale.lean 4 declarations
OriginalQuadraticTerm.lean 3 declarations
OriginalSeparatedBulkBound.lean 2 declarations
OriginalSignedFourier.lean 6 declarations
OriginalSmallMoment.lean 1 declarations
OriginalTailCenter.lean 1 declarations
OriginalTupleLifts.lean 5 declarations
OriginalTwoTailContradiction.lean 1 declarations
OriginalWitnessProbability.lean 1 declarations
PairedScheduledHistory.lean 7 declarations
PeriodicPoisson.lean 7 declarations
PhaseGiantCollision.lean 3 declarations
PhaseGiantInitialStatistic.lean 4 declarations
PhaseGiantMean.lean 8 declarations
PhaseGiantTest.lean 15 declarations
PhysicalAmplification.lean 7 declarations
PhysicalAmplificationBudget.lean 2 declarations
PhysicalMomentLower.lean 3 declarations
PivotFrequencyReindex.lean 5 declarations
Poisson.lean 3 declarations
PositiveFourierCutoff.lean 12 declarations
PositiveWordBins.lean 7 declarations
PositiveWordStatistic.lean 4 declarations
PreorderTransferPaths.lean 5 declarations
PrimeAlphabet.lean 4 declarations
PrimeBlockLogBounds.lean 2 declarations
PrimeBulkInsertion.lean 8 declarations
PrimeCellIdealization.lean 4 declarations
PrimeCellMassRate.lean 3 declarations
PrimeCellPartitionConstruction.lean 7 declarations
PrimeCellPriors.lean 6 declarations
PrimeCellProductIntervals.lean 6 declarations
PrimeCellWordPriors.lean 6 declarations
PrimeCutoffFactors.lean 5 declarations
PrimeDiagonalMatching.lean 6 declarations
PrimeExceptionalPoints.lean 2 declarations
PrimeExternalAverage.lean 8 declarations
PrimeExternalLogCoordinates.lean 3 declarations
PrimeExternalPartition.lean 6 declarations
PrimeFamilyEnumeration.lean 12 declarations
PrimeGridResidueLift.lean 3 declarations
PrimeGridSupport.lean 2 declarations
PrimeGroupBins.lean 9 declarations
PrimeGuardedAmplitude.lean 3 declarations
PrimeHarmonicWeightBounds.lean 3 declarations
PrimeLogBlockMass.lean 3 declarations
PrimeLogCellMeans.lean 4 declarations
PrimeLogCellMeasure.lean 6 declarations
PrimeLogCellUpper.lean 4 declarations
PrimeLogGrid.lean 6 declarations
PrimeLogLogIntervalMass.lean 2 declarations
PrimeMaskExtension.lean 5 declarations
PrimeMatchingSupport.lean 9 declarations
PrimeOriginalPair.lean 2 declarations
PrimePairSupport.lean 1 declarations
PrimePhysicalTest.lean 7 declarations
PrimePowerDecayRate.lean 3 declarations
PrimePriorAtoms.lean 4 declarations
PrimePriorDecay.lean 2 declarations
PrimeProductMatching.lean 5 declarations
PrimeProductMoment.lean 3 declarations
PrimeProductNormTransfer.lean 1 declarations
PrimeProductParameterBudget.lean 2 declarations
PrimeProductTranslations.lean 4 declarations
PrimeRestorationDifference.lean 4 declarations
PrimeRichBlock.lean 2 declarations
PrimeShellIndex.lean 4 declarations
PrimeSources.lean 13 declarations
PrimeSubsetCellMixture.lean 2 declarations
PrimeSubsetLogMeasure.lean 5 declarations
PrimeTupleAverages.lean 3 declarations
PrimeTupleDiagonal.lean 4 declarations
PrimeTupleFiber.lean 3 declarations
PrimeTupleSupport.lean 1 declarations
PrimeTupleTranslation.lean 8 declarations
PrimeWordCoefficient.lean 3 declarations
PrimeWordEmbedding.lean 4 declarations
PrimeWordInitialAmplitude.lean 2 declarations
PrimeWordInitialStatistic.lean 2 declarations
PrimeWordPairBound.lean 1 declarations
PrimeWordProduct.lean 2 declarations
RecursiveTransferWeight.lean 9 declarations
RegularDiagonalCancellation.lean 5 declarations
RegularGiantMultiplier.lean 7 declarations
RegularInitialAmplitude.lean 6 declarations
RegularMultiplierNorm.lean 2 declarations
RegularResidueNorm.lean 8 declarations
RemainingDiagonal.lean 9 declarations
RemainingOffDiagonal.lean 4 declarations
RemainingRows.lean 7 declarations
RemainingSupport.lean 5 declarations
ReorderNaturality.lean 2 declarations
ReorderNaturalityIndex.lean 7 declarations
ReorderNaturalityPlan.lean 4 declarations
ReorderNaturalityReinsert.lean 8 declarations
ReorderNaturalityReinsertMap.lean 3 declarations
RepeatFactorBounds.lean 6 declarations
RepeatRemovalAsymptotics.lean 1 declarations
RepeatRemovalBudget.lean 2 declarations
RepeatRemovalPointwise.lean 3 declarations
RepeatedErrorScale.lean 1 declarations
RepeatedErrorScaleAbsorption.lean 1 declarations
RepeatedErrorScaleCombinatorial.lean 2 declarations
RepeatedErrorScalePolynomial.lean 2 declarations
RepeatedLocal.lean 3 declarations
RepeatedMultiplicity.lean 2 declarations
RepeatedPatternPrior.lean 4 declarations
RepeatedPeriod.lean 3 declarations
RepeatedPhysical.lean 3 declarations
RepeatedPhysicalPrior.lean 3 declarations
RepeatedPhysicalTests.lean 13 declarations
RepeatedPivotPhase.lean 4 declarations
RepeatedPrimeGroups.lean 9 declarations
RepeatedPrior.lean 2 declarations
RepeatedPriorBounds.lean 0 declarations
RepeatedPriorBoundsBasic.lean 4 declarations
RepeatedPriorBoundsCandidates.lean 7 declarations
RepeatedPriorBoundsCenters.lean 2 declarations
RepeatedPriorBoundsMass.lean 1 declarations
RepeatedPriorBoundsProduct.lean 3 declarations
RepeatedPriorBoundsScales.lean 2 declarations
RepeatedPriorBoundsUnion.lean 4 declarations
RepeatedTupleEntropy.lean 1 declarations
RepeatedTuplePoisson.lean 4 declarations
RepeatedWeightCounting.lean 5 declarations
ResidueBlockEnergy.lean 1 declarations
RetainedAdditiveMatching.lean 4 declarations
RetainedCharacterGraph.lean 3 declarations
RetainedCharacterPrimeBound.lean 3 declarations
RetainedGraphRatioPair.lean 1 declarations
RetainedGroupedPhase.lean 1 declarations
RetainedInvariantCharacter.lean 2 declarations
RetainedKernelPrimeBound.lean 1 declarations
RetainedPrimeNormalization.lean 2 declarations
RetainedSplitPrimeMass.lean 1 declarations
Reversal.lean 6 declarations
ReverseAtomSources.lean 7 declarations
ReverseCopyCoprime.lean 3 declarations
ReverseCopyMap.lean 6 declarations
RichAnchorCell.lean 1 declarations
RichGridShell.lean 2 declarations
RichPrimeCellTargets.lean 1 declarations
RichSubintervals.lean 5 declarations
RoundedCellTargets.lean 2 declarations
RoundedEnergyCutoffs.lean 3 declarations
RoundedProtectedTarget.lean 1 declarations
RoundedScheduleRanges.lean 1 declarations
RoundedTailScale.lean 1 declarations
RowCongruence.lean 4 declarations
RowDiagonal.lean 5 declarations
SamplePatternCoordinates.lean 10 declarations
SampledPrimeProducts.lean 3 declarations
ScaledPeriodicPoisson.lean 2 declarations
ScaledWordLeaves.lean 9 declarations
ScheduleAtomSystem.lean 9 declarations
ScheduleFullCoprime.lean 3 declarations
ScheduleGraphInvariants.lean 5 declarations
ScheduleInheritedCoprime.lean 1 declarations
SchedulePairwiseReplay.lean 3 declarations
SchedulePivotSlots.lean 7 declarations
SchedulePivotUnary.lean 2 declarations
ScheduleWordSlots.lean 6 declarations
ScheduleWordUnary.lean 2 declarations
ScheduledActiveCharacters.lean 3 declarations
ScheduledAllBulkProducts.lean 5 declarations
ScheduledAmplitude.lean 4 declarations
ScheduledAmplitudeAlphabet.lean 1 declarations
ScheduledAnalyticParameters.lean 4 declarations
ScheduledAnchorDiagonalBound.lean 1 declarations
ScheduledAnchorDiagonalSplit.lean 2 declarations
ScheduledAnchorEnergyBound.lean 1 declarations
ScheduledAnchorGraph.lean 8 declarations
ScheduledAnchorHarmonicBudget.lean 2 declarations
ScheduledAnchorMatchingCount.lean 8 declarations
ScheduledAnchorSymmetry.lean 2 declarations
ScheduledArithmeticIteration.lean 4 declarations
ScheduledArithmeticTransfer.lean 1 declarations
ScheduledBadDiagonalBound.lean 1 declarations
ScheduledBulkMatchingCount.lean 12 declarations
ScheduledCellGap.lean 8 declarations
ScheduledCellIteration.lean 2 declarations
ScheduledCellSteps.lean 7 declarations
ScheduledCoefficientGap.lean 1 declarations
ScheduledComparisonCounts.lean 3 declarations
ScheduledComparisonCutoffs.lean 3 declarations
ScheduledCompensationBounds.lean 1 declarations
ScheduledCopiedAmplitude.lean 3 declarations
ScheduledCopiedSamplePhase.lean 1 declarations
ScheduledCopiedSupport.lean 3 declarations
ScheduledCurrentAmplitude.lean 4 declarations
ScheduledDiagonalDecomposition.lean 1 declarations
ScheduledDiagonalLengths.lean 3 declarations
ScheduledDistinctSources.lean 4 declarations
ScheduledFinalBound.lean 1 declarations
ScheduledFinalComparison.lean 6 declarations
ScheduledFinalContradiction.lean 2 declarations
ScheduledFinalEnergyComparison.lean 1 declarations
ScheduledFinalInteraction.lean 4 declarations
ScheduledFinalPairDecay.lean 1 declarations
ScheduledFinalPairReindex.lean 6 declarations
ScheduledFinalPermutation.lean 10 declarations
ScheduledFinalPrimeComparison.lean 1 declarations
ScheduledFinalPrimeRanges.lean 5 declarations
ScheduledFinalTemplate.lean 3 declarations
ScheduledFourierEnergy.lean 3 declarations
ScheduledFrequencyBounds.lean 5 declarations
ScheduledFrequencyHistory.lean 7 declarations
ScheduledFullFinalPermutation.lean 8 declarations
ScheduledFullMatchingGraph.lean 13 declarations
ScheduledGiantFactorization.lean 3 declarations
ScheduledGiantSeparation.lean 3 declarations
ScheduledGroupedPhase.lean 1 declarations
ScheduledHarmonicNormalization.lean 2 declarations
ScheduledHistoryEmbedding.lean 9 declarations
ScheduledHistoryError.lean 1 declarations
ScheduledInitialPhase.lean 5 declarations
ScheduledInitialWindow.lean 1 declarations
ScheduledInputPhase.lean 5 declarations
ScheduledIntegerRigidity.lean 7 declarations
ScheduledIntervalStep.lean 1 declarations
ScheduledIterationThresholds.lean 1 declarations
ScheduledLeafProducts.lean 5 declarations
ScheduledLiveBounds.lean 3 declarations
ScheduledMatchedCodeSplit.lean 1 declarations
ScheduledMatchedEdges.lean 8 declarations
ScheduledMatchedPairDecay.lean 1 declarations
ScheduledMatchedPrimeRanges.lean 1 declarations
ScheduledMatchingError.lean 2 declarations
ScheduledNodeEquations.lean 3 declarations
ScheduledNodeFrequencies.lean 4 declarations
ScheduledNodeSources.lean 19 declarations
ScheduledNodeUnits.lean 4 declarations
ScheduledNonanchorDecay.lean 1 declarations
ScheduledNonanchorDiagonal.lean 1 declarations
ScheduledNonanchorWitness.lean 2 declarations
ScheduledPageAvoidance.lean 6 declarations
ScheduledPageDeletions.lean 6 declarations
ScheduledPhaseNorm.lean 3 declarations
ScheduledPivotPartition.lean 7 declarations
ScheduledPreorderNodes.lean 8 declarations
ScheduledPrimeCutoffs.lean 2 declarations
ScheduledPrimePhase.lean 4 declarations
ScheduledPrimeRanges.lean 10 declarations
ScheduledPriorFubini.lean 5 declarations
ScheduledRegularUnary.lean 11 declarations
ScheduledRolePrior.lean 6 declarations
ScheduledRootIndex.lean 2 declarations
ScheduledSamplePhase.lean 3 declarations
ScheduledSampleQuotient.lean 3 declarations
ScheduledSampledEnergy.lean 2 declarations
ScheduledSampledValidity.lean 2 declarations
ScheduledSelectedGaps.lean 5 declarations
ScheduledSourceScheme.lean 8 declarations
ScheduledSpectatorComparison.lean 2 declarations
ScheduledSpectatorProducts.lean 1 declarations
ScheduledTemplateBounds.lean 6 declarations
ScheduledTransferGraph.lean 6 declarations
ScheduledTreeBulkCoordinates.lean 12 declarations
ScheduledWordLeafCoordinates.lean 17 declarations
ScheduledWordLeafPrior.lean 2 declarations
ScheduledWordLeafProducts.lean 6 declarations
ScheduledWordTemplate.lean 6 declarations
SelectedAnchorBudget.lean 1 declarations
SelectedAnchorDiagonalBound.lean 1 declarations
SelectedAnchorDiagonalSplit.lean 2 declarations
SelectedAnchorEnergyBound.lean 1 declarations
SelectedAnchorHarmonicBudget.lean 2 declarations
SelectedAnchorMatchingCount.lean 6 declarations
SelectedAnchorNaturalEnergy.lean 1 declarations
SelectedAnchorProductBound.lean 1 declarations
SelectedAnchorSupportedEnergy.lean 1 declarations
SelectedAnchorSymmetry.lean 2 declarations
SelectedBadDiagonalRate.lean 2 declarations
SelectedBulkCoordinates.lean 12 declarations
SelectedBulkPermutation.lean 16 declarations
SelectedBulkSupport.lean 4 declarations
SelectedCellGap.lean 6 declarations
SelectedCellMassRate.lean 2 declarations
SelectedCellSources.lean 14 declarations
SelectedCellTiers.lean 11 declarations
SelectedCompensationCells.lean 4 declarations
SelectedCompensationFrequency.lean 3 declarations
SelectedCompensationPrior.lean 5 declarations
SelectedConstituentWord.lean 7 declarations
SelectedCounterpartBound.lean 4 declarations
SelectedCounterpartFirstSquare.lean 1 declarations
SelectedCounterpartWindows.lean 2 declarations
SelectedCovarianceHistoryXi.lean 6 declarations
SelectedCutoffData.lean 1 declarations
SelectedDiagonalBadBudget.lean 1 declarations
SelectedDiagonalBadEnergy.lean 3 declarations
SelectedDiagonalBadOriginal.lean 2 declarations
SelectedDiagonalBadSquare.lean 3 declarations
SelectedDiagonalBudget.lean 1 declarations
SelectedDiagonalComparisonConsumer.lean 1 declarations
SelectedDiagonalCountBudget.lean 2 declarations
SelectedDiagonalDecay.lean 1 declarations
SelectedDiagonalEnvironment.lean 3 declarations
SelectedDiagonalFirstSquare.lean 3 declarations
SelectedDiagonalGoodAbsorption.lean 1 declarations
SelectedDiagonalGoodEnergy.lean 2 declarations
SelectedDiagonalGoodNormalizer.lean 1 declarations
SelectedDiagonalGoodNormalizerBasic.lean 6 declarations
SelectedDiagonalGoodSum.lean 3 declarations
SelectedDiagonalNormalizer.lean 3 declarations
SelectedDiagonalReduction.lean 1 declarations
SelectedDiagonalSplit.lean 8 declarations
SelectedEndpointGiant.lean 1 declarations
SelectedFinalComparison.lean 4 declarations
SelectedFinalEnergyComparison.lean 1 declarations
SelectedFinalInteraction.lean 6 declarations
SelectedFinalNaturalEnergy.lean 1 declarations
SelectedFinalNaturalPrimeComparison.lean 1 declarations
SelectedFinalPairDecay.lean 1 declarations
SelectedFinalPairReindex.lean 3 declarations
SelectedFinalPermutation.lean 10 declarations
SelectedFinalPrimeComparison.lean 1 declarations
SelectedFrequencySeparation.lean 1 declarations
SelectedFullFinalPermutation.lean 7 declarations
SelectedInitialAlphabet.lean 4 declarations
SelectedInitialAmplitude.lean 1 declarations
SelectedInitialCells.lean 2 declarations
SelectedInitialMovingAmplitude.lean 1 declarations
SelectedInitialPrimeLower.lean 4 declarations
SelectedInitialPriorBounds.lean 2 declarations
SelectedInitialProductWindow.lean 4 declarations
SelectedInitialScheduledAmplitude.lean 1 declarations
SelectedInitialTotal.lean 2 declarations
SelectedInitialUnshiftedCutoff.lean 3 declarations
SelectedInitialWindowRate.lean 2 declarations
SelectedMatchedPairDecay.lean 1 declarations
SelectedNaturalAnchorDecay.lean 1 declarations
SelectedNaturalFinalContradiction.lean 1 declarations
SelectedNodeSources.lean 8 declarations
SelectedNonanchorDecay.lean 1 declarations
SelectedNonanchorDiagonal.lean 1 declarations
SelectedNonanchorProductDecay.lean 1 declarations
SelectedNonanchorProductDiagonal.lean 1 declarations
SelectedNonanchorWitness.lean 3 declarations
SelectedPrimeFubini.lean 12 declarations
SelectedProductBudget.lean 2 declarations
SelectedProductFrequency.lean 3 declarations
SelectedProductSchedule.lean 4 declarations
SelectedRemainingBands.lean 4 declarations
SelectedRemainingBandsMetadata.lean 2 declarations
SelectedSchedulePrimeData.lean 5 declarations
SelectedScheduledCutoffs.lean 2 declarations
SelectedScheduledDiagonal.lean 1 declarations
SelectedScheduledFinalContradiction.lean 1 declarations
SelectedScheduledIteration.lean 1 declarations
SelectedScheduledProduct.lean 8 declarations
SelectedScheduledTransfer.lean 3 declarations
SelectedSmallPrimes.lean 1 declarations
SelectedSourceSupport.lean 3 declarations
SelectedSupportedPairDecay.lean 1 declarations
SelectedTailCells.lean 2 declarations
SelectedTierConstruction.lean 2 declarations
SelectedTransfer.lean 2 declarations
SelectedTransferEventually.lean 1 declarations
SelectedWordReversal.lean 3 declarations
SeparatedMassIntervals.lean 3 declarations
SeparatedMatchingCount.lean 8 declarations
SeparatedPhasePacking.lean 4 declarations
SeparatedPrimeBands.lean 1 declarations
SignedAtomSchedule.lean 4 declarations
SignedBulkGain.lean 5 declarations
SimultaneousTailTests.lean 1 declarations
SmallEndpointBudget.lean 3 declarations
SmallPrimeSubset.lean 5 declarations
SmallPrimeSupply.lean 2 declarations
SmoothCellDeletion.lean 9 declarations
SmoothGiantActiveSupport.lean 2 declarations
SmoothGiantAmbientPrior.lean 3 declarations
SmoothGiantExternalAverage.lean 4 declarations
SmoothGiantIntervalBridge.lean 3 declarations
SmoothGiantLiveSupport.lean 7 declarations
SmoothGiantLossBudget.lean 1 declarations
SmoothGiantMassEstimate.lean 3 declarations
SmoothGiantMixedInterval.lean 3 declarations
SmoothGiantPrior.lean 7 declarations
SmoothGiantSupport.lean 8 declarations
SmoothGiantSupportedTransfer.lean 1 declarations
SmoothGiantTransfer.lean 2 declarations
SmoothHistoryFactor.lean 7 declarations
SmoothLogCellProfile.lean 13 declarations
SmoothMatchedPrior.lean 6 declarations
SmoothMeanDecayRates.lean 2 declarations
SmoothPrimeMeanTest.lean 10 declarations
SmoothedStatistic.lean 4 declarations
SoftPrimeCellSelection.lean 5 declarations
SourceAssignmentSupport.lean 6 declarations
SourceAssignmentSupportCells.lean 4 declarations
SourceAssignmentSupportCenters.lean 2 declarations
SourceAssignmentSupportFrequency.lean 1 declarations
SourceFrequencyBounds.lean 1 declarations
SourceFrequencyBoundsFamily.lean 4 declarations
SourceFrequencyBoundsNumeric.lean 1 declarations
SourcePositive.lean 3 declarations
SourcePriorGridDeletion.lean 3 declarations
SourcePriorGridDeletionBasic.lean 11 declarations
SourcePriorGridDeletionHardCell.lean 3 declarations
SourcePriorGridDeletionMass.lean 6 declarations
SourcePriorGridDeletionMixed.lean 2 declarations
SourcePriorGridDeletionPair.lean 3 declarations
SourcePriors.lean 5 declarations
SourceRangeSeparation.lean 2 declarations
SourceRangeSeparationBasic.lean 4 declarations
SourceRangeSeparationConstruction.lean 1 declarations
SourceRangeSeparationPriors.lean 8 declarations
SourceRangeSeparationScales.lean 1 declarations
SourceWindowCoverage.lean 5 declarations
SpectatorBulkComparison.lean 5 declarations
SpectatorBulkScale.lean 7 declarations
SpectatorNorm.lean 2 declarations
SpectatorProductNorm.lean 5 declarations
SpectatorSmoothNorm.lean 3 declarations
SpectatorWeightFactorization.lean 10 declarations
StablePrimeSelection.lean 3 declarations
StatisticScale.lean 2 declarations
SupportedAlphabetSum.lean 3 declarations
SupportedHalfInitialAmplitude.lean 1 declarations
SupportedInitialLogSum.lean 3 declarations
SupportedPivotTransfer.lean 5 declarations
SupportedPivotTuples.lean 4 declarations
SupportedPrimePrior.lean 5 declarations
SupportedRegularInitialAmplitude.lean 5 declarations
SurvivingSlotCount.lean 5 declarations
TailBandBalance.lean 1 declarations
TailBandCollision.lean 2 declarations
TailBroadPriorBalance.lean 1 declarations
TailBudgetNegligible.lean 2 declarations
TailCellWindow.lean 2 declarations
TailCoordinateTransport.lean 2 declarations
TailCutoffHarmonicMass.lean 2 declarations
TailEndpointTests.lean 2 declarations
TailFourierMass.lean 3 declarations
TailGiantBlockSelection.lean 1 declarations
TailGiantEndpointStatistic.lean 3 declarations
TailGoodPrimeCells.lean 3 declarations
TailInitialBroadPriors.lean 2 declarations
TailMaskCollision.lean 6 declarations
TailPairDeletion.lean 2 declarations
TailPrimeRange.lean 2 declarations
TailSieveMasks.lean 6 declarations
TailSpectatorFamily.lean 4 declarations
TailSpectatorPool.lean 1 declarations
TailSpectatorSupply.lean 2 declarations
TargetPrimeWords.lean 3 declarations
TargetShellLocation.lean 3 declarations
Template.lean 12 declarations
TemplateLabels.lean 5 declarations
TemplateReinsert.lean 4 declarations
TopPrimeSupport.lean 12 declarations
TopWordBinScale.lean 5 declarations
TransferAdditiveProduct.lean 2 declarations
TransferArithmetic.lean 4 declarations
TransferCharacterProduct.lean 2 declarations
TransferCompletePhase.lean 4 declarations
TransferConjugations.lean 8 declarations
TransferCopiedSupport.lean 4 declarations
TransferDirectedPhase.lean 3 declarations
TransferFrequencyRange.lean 5 declarations
TransferFrequencyRigidity.lean 2 declarations
TransferGapRanges.lean 7 declarations
TransferGraph.lean 6 declarations
TransferGraphPhase.lean 6 declarations
TransferGraphRows.lean 4 declarations
TransferHistoryEnergy.lean 2 declarations
TransferHistorySquare.lean 3 declarations
TransferHistoryUniqueness.lean 5 declarations
TransferIntegerPhases.lean 6 declarations
TransferIteration.lean 3 declarations
TransferLocalPhases.lean 13 declarations
TransferOutputSupport.lean 3 declarations
TransferPhaseSupport.lean 3 declarations
TransferRoundedCutoffs.lean 4 declarations
TransferRowProducts.lean 5 declarations
TransferTupleCoordinates.lean 6 declarations
TransferTupleSupport.lean 3 declarations
TransferredPivotSubstitution.lean 8 declarations
TransformExtraction.lean 6 declarations
TransformReversal.lean 4 declarations
TupleFrequencyCutoff.lean 5 declarations
TwoCoordinatePrior.lean 9 declarations
TwoGiantIntegralTransport.lean 1 declarations
TypicalCharacterEndpoints.lean 4 declarations
TypicalCharacterShells.lean 3 declarations
TypicalEndpoints.lean 5 declarations
TypicalTailAssembly.lean 1 declarations
UnbalancedLogMass.lean 4 declarations
UniformConstituentEnergy.lean 1 declarations
UniformFixedPivotHistoryEnergy.lean 1 declarations
UniformInitialAmplitude.lean 1 declarations
UniformSupportedInitialAmplitude.lean 1 declarations
UnitPrimeCellSupport.lean 4 declarations
VariableTransferIteration.lean 2 declarations
WeightEquiv.lean 7 declarations
WeightedPrimeNormalization.lean 2 declarations
WeightedPrimeSelection.lean 3 declarations
WeightedRegularNorm.lean 2 declarations
WeightedRepeatRemoval.lean 5 declarations
WeightedSelection.lean 5 declarations
WeightedWordLeaves.lean 13 declarations
WholePrimeGrid.lean 8 declarations
WholeShellLinearMass.lean 3 declarations
WholeShellMass.lean 1 declarations
WholeShellRetainedLinearMass.lean 1 declarations
WordCellBulkGeometry.lean 7 declarations
WordCharacterRemoval.lean 5 declarations
WordCharacterStatistic.lean 5 declarations
WordCoefficientNorm.lean 3 declarations
WordCopyCoordinates.lean 10 declarations
WordFourierBudgetBounds.lean 4 declarations
WordGraphAmplitude.lean 3 declarations
WordHistoryCoefficient.lean 4 declarations
WordPeriodBudget.lean 2 declarations
WordPrimeBounds.lean 6 declarations
WordPrimeCheckBound.lean 4 declarations
WordPrimeReplay.lean 11 declarations
WordProductWindow.lean 6 declarations
WordRangeBounds.lean 5 declarations
WordRangePolynomial.lean 11 declarations
WordRangeReplay.lean 12 declarations
WordRangeWeight.lean 4 declarations
WordRootRange.lean 6 declarations
WordTransferArrays.lean 9 declarations
WordTransferCoefficient.lean 11 declarations
WordTransferCounts.lean 4 declarations
WordTransferFormulaBounds.lean 2 declarations
WordTransferFourier.lean 6 declarations
WordTransferFullPeriod.lean 10 declarations
WordTransferGuard.lean 7 declarations
WordTransferGuardBounds.lean 5 declarations
WordTransferGuardFamily.lean 10 declarations
WordTransferGuardPolynomial.lean 6 declarations
WordTransferGuardReplay.lean 5 declarations
WordTransferPairBound.lean 1 declarations
WordTransferPeriods.lean 5 declarations
WordTransferReplay.lean 6 declarations
WordTransferTemplate.lean 18 declarations
WordTransferUniformCoefficient.lean 7 declarations
WordTransferWeightIdentity.lean 4 declarations
WordUnitCoefficient.lean 13 declarations
WordUnitPeriod.lean 4 declarations
WordUnitReplay.lean 9 declarations
ZModPoisson.lean 4 declarations