`OAI/NumberTheory/Ostmann/Characters/`

5228 declarations, 0 contain sorry, 0 declared as axioms; 1201 files

Files

AdditiveFourier.lean 9 declarations
AffineAction.lean 11 declarations
AffineCoefficients.lean 8 declarations
AffineFibers.lean 6 declarations
AffineFourier.lean 10 declarations
AffineKernelBias.lean 5 declarations
AffineKernelCount.lean 1 declarations
AffineMean.lean 9 declarations
AffineOperator.lean 12 declarations
AllCharacterDecorrelation.lean 7 declarations
AmplifiedCharacterPoisson.lean 5 declarations
AnchorCodes.lean 10 declarations
AnchorDiagonalTotal.lean 3 declarations
AnchorGraphEvolution.lean 6 declarations
AnchorInteraction.lean 2 declarations
AnchorMatchingCount.lean 2 declarations
AnchorNonbulkBudget.lean 4 declarations
AnchorOneSidedEdge.lean 3 declarations
AnchorPairCode.lean 14 declarations
Basic.lean 7 declarations
BinEndpointSelection.lean 1 declarations
BinaryExposure.lean 15 declarations
BinaryExposureLeaves.lean 4 declarations
BinaryExposureTree.lean 5 declarations
BinaryHaar.lean 11 declarations
BinaryPriorExposure.lean 8 declarations
BinaryPriorSum.lean 2 declarations
BinaryPriorSupport.lean 4 declarations
BonamiCube.lean 8 declarations
BonamiInput.lean 4 declarations
BonamiMean.lean 3 declarations
BonamiMonomialFamily.lean 5 declarations
BonamiTensor.lean 4 declarations
BonamiTwoPoint.lean 4 declarations
BottomPairMellin.lean 8 declarations
CRTFourier.lean 6 declarations
CharacterAbsoluteRightBound.lean 1 declarations
CharacterAmbientPrimeBounds.lean 2 declarations
CharacterAnchorCells.lean 12 declarations
CharacterAnchorDecay.lean 2 declarations
CharacterAtomIteration.lean 5 declarations
CharacterBackwardsWords.lean 1 declarations
CharacterBandCutoffs.lean 3 declarations
CharacterBandGeometry.lean 4 declarations
CharacterBandSelection.lean 1 declarations
CharacterBulkSeparation.lean 4 declarations
CharacterCellCovering.lean 4 declarations
CharacterCellIntervals.lean 4 declarations
CharacterComparisonCounts.lean 3 declarations
CharacterCompletedDiskGrowth.lean 1 declarations
CharacterCompletedDivergence.lean 3 declarations
CharacterCompletedFiniteBound.lean 1 declarations
CharacterCompletedFiniteFactors.lean 1 declarations
CharacterCompletedLogDerivative.lean 4 declarations
CharacterCompletedLogGrowth.lean 1 declarations
CharacterCompletedOrderOne.lean 1 declarations
CharacterCompletedRightGrowth.lean 2 declarations
CharacterConcreteBandContradiction.lean 1 declarations
CharacterConstructedCounts.lean 3 declarations
CharacterConstructedEndpointContradiction.lean 1 declarations
CharacterConstructedRanges.lean 6 declarations
CharacterConstructedTargetCutoff.lean 2 declarations
CharacterConstructedTargets.lean 3 declarations
CharacterDepthChoice.lean 3 declarations
CharacterDepthParameters.lean 2 declarations
CharacterDiagonalBudget.lean 2 declarations
CharacterDiagonalDecay.lean 2 declarations
CharacterDiagonalGap.lean 2 declarations
CharacterDiskGrowth.lean 1 declarations
CharacterDiskIndices.lean 5 declarations
CharacterEndpointContradiction.lean 1 declarations
CharacterEnergy.lean 3 declarations
CharacterEnergyPrimeRange.lean 3 declarations
CharacterEnumerationCount.lean 4 declarations
CharacterFaithfulEnumeration.lean 5 declarations
CharacterFinalContradiction.lean 1 declarations
CharacterFinalTop.lean 2 declarations
CharacterFixedParameters.lean 1 declarations
CharacterFourierBudgets.lean 5 declarations
CharacterFourthBound.lean 1 declarations
CharacterFourthMoment.lean 4 declarations
CharacterFullPrimeCells.lean 8 declarations
CharacterFunctionalEquation.lean 10 declarations
CharacterHBounds.lean 3 declarations
CharacterHCoordinates.lean 12 declarations
CharacterHigherBias.lean 7 declarations
CharacterHistoryWeight.lean 5 declarations
CharacterHorizontalGrowth.lean 1 declarations
CharacterIndexCutoff.lean 3 declarations
CharacterInitialAmplitude.lean 1 declarations
CharacterInitialPhase.lean 4 declarations
CharacterInitialProduct.lean 4 declarations
CharacterInitialRate.lean 1 declarations
CharacterIntervalGeometry.lean 2 declarations
CharacterIterationContradiction.lean 1 declarations
CharacterLeftGrowth.lean 1 declarations
CharacterLengthBounds.lean 2 declarations
CharacterLiftCellBounds.lean 3 declarations
CharacterLiteralDiagonal.lean 1 declarations
CharacterLogDerivativeGrowth.lean 1 declarations
CharacterLogDerivativeLeft.lean 1 declarations
CharacterLogDerivativeLocal.lean 2 declarations
CharacterLogDerivativePole.lean 2 declarations
CharacterLogDerivativeRight.lean 1 declarations
CharacterLogDerivativeSeparated.lean 1 declarations
CharacterLogarithmicSeparation.lean 1 declarations
CharacterMaximum.lean 4 declarations
CharacterMeanRotation.lean 6 declarations
CharacterMellinBound.lean 2 declarations
CharacterMellinIntegral.lean 10 declarations
CharacterNonanchorDecay.lean 1 declarations
CharacterNonbulkBudget.lean 3 declarations
CharacterOriginalProductWindow.lean 1 declarations
CharacterPageComparison.lean 4 declarations
CharacterParameterChoice.lean 2 declarations
CharacterPartialSum.lean 5 declarations
CharacterPhaseBounds.lean 3 declarations
CharacterPoisson.lean 5 declarations
CharacterPoissonCutoff.lean 2 declarations
CharacterPositiveMassExclusion.lean 1 declarations
CharacterPrimeCells.lean 5 declarations
CharacterPrimeFrequency.lean 3 declarations
CharacterPrimeMean.lean 6 declarations
CharacterPriorMass.lean 3 declarations
CharacterRepeatRate.lean 2 declarations
CharacterRepeatedTuplesBasic.lean 7 declarations
CharacterRepeatedTuplesBound.lean 2 declarations
CharacterRepeatedTuplesDefs.lean 5 declarations
CharacterRepeatedTuplesPoisson.lean 4 declarations
CharacterRepeatedTuplesPrior.lean 9 declarations
CharacterRepeatedTuplesSeries.lean 2 declarations
CharacterResolventBound.lean 2 declarations
CharacterRightHalfPlane.lean 5 declarations
CharacterRightLogDerivativeBound.lean 1 declarations
CharacterRootNumberBound.lean 1 declarations
CharacterRootNumberUnit.lean 1 declarations
CharacterRoundedEndpoint.lean 7 declarations
CharacterScheduleCounts.lean 3 declarations
CharacterScheduleRoles.lean 22 declarations
CharacterScheduledInitial.lean 1 declarations
CharacterScheduledInitialRate.lean 1 declarations
CharacterSelectedBulk.lean 7 declarations
CharacterSelectedShellGeometry.lean 2 declarations
CharacterSelectionBudget.lean 4 declarations
CharacterSelectionRate.lean 1 declarations
CharacterSelectionScales.lean 5 declarations
CharacterSelfReflection.lean 4 declarations
CharacterSeparatedHeights.lean 1 declarations
CharacterTailShellContradiction.lean 1 declarations
CharacterTargetCellData.lean 7 declarations
CharacterTargetCenters.lean 5 declarations
CharacterTargetCode.lean 9 declarations
CharacterTargetCount.lean 4 declarations
CharacterTargetGaps.lean 3 declarations
CharacterTargetRanges.lean 2 declarations
CharacterTargetSelectionRate.lean 1 declarations
CharacterTargetWords.lean 3 declarations
CharacterTestedShellContradiction.lean 1 declarations
CharacterUniformEndpoint.lean 1 declarations
CharacterUniformIteration.lean 1 declarations
CharacterUnitParseval.lean 2 declarations
CharacterWordAmplitudeLower.lean 1 declarations
CharacterWordBinSelection.lean 1 declarations
CharacterWordGeometry.lean 1 declarations
CharacterWordIntervals.lean 2 declarations
CharacterWordSupport.lean 7 declarations
ConcreteQuartetFourier.lean 7 declarations
ConjugatedPairMeans.lean 6 declarations
CorrelationWeightVariation.lean 3 declarations
CycleAction.lean 7 declarations
CycleCoefficient.lean 1 declarations
CycleMellin.lean 2 declarations
CycleMovingPair.lean 2 declarations
CycleQuartets.lean 10 declarations
CyclicGeneration.lean 2 declarations
DenseAdditiveCoverage.lean 2 declarations
DenseGroupCoverage.lean 7 declarations
DiagonalEstimateActualPairs.lean 3 declarations
DiagonalEstimateAssembly.lean 1 declarations
DiagonalEstimateCancellation.lean 1 declarations
DiagonalEstimateChangingBudget.lean 1 declarations
DiagonalEstimateChangingBudgetBasic.lean 5 declarations
DiagonalEstimateChangingSum.lean 3 declarations
DiagonalEstimateCodeFactorActual.lean 2 declarations
DiagonalEstimateCodeFamily.lean 10 declarations
DiagonalEstimateComplex.lean 5 declarations
DiagonalEstimateCopiedCodes.lean 6 declarations
DiagonalEstimateCopiedCodesActual.lean 3 declarations
DiagonalEstimateCopiedCodesBasic.lean 10 declarations
DiagonalEstimateCopiedCodesCounts.lean 3 declarations
DiagonalEstimateCopiedCodesEdges.lean 3 declarations
DiagonalEstimateCopiedCodesEdgesBasic.lean 8 declarations
DiagonalEstimateCopiedCodesPermutation.lean 8 declarations
DiagonalEstimateCopiedCodesShells.lean 3 declarations
DiagonalEstimateCoreSlices.lean 6 declarations
DiagonalEstimateEnergy.lean 5 declarations
DiagonalEstimateExternal.lean 2 declarations
DiagonalEstimateFiniteRates.lean 3 declarations
DiagonalEstimateFrequencyScales.lean 4 declarations
DiagonalEstimateGapBudget.lean 2 declarations
DiagonalEstimateGapBudgetBasic.lean 5 declarations
DiagonalEstimateGapBudgetScales.lean 2 declarations
DiagonalEstimateHistoryExpansion.lean 3 declarations
DiagonalEstimateHistoryRatio.lean 3 declarations
DiagonalEstimateHistoryRatioBasic.lean 3 declarations
DiagonalEstimateIntegerPrior.lean 6 declarations
DiagonalEstimateIntegerPriorBasic.lean 7 declarations
DiagonalEstimateIntegerPriorProperties.lean 13 declarations
DiagonalEstimateIntegerPriorSource.lean 9 declarations
DiagonalEstimateMarginalScales.lean 2 declarations
DiagonalEstimateMarginalScalesBasic.lean 3 declarations
DiagonalEstimateMass.lean 5 declarations
DiagonalEstimateMatchingPairs.lean 1 declarations
DiagonalEstimateNormalization.lean 6 declarations
DiagonalEstimateNormalizationActual.lean 1 declarations
DiagonalEstimateNormalizationCounts.lean 8 declarations
DiagonalEstimateNormalizationPower.lean 1 declarations
DiagonalEstimatePivotHeight.lean 3 declarations
DiagonalEstimatePivotHeightBasic.lean 4 declarations
DiagonalEstimateRootEnergy.lean 3 declarations
DiagonalEstimateRootPairs.lean 2 declarations
DiagonalEstimateScales.lean 3 declarations
DiagonalEstimateSourceDefs.lean 11 declarations
DiagonalEstimateSourceEnergy.lean 1 declarations
DiagonalEstimateSourceHistory.lean 4 declarations
DiagonalEstimateSourceHistoryZero.lean 3 declarations
DiagonalEstimateSourcePivotCoprime.lean 3 declarations
DiagonalEstimateSourcePreserving.lean 2 declarations
DiagonalEstimateSourceSurvivorSupport.lean 2 declarations
DiagonalEstimateSupportPrimes.lean 3 declarations
DiagonalEstimateSupportRemoval.lean 1 declarations
DiagonalEstimateSupportRemovalCombine.lean 2 declarations
DiagonalEstimateSupportRemovalDefs.lean 5 declarations
DiagonalEstimateSupportRemovalEnd.lean 5 declarations
DiagonalEstimateSupportRemovalEstimate.lean 1 declarations
DiagonalEstimateSupportRemovalKernels.lean 5 declarations
DiagonalEstimateSupportRemovalLiteral.lean 1 declarations
DiagonalEstimateSupportRemovalNumerics.lean 2 declarations
DiagonalEstimateSupportRemovalPhase.lean 3 declarations
DiagonalEstimateSupportRemovalPhaseDefs.lean 6 declarations
DiagonalEstimateSupportRemovalPhaseIdentity.lean 3 declarations
DiagonalEstimateSupportRemovalPhaseNorm.lean 3 declarations
DiagonalEstimateSupportRemovalPrior.lean 8 declarations
DiagonalEstimateSupportRemovalPriorProperties.lean 10 declarations
DiagonalEstimateSupportRemovalStart.lean 4 declarations
DiagonalEstimateSupportRemovalWeights.lean 2 declarations
DiagonalEstimateSupportTags.lean 5 declarations
DiagonalEstimateTotalCount.lean 7 declarations
DiagonalEstimateTotalCountActual.lean 1 declarations
DiagonalEstimateTotalCountBasic.lean 6 declarations
DiagonalEstimateUnitEnergy.lean 1 declarations
DiagonalEstimateUnitFamily.lean 3 declarations
DiagonalEstimateUnitHistory.lean 3 declarations
DiagonalEstimateUnitMatching.lean 4 declarations
DifferenceMoment.lean 5 declarations
DyadicCharacterBudget.lean 3 declarations
FactorialContradiction.lean 3 declarations
FactorialContradictionBounds.lean 9 declarations
FactorialContradictionDecay.lean 6 declarations
FactorialContradictionHilbert.lean 3 declarations
FactorialContradictionRemainders.lean 2 declarations
FactorialContradictionThreshold.lean 3 declarations
FieldPairMoment.lean 8 declarations
FiniteKernelBlocks.lean 7 declarations
FiniteKernelCoordinates.lean 7 declarations
FiniteKernelExclusion.lean 3 declarations
FiniteKernelLinearMaps.lean 7 declarations
FiniteKernelOperator.lean 6 declarations
FiniteKernelPairing.lean 3 declarations
FinitePoissonTransform.lean 4 declarations
FourierGridMargin.lean 1 declarations
FourierWindowDecay.lean 8 declarations
FrequencyExposure.lean 7 declarations
FrequencyExposureLeaves.lean 1 declarations
FrequencyHarmonic.lean 4 declarations
FrequencyTreeSum.lean 11 declarations
GCDReduction.lean 5 declarations
Gauss.lean 3 declarations
GaussFourier.lean 7 declarations
GaussFourthMoment.lean 3 declarations
GcdFrequencyTree.lean 2 declarations
HaarCounting.lean 1 declarations
HarmonicResidueDomination.lean 3 declarations
HeldCycleAverage.lean 5 declarations
HigherBiasCancellationEndpoints.lean 2 declarations
HigherBiasContradictionAssembly.lean 1 declarations
HigherBiasHarmonic.lean 3 declarations
HigherBiasHarmonicAssembly.lean 2 declarations
HigherBiasHarmonicThreshold.lean 4 declarations
HigherBiasHarmonicTransfer.lean 4 declarations
HigherBiasSelection.lean 4 declarations
HigherBiasSource.lean 1 declarations
HigherBiasSourceActualWord.lean 1 declarations
HigherBiasSourceAmplitude.lean 1 declarations
HigherBiasSourceAmplitudeData.lean 9 declarations
HigherBiasSourceBounds.lean 7 declarations
HigherBiasSourceCellSums.lean 1 declarations
HigherBiasSourceCellSumsCover.lean 2 declarations
HigherBiasSourceCellSumsDensity.lean 6 declarations
HigherBiasSourceCellSumsDepth.lean 1 declarations
HigherBiasSourceCellSumsNatural.lean 1 declarations
HigherBiasSourceCellSumsNormalize.lean 3 declarations
HigherBiasSourceCellSumsTargetScales.lean 3 declarations
HigherBiasSourceCellSumsTargets.lean 4 declarations
HigherBiasSourceCells.lean 1 declarations
HigherBiasSourceCellsBounded.lean 10 declarations
HigherBiasSourceCellsFinite.lean 2 declarations
HigherBiasSourceCellsMass.lean 3 declarations
HigherBiasSourceCellsPartition.lean 10 declarations
HigherBiasSourceConfigurationCost.lean 9 declarations
HigherBiasSourceConfigurationRoles.lean 13 declarations
HigherBiasSourceConfigurationRolesCells.lean 9 declarations
HigherBiasSourceConfigurations.lean 2 declarations
HigherBiasSourceConfigurationsFinite.lean 8 declarations
HigherBiasSourceConfigurationsLists.lean 6 declarations
HigherBiasSourceConfigurationsScale.lean 4 declarations
HigherBiasSourceData.lean 7 declarations
HigherBiasSourceFamily.lean 5 declarations
HigherBiasSourceFixedConfiguration.lean 1 declarations
HigherBiasSourceFixedConfigurationCells.lean 3 declarations
HigherBiasSourceFixedConfigurationDefs.lean 6 declarations
HigherBiasSourceFixedConfigurationIdentity.lean 4 declarations
HigherBiasSourceFixedConfigurationPointwise.lean 3 declarations
HigherBiasSourceFrequencyCutoff.lean 1 declarations
HigherBiasSourceGaps.lean 10 declarations
HigherBiasSourceGoodCells.lean 3 declarations
HigherBiasSourceHalfMean.lean 4 declarations
HigherBiasSourceHalfProduct.lean 3 declarations
HigherBiasSourcePrimeSets.lean 14 declarations
HigherBiasSourceRoleBounds.lean 0 declarations
HigherBiasSourceRoleBoundsConfiguration.lean 4 declarations
HigherBiasSourceRoleBoundsGeometry.lean 10 declarations
HigherBiasSourceRoleBoundsNormalization.lean 6 declarations
HigherBiasSourceRoleBoundsPrior.lean 2 declarations
HigherBiasSourceRoleBoundsTargets.lean 3 declarations
HigherBiasSourceScale.lean 7 declarations
HigherBiasSourceScaleCutoff.lean 3 declarations
HigherBiasSourceScaleUniform.lean 2 declarations
HigherBiasSourceSelectedWord.lean 1 declarations
HigherBiasSourceShellSelection.lean 2 declarations
HigherBiasSourceTargetCells.lean 2 declarations
HigherBiasSourceTargetCellsGrid.lean 1 declarations
HigherBiasSourceTargetCellsLocations.lean 5 declarations
HigherBiasSourceTargetsAlgebra.lean 12 declarations
HigherBiasSourceTargetsBounds.lean 3 declarations
HigherBiasSourceTargetsBoundsBasic.lean 10 declarations
HigherBiasSourceTargetsShell.lean 3 declarations
HigherBiasSourceTestShells.lean 10 declarations
HigherBiasSourceTop.lean 4 declarations
HigherBiasSourceTypical.lean 2 declarations
HigherBiasSourceTypicalAlgebra.lean 2 declarations
HigherBiasSourceTypicalMass.lean 1 declarations
HigherBiasSourceTypicalScale.lean 1 declarations
HigherBiasSourceTypicalShells.lean 3 declarations
HigherBiasSourceWord.lean 1 declarations
HigherBiasSourceWordAbsorption.lean 3 declarations
HigherBiasSourceWordBins.lean 2 declarations
HigherBiasSourceWordDefs.lean 7 declarations
HigherBiasSourceWordFinite.lean 2 declarations
HigherBiasSourceWordScale.lean 5 declarations
HigherBiasSourceWordStatistic.lean 12 declarations
HigherBiasValue.lean 6 declarations
HigherCharacterDecorrelation.lean 5 declarations
HistoryArchimedeanVariationBoundary.lean 3 declarations
HistoryArchimedeanVariationChain.lean 2 declarations
HistoryArchimedeanVariationCost.lean 1 declarations
HistoryArchimedeanVariationData.lean 8 declarations
HistoryArchimedeanVariationPiece.lean 2 declarations
HistoryArchimedeanVariationPolynomial.lean 3 declarations
HistoryArchimedeanVariationProduct.lean 10 declarations
HistoryArchimedeanVariationProfiles.lean 9 declarations
HistoryArchimedeanVariationWindow.lean 4 declarations
HistoryFrequencyBudgetAbsorption.lean 1 declarations
HistoryFrequencyBudgetBasic.lean 13 declarations
HistoryFrequencyBudgetCancellation.lean 2 declarations
HistoryFrequencyBudgetEnvelope.lean 4 declarations
HistoryFrequencyBudgetModulus.lean 5 declarations
HistoryFrequencyLabels.lean 6 declarations
HistoryFrequencyLabelsBasic.lean 17 declarations
HistoryFrequencyLabelsBudget.lean 6 declarations
HistoryFrequencyLabelsModulus.lean 13 declarations
HistoryFrequencyLabelsNodes.lean 9 declarations
HistoryReconstruction.lean 11 declarations
HistorySymbolicSupport.lean 6 declarations
HistorySymbolicTrace.lean 13 declarations
HistoryUniqueness.lean 5 declarations
HistoryUniquenessRange.lean 1 declarations
InitialCharacterStatisticBasic.lean 6 declarations
InitialCharacterStatisticDouble.lean 10 declarations
InitialCharacterStatisticExpansion.lean 2 declarations
InitialCharacterStatisticFamily.lean 11 declarations
InitialCharacterStatisticLower.lean 3 declarations
InitialCharacterStatisticProperties.lean 6 declarations
InitialCharacterStatisticRoles.lean 4 declarations
InitialCharacterStatisticScale.lean 2 declarations
InitialCharacterStatisticScaleAbsorption.lean 2 declarations
InitialCharacterStatisticScaleActual.lean 1 declarations
InitialCharacterStatisticScaleBasic.lean 11 declarations
InitialCharacterStatisticScaleCounting.lean 2 declarations
InitialCharacterStatisticScaleError.lean 1 declarations
InitialCharacterStatisticScaleGeometry.lean 1 declarations
InitialCharacterStatisticScalePositive.lean 3 declarations
InitialCharacterStatisticScaleSourceError.lean 3 declarations
IntegerPolynomialBounds.lean 5 declarations
IntervalLifting.lean 1 declarations
LogCutoffPolynomial.lean 5 declarations
Mellin.lean 6 declarations
MellinDiagonal.lean 6 declarations
MellinParseval.lean 5 declarations
MixedBoundedPhaseStatistic.lean 1 declarations
MixedBounds.lean 3 declarations
MixedBulkSymmetrization.lean 3 declarations
MixedExternalAverage.lean 7 declarations
MixedExternalGram.lean 2 declarations
MixedExternalMass.lean 7 declarations
MixedExternalPartition.lean 5 declarations
MixedExternalPermutation.lean 3 declarations
MixedExternalStatistic.lean 5 declarations
MixedExternalSupportedEnergy.lean 1 declarations
MixedFlatnessFinite.lean 2 declarations
MixedFlatnessSpectator.lean 5 declarations
MixedFlatnessSpectatorActual.lean 2 declarations
MixedFlatnessSpectatorBasic.lean 3 declarations
MixedFlatnessSpectatorFacade.lean 1 declarations
MixedFlatnessSpectatorHarmonic.lean 3 declarations
MixedFlatnessSpectatorSelection.lean 5 declarations
MixedFourier.lean 5 declarations
MixedGiantIdealization.lean 1 declarations
MixedIndicator.lean 7 declarations
MixedMaximum.lean 4 declarations
MixedPairHaarRegularity.lean 1 declarations
MixedPairIntegral.lean 1 declarations
MixedPrimeBiasDefs.lean 3 declarations
MixedQuartetBounds.lean 7 declarations
MixedQuartetCoordinates.lean 1 declarations
MonotoneWeightVariation.lean 9 declarations
NormalizedCharacterPoisson.lean 4 declarations
NormalizedFourierProfile.lean 11 declarations
NormalizedMixedFourier.lean 6 declarations
NormalizedResidueFamily.lean 4 declarations
NormalizedResidueIndicator.lean 12 declarations
OneSided.lean 3 declarations
OneSidedBilinear.lean 4 declarations
OneSidedBilinearCauchy.lean 5 declarations
OneSidedBilinearCells.lean 5 declarations
OneSidedBilinearGram.lean 6 declarations
OneSidedBilinearProgressions.lean 7 declarations
OneSidedBilinearRows.lean 4 declarations
OneSidedBounds.lean 4 declarations
OneSidedCharacterBound.lean 3 declarations
OneSidedScaleGap.lean 1 declarations
OneSidedScaleGapAsymptotics.lean 4 declarations
OneSidedScaleGapBilinear.lean 2 declarations
OneSidedScaleGapLong.lean 1 declarations
OneSidedScaleGapMajorant.lean 6 declarations
OneSidedScaleGapNumerics.lean 3 declarations
OneSidedScaleGapRows.lean 2 declarations
OneSidedScaleGapSum.lean 1 declarations
PairedFrequencyProbability.lean 3 declarations
PairedSquareProbability.lean 5 declarations
ParityPermutations.lean 6 declarations
PeriodicCancellation.lean 3 declarations
PeriodicCharacterSum.lean 4 declarations
PeriodicLinearPhase.lean 5 declarations
PeriodicPolynomialCharacterSum.lean 1 declarations
PeriodicPolynomialOneSidedBound.lean 1 declarations
PermutationComparison.lean 2 declarations
PermutedAdditiveCancellation.lean 5 declarations
PhysicalTuplePoisson.lean 3 declarations
PivotArithmeticTransfer.lean 5 declarations
PivotEliminationActual.lean 4 declarations
PivotEliminationActualMaskedRange.lean 1 declarations
PivotEliminationActualSupport.lean 7 declarations
PivotEliminationBasic.lean 3 declarations
PivotEliminationRange.lean 2 declarations
PivotIntegerTransfer.lean 1 declarations
PivotKeyReduction.lean 4 declarations
PivotLossBudget.lean 4 declarations
PivotProductFibers.lean 0 declarations
PivotProductFibersCount.lean 12 declarations
PivotProductFibersMass.lean 6 declarations
PivotProductNormalization.lean 9 declarations
PivotProductNormalizationCells.lean 5 declarations
PivotProductPrior.lean 5 declarations
PivotResidueEquation.lean 2 declarations
PivotResidueGrouping.lean 2 declarations
PivotRowPhase.lean 6 declarations
PivotSquareExpansion.lean 5 declarations
PivotSquareSplit.lean 6 declarations
PivotTargetScale.lean 5 declarations
PolynomialAncestorNonvanishing.lean 3 declarations
PolynomialCellSupports.lean 5 declarations
PolynomialCellVariation.lean 4 declarations
PolynomialCharacterSum.lean 1 declarations
PolynomialCircleEstimate.lean 7 declarations
PolynomialGiantRows.lean 13 declarations
PolynomialGiantTests.lean 10 declarations
PolynomialIntegerCharacterSum.lean 2 declarations
PolynomialKernelCoordinates.lean 4 declarations
PolynomialLineBounds.lean 7 declarations
PolynomialLineFlags.lean 5 declarations
PolynomialOneSidedBound.lean 1 declarations
PolynomialRangeGuards.lean 6 declarations
PolynomialRootCells.lean 8 declarations
PolynomialSupportPartition.lean 10 declarations
PolynomialSupportPartitionCells.lean 9 declarations
PolynomialSupportPartitionSigns.lean 5 declarations
PolynomialSupportPartitionTotal.lean 9 declarations
PolynomialValueBounds.lean 6 declarations
PolynomialVariableSupport.lean 9 declarations
PolynomialWeightPair.lean 11 declarations
PrimeCRTFourier.lean 4 declarations
PrimeCorrelationBounds.lean 2 declarations
PrimeDyadicCover.lean 8 declarations
PrimeDyadicCoverCost.lean 7 declarations
PrimeDyadicCoverSource.lean 8 declarations
PrimeFrequencyExposure.lean 2 declarations
PrimeMomentAsymptotics.lean 1 declarations
PrimeMomentFactors.lean 4 declarations
PrimeResidueCost.lean 3 declarations
PrimeResiduePrior.lean 5 declarations
PrimitiveCharacterEnergy.lean 3 declarations
PrimitiveCharacterLifts.lean 4 declarations
PrimitiveCharacterReduction.lean 7 declarations
PrimitiveCharacterSieve.lean 3 declarations
PrimitiveGaussFourier.lean 2 declarations
PrimitiveLiftReduction.lean 3 declarations
PriorResidueDomination.lean 5 declarations
ProductMellinParseval.lean 4 declarations
ProductPriorSplit.lean 4 declarations
ProductWeightVariation.lean 2 declarations
PublishedBonami.lean 2 declarations
QuadraticClassification.lean 6 declarations
QuartetAllMajorants.lean 4 declarations
QuartetBadCoordinates.lean 9 declarations
QuartetConjugation.lean 4 declarations
QuartetCrossBound.lean 9 declarations
QuartetCutAverages.lean 4 declarations
QuartetCutConjugations.lean 2 declarations
QuartetCycleCoordinates.lean 3 declarations
QuartetCycleMean.lean 2 declarations
QuartetExpansion.lean 5 declarations
QuartetFourier.lean 3 declarations
QuartetFriendlyBound.lean 1 declarations
QuartetFriendlyCoordinates.lean 7 declarations
QuartetFullCoordinates.lean 6 declarations
QuartetHorizontalMean.lean 2 declarations
QuartetIndexCoordinates.lean 11 declarations
QuartetLocalBounds.lean 8 declarations
QuartetMovingAction.lean 11 declarations
QuartetOrientations.lean 7 declarations
QuartetOrientedValue.lean 6 declarations
QuartetOuterAverage.lean 3 declarations
QuartetParseval.lean 8 declarations
QuartetProductCoordinates.lean 4 declarations
QuartetProductFibers.lean 12 declarations
QuartetProductProjection.lean 2 declarations
QuartetProjectedCut.lean 1 declarations
QuartetRatioSwap.lean 2 declarations
QuartetSamePairBound.lean 13 declarations
QuartetSignClassification.lean 1 declarations
QuartetSpectrumBound.lean 4 declarations
QuartetStateBounds.lean 3 declarations
QuartetSymmetry.lean 4 declarations
QuartetTestSymmetries.lean 6 declarations
QuartetTotalMoment.lean 7 declarations
QuartetTreeData.lean 2 declarations
QuartetTreeSmallParameters.lean 4 declarations
RademacherMoments.lean 6 declarations
RatioParseval.lean 5 declarations
RationalHistory.lean 12 declarations
RationalHistoryDegree.lean 2 declarations
RationalHistoryHeight.lean 6 declarations
RationalHistoryVariables.lean 6 declarations
ReciprocalPolynomialFactor.lean 6 declarations
ReciprocalTwist.lean 5 declarations
ReducedCongruence.lean 2 declarations
ReducedFrequencyTree.lean 3 declarations
ReducedSquare.lean 2 declarations
RegularTuplePoisson.lean 6 declarations
RepeatedCharacterCancellation.lean 8 declarations
RepeatedPrimePeriod.lean 7 declarations
RescaledWeightVariation.lean 3 declarations
ResidueDivision.lean 7 declarations
RichShellSelection.lean 1 declarations
RichShellSelectionBlocks.lean 2 declarations
RichShellSelectionDensity.lean 1 declarations
RichShellSelectionFinite.lean 4 declarations
RichShellSelectionMass.lean 8 declarations
RichShellSelectionStarting.lean 1 declarations
RichShellSelectionThree.lean 1 declarations
RichShellSelectionTree.lean 9 declarations
SchwartzWeightVariation.lean 5 declarations
ShellPrior.lean 5 declarations
SignedFrequencySum.lean 3 declarations
SkewKernelSquare.lean 1 declarations
SourceTemplateActualDisjoint.lean 4 declarations
SourceTemplateCharacterLaw.lean 3 declarations
SourceTemplateCopiedData.lean 2 declarations
SourceTemplateDefs.lean 10 declarations
SourceTemplateEligibleData.lean 3 declarations
SourceTemplateIndices.lean 11 declarations
SourceTemplateInitialActual.lean 3 declarations
SourceTemplateInitialFinite.lean 3 declarations
SourceTemplateInitialIntegrand.lean 1 declarations
SourceTemplateInitialPrior.lean 1 declarations
SourceTemplateLeafMask.lean 5 declarations
SourceTemplateListIndices.lean 4 declarations
SourceTemplateNormInputs.lean 8 declarations
SourceTemplatePhase.lean 3 declarations
SourceTemplatePhaseCore.lean 3 declarations
SourceTemplatePhaseDefs.lean 4 declarations
SourceTemplatePhaseSupport.lean 3 declarations
SourceTemplatePrefix.lean 6 declarations
SourceTemplatePrefixData.lean 3 declarations
SourceTemplatePriors.lean 12 declarations
SourceTemplateRoleIndices.lean 9 declarations
SourceTemplateShells.lean 9 declarations
SourceTemplateShellsDisjoint.lean 5 declarations
SourceTemplateState.lean 5 declarations
SourceTemplateTruncation.lean 4 declarations
SourceTemplateWindow.lean 2 declarations
SparseAdditiveKernel.lean 6 declarations
SparseBandMass.lean 3 declarations
SparseCoefficientMajorant.lean 4 declarations
SparseCoefficientSupport.lean 2 declarations
SparseConductorCutoff.lean 7 declarations
SparseCoverageContradiction.lean 2 declarations
SparseExpandedMean.lean 2 declarations
SparseFiniteContraction.lean 2 declarations
SparseIntegerExpansion.lean 2 declarations
SparseKernelEnergy.lean 6 declarations
SparseKernelLocalBlocks.lean 7 declarations
SparseKernelMeans.lean 6 declarations
SparseKernelNumerics.lean 1 declarations
SparseKernelScalar.lean 3 declarations
SparseKernelScalarRange.lean 2 declarations
SparseKernelUnitFactor.lean 4 declarations
SparseMatrixPolynomial.lean 1 declarations
SparseMellinCoefficients.lean 5 declarations
SparseNumericalContradiction.lean 2 declarations
SparsePairEnergyBudget.lean 3 declarations
SparsePairSizeBound.lean 2 declarations
SparsePolydiscBlocks.lean 5 declarations
SparsePolydiscScalar.lean 3 declarations
SparsePrimeFamilyCard.lean 2 declarations
SparsePrimeIdentity.lean 2 declarations
SparsePrimeLowerBound.lean 1 declarations
SparsePrimeMean.lean 2 declarations
SparsePrimitiveExpansion.lean 9 declarations
SparseProductCharacter.lean 5 declarations
SparseResidueMatrix.lean 5 declarations
SparseResidueProjection.lean 1 declarations
SparseScalarNorm.lean 1 declarations
SparseSubsetParameters.lean 2 declarations
SparseTailCoverage.lean 1 declarations
SparseTailMassBound.lean 1 declarations
SparseTailSieveContradiction.lean 1 declarations
SparseTensorKernel.lean 5 declarations
SparseTensorModes.lean 6 declarations
SparseTensorPolynomial.lean 6 declarations
SparseTransformSpectrum.lean 5 declarations
SparseTruncatedOperator.lean 2 declarations
SparseTruncatedWeight.lean 3 declarations
SparseTruncationRate.lean 3 declarations
SparseUnitMassBounds.lean 4 declarations
SparseUnitPolydisc.lean 5 declarations
SparseWeightGrowth.lean 2 declarations
SparseWeightMellinExpansion.lean 2 declarations
SparseWeightPairAverage.lean 4 declarations
SparseWeightUniformBound.lean 5 declarations
SparseWeightUnitMean.lean 3 declarations
SquareAverage.lean 2 declarations
SquareCharacterMass.lean 4 declarations
SquareCongruence.lean 4 declarations
SquareProductMoment.lean 3 declarations
SquarePullback.lean 6 declarations
SquarePullbackNorm.lean 2 declarations
SquareRatioCoefficient.lean 6 declarations
SquarefreeBonami.lean 6 declarations
SquarefreeCoefficientBudget.lean 2 declarations
SubsetTestStability.lean 1 declarations
SymbolicHistory.lean 13 declarations
SymbolicHistoryResidues.lean 5 declarations
TailCharacterBias.lean 6 declarations
TailCharacterRotation.lean 3 declarations
TemplateActualPhasePair.lean 1 declarations
TemplateActualPhasePairRows.lean 4 declarations
TemplateActualPhaseSplit.lean 1 declarations
TemplateActualPivotFactors.lean 6 declarations
TemplateAdaptedCoordinates.lean 8 declarations
TemplateAdaptedProducts.lean 3 declarations
TemplateAdaptedResidues.lean 4 declarations
TemplateAmplitudeIteration.lean 4 declarations
TemplateAmplitudeIterationScales.lean 3 declarations
TemplateAmplitudePrior.lean 1 declarations
TemplateAmplitudePriorBasic.lean 4 declarations
TemplateAmplitudePriorDefs.lean 13 declarations
TemplateAmplitudePriorDisintegration.lean 7 declarations
TemplateAmplitudePriorSources.lean 11 declarations
TemplateAmplitudePriorStates.lean 6 declarations
TemplateAmplitudeRecurrenceActualElimination.lean 1 declarations
TemplateAmplitudeRecurrenceAmplitude.lean 8 declarations
TemplateAmplitudeRecurrenceBounds.lean 2 declarations
TemplateAmplitudeRecurrenceCanonical.lean 5 declarations
TemplateAmplitudeRecurrenceCanonicalPair.lean 1 declarations
TemplateAmplitudeRecurrenceCutoffBasic.lean 2 declarations
TemplateAmplitudeRecurrenceDiagonal.lean 7 declarations
TemplateAmplitudeRecurrenceElimination.lean 1 declarations
TemplateAmplitudeRecurrenceEnergy.lean 6 declarations
TemplateAmplitudeRecurrenceFrequencySum.lean 4 declarations
TemplateAmplitudeRecurrenceFrequencySupport.lean 1 declarations
TemplateAmplitudeRecurrenceLabels.lean 6 declarations
TemplateAmplitudeRecurrenceNodeSupport.lean 6 declarations
TemplateAmplitudeRecurrenceOffDiagonal.lean 1 declarations
TemplateAmplitudeRecurrenceOffDiagonalBounds.lean 1 declarations
TemplateAmplitudeRecurrencePairTerm.lean 2 declarations
TemplateAmplitudeRecurrencePairTermSampleSupported.lean 1 declarations
TemplateAmplitudeRecurrencePairs.lean 2 declarations
TemplateAmplitudeRecurrencePhase.lean 3 declarations
TemplateAmplitudeRecurrencePrimeSize.lean 6 declarations
TemplateAmplitudeRecurrencePrimeSizeBasic.lean 4 declarations
TemplateAmplitudeRecurrencePrimeSizeFrequency.lean 6 declarations
TemplateAmplitudeRecurrencePrimeSupport.lean 5 declarations
TemplateAmplitudeRecurrencePrimeSupportBasic.lean 5 declarations
TemplateAmplitudeRecurrencePrimeSupportSamples.lean 4 declarations
TemplateAmplitudeRecurrenceReindex.lean 3 declarations
TemplateAmplitudeRecurrenceReindexBasic.lean 3 declarations
TemplateAmplitudeRecurrenceReindexPositive.lean 6 declarations
TemplateAmplitudeRecurrenceRetained.lean 7 declarations
TemplateAmplitudeRecurrenceRows.lean 6 declarations
TemplateAmplitudeRecurrenceSamplePair.lean 1 declarations
TemplateAmplitudeRecurrenceSamplePairCore.lean 1 declarations
TemplateAmplitudeRecurrenceSamplePairCoreSample.lean 1 declarations
TemplateAmplitudeRecurrenceSamplePairMaps.lean 3 declarations
TemplateAmplitudeRecurrenceSamplePairSample.lean 1 declarations
TemplateAmplitudeRecurrenceSampleUnits.lean 5 declarations
TemplateAmplitudeRecurrenceScheduledData.lean 8 declarations
TemplateAmplitudeRecurrenceShellPair.lean 1 declarations
TemplateAmplitudeRecurrenceShellSource.lean 3 declarations
TemplateAmplitudeRecurrenceSourceFactorDefs.lean 5 declarations
TemplateAmplitudeRecurrenceSourceFactors.lean 1 declarations
TemplateAmplitudeRecurrenceSourceFactorsSample.lean 1 declarations
TemplateAmplitudeRecurrenceStates.lean 8 declarations
TemplateAmplitudeRecurrenceSupport.lean 6 declarations
TemplateAmplitudeRecurrenceSupportPropagation.lean 2 declarations
TemplateAmplitudeRecurrenceSupportPropagationActual.lean 1 declarations
TemplateAmplitudeRecurrenceSupportPropagationBasic.lean 10 declarations
TemplateAmplitudeRecurrenceSurvivorNorm.lean 3 declarations
TemplateAmplitudeRecurrenceSurvivorNormBasic.lean 2 declarations
TemplateAmplitudeRecurrenceSurvivorRows.lean 1 declarations
TemplateAmplitudeRecurrenceTransfer.lean 1 declarations
TemplateAmplitudeRecurrenceUnitAmplitude.lean 6 declarations
TemplateAmplitudeRecurrenceUnitEnergy.lean 3 declarations
TemplateAmplitudeRecurrenceUnitExpectation.lean 1 declarations
TemplateAmplitudeRecurrenceUnitExtracted.lean 2 declarations
TemplateAmplitudeRecurrenceUnitPairAlgebra.lean 2 declarations
TemplateAmplitudeRecurrenceUnitPairTerm.lean 3 declarations
TemplateAmplitudeRecurrenceUnitSource.lean 4 declarations
TemplateAmplitudeRecurrenceWeight.lean 5 declarations
TemplateAmplitudeRecurrenceWeightReindex.lean 2 declarations
TemplateAmplitudeRecurrenceWeightReindexSupported.lean 1 declarations
TemplateAmplitudeRecurrenceWindowBudget.lean 2 declarations
TemplateAmplitudeRecurrenceWindowBudgetBasic.lean 8 declarations
TemplateAmplitudeRecurrenceWindowBudgetPair.lean 1 declarations
TemplateAmplitudeRecurrenceWindowBudgetScalar.lean 5 declarations
TemplateAmplitudeRecurrenceWindowsActual.lean 6 declarations
TemplateAmplitudeRecurrenceWindowsAtoms.lean 4 declarations
TemplateAmplitudeRecurrenceWindowsBins.lean 5 declarations
TemplateAmplitudeRecurrenceWindowsCells.lean 3 declarations
TemplateAmplitudeRecurrenceWindowsCopied.lean 2 declarations
TemplateAmplitudeRecurrenceWindowsPairCoefficient.lean 2 declarations
TemplateAmplitudeRecurrenceWindowsPivotRange.lean 8 declarations
TemplateAmplitudeRecurrenceWindowsRetained.lean 2 declarations
TemplateAmplitudeRecurrenceWindowsRoles.lean 8 declarations
TemplateAmplitudeRecurrenceWindowsRolesBasic.lean 10 declarations
TemplateAmplitudeRecurrenceWindowsTargets.lean 10 declarations
TemplateAmplitudeSourceUnits.lean 3 declarations
TemplateAmplitudeSourceUnitsDefs.lean 8 declarations
TemplateAmplitudeSourceUnitsNorms.lean 6 declarations
TemplateAmplitudeSourceUnitsSplit.lean 2 declarations
TemplateArithmeticSupport.lean 4 declarations
TemplateBranchPhase.lean 5 declarations
TemplateBranchProducts.lean 6 declarations
TemplateCharacterTransport.lean 4 declarations
TemplateCharacterTransportCore.lean 5 declarations
TemplateChosenPrime.lean 8 declarations
TemplateChosenPrimePrior.lean 1 declarations
TemplateCompositePivotSupport.lean 6 declarations
TemplateCompositePivotSupportActual.lean 4 declarations
TemplateCompositePivotSupportBasic.lean 4 declarations
TemplateCompositePivotSupportFamily.lean 7 declarations
TemplateCompositePivotSupportFamilyActual.lean 1 declarations
TemplateCompositePivotSupportFamilyCore.lean 4 declarations
TemplateCompositePivotSupportFamilyValue.lean 4 declarations
TemplateCompositePivotSupportOrigins.lean 10 declarations
TemplateCompositePivotSupportSampled.lean 3 declarations
TemplateConstituentActions.lean 4 declarations
TemplateConstituentInput.lean 6 declarations
TemplateConstituentNorm.lean 2 declarations
TemplateConstituentNormBasic.lean 4 declarations
TemplateConstituentNormFixed.lean 1 declarations
TemplateConstituentNormFixedBasic.lean 5 declarations
TemplateConstituents.lean 14 declarations
TemplateConstituentsGraph.lean 2 declarations
TemplateConstituentsTransfer.lean 6 declarations
TemplateCore.lean 14 declarations
TemplateDiagonalMatching.lean 4 declarations
TemplateDiagonalMatchingCount.lean 7 declarations
TemplateDiagonalMatchingReindex.lean 3 declarations
TemplateDiagonalMatchingUnary.lean 2 declarations
TemplateDiagonalMatchingWhole.lean 5 declarations
TemplateExposureRealizationCore.lean 4 declarations
TemplateExposureRealizationStep.lean 2 declarations
TemplateFrequencyConstraint.lean 5 declarations
TemplateGraphAnchors.lean 12 declarations
TemplateGraphCodes.lean 2 declarations
TemplateGraphCore.lean 12 declarations
TemplateGraphFibers.lean 4 declarations
TemplateGraphPairs.lean 2 declarations
TemplateGraphRegular.lean 7 declarations
TemplateHistory.lean 13 declarations
TemplateHistoryRangeStep.lean 1 declarations
TemplateHistoryRootNorm.lean 2 declarations
TemplateHistoryRootSum.lean 4 declarations
TemplateHistorySquareSum.lean 2 declarations
TemplateHistoryUnary.lean 3 declarations
TemplateHistoryUnaryBasic.lean 10 declarations
TemplateHistoryUnaryConjugate.lean 1 declarations
TemplateHistoryUnaryConstituent.lean 2 declarations
TemplateHistoryUnaryModulus.lean 4 declarations
TemplateHistoryUnaryNorm.lean 5 declarations
TemplateHistoryUnaryRegular.lean 4 declarations
TemplateHistoryUnaryReindex.lean 5 declarations
TemplateHistoryUnaryTransfer.lean 6 declarations
TemplateHistoryWeightBound.lean 1 declarations
TemplateInitialPhase.lean 3 declarations
TemplateInitialPhaseReindex.lean 1 declarations
TemplateInitialUnary.lean 4 declarations
TemplateInputColumns.lean 2 declarations
TemplateIntegerSupport.lean 4 declarations
TemplateLeafSymbolic.lean 10 declarations
TemplateNormAsymptotic.lean 1 declarations
TemplateNormAsymptoticNormalization.lean 2 declarations
TemplateNormAsymptoticPrecision.lean 3 declarations
TemplateOneSidedBudget.lean 4 declarations
TemplateOneSidedBudgetDegree.lean 3 declarations
TemplateOneSidedBudgetFrequency.lean 6 declarations
TemplateOneSidedBudgetGuards.lean 5 declarations
TemplateOneSidedBudgetHistoryCount.lean 6 declarations
TemplateOneSidedBudgetModulus.lean 5 declarations
TemplateOneSidedBudgetResidues.lean 9 declarations
TemplateOneSidedBudgetSampled.lean 8 declarations
TemplateOneSidedBudgetStructure.lean 7 declarations
TemplateOneSidedBudgetWindows.lean 16 declarations
TemplateOneSidedCancellationBasic.lean 11 declarations
TemplateOneSidedCancellationCanonical.lean 5 declarations
TemplateOneSidedCancellationCoarseWindow.lean 3 declarations
TemplateOneSidedCancellationCompiled.lean 1 declarations
TemplateOneSidedCancellationCompiledBudget.lean 5 declarations
TemplateOneSidedCancellationCore.lean 4 declarations
TemplateOneSidedCancellationCoreData.lean 5 declarations
TemplateOneSidedCancellationCrossData.lean 10 declarations
TemplateOneSidedCancellationDataNorm.lean 2 declarations
TemplateOneSidedCancellationDegree.lean 4 declarations
TemplateOneSidedCancellationEmptyData.lean 1 declarations
TemplateOneSidedCancellationFrequencyGuards.lean 8 declarations
TemplateOneSidedCancellationFrequencySupport.lean 9 declarations
TemplateOneSidedCancellationGatedData.lean 9 declarations
TemplateOneSidedCancellationGuards.lean 9 declarations
TemplateOneSidedCancellationLongData.lean 7 declarations
TemplateOneSidedCancellationNodes.lean 6 declarations
TemplateOneSidedCancellationPrimePriors.lean 1 declarations
TemplateOneSidedCancellationPrimePriorsBasic.lean 4 declarations
TemplateOneSidedCancellationPrimePriorsGrid.lean 2 declarations
TemplateOneSidedCancellationPrimePriorsGridDefs.lean 2 declarations
TemplateOneSidedCancellationPrimePriorsRows.lean 1 declarations
TemplateOneSidedCancellationProfileBudget.lean 1 declarations
TemplateOneSidedCancellationProfileBudgetBasic.lean 5 declarations
TemplateOneSidedCancellationProfiles.lean 5 declarations
TemplateOneSidedCancellationRatioBudget.lean 1 declarations
TemplateOneSidedCancellationRatioData.lean 3 declarations
TemplateOneSidedCancellationResidueRows.lean 5 declarations
TemplateOneSidedCancellationResidueValidity.lean 6 declarations
TemplateOneSidedCancellationResidues.lean 11 declarations
TemplateOneSidedCancellationSampled.lean 5 declarations
TemplateOneSidedCancellationSourceBins.lean 5 declarations
TemplateOneSidedCancellationSourceBudget.lean 4 declarations
TemplateOneSidedCancellationSourceBudgetSplitWidth.lean 4 declarations
TemplateOneSidedCancellationSourceCore.lean 1 declarations
TemplateOneSidedCancellationSourceData.lean 3 declarations
TemplateOneSidedCancellationSourceDataSplitWidth.lean 3 declarations
TemplateOneSidedCancellationSourceHeights.lean 3 declarations
TemplateOneSidedCancellationSourceNormalizedData.lean 4 declarations
TemplateOneSidedCancellationSourcePairActual.lean 2 declarations
TemplateOneSidedCancellationSourcePairData.lean 4 declarations
TemplateOneSidedCancellationSourceRows.lean 3 declarations
TemplateOneSidedCancellationSourceRowsBasic.lean 6 declarations
TemplateOneSidedCancellationSourceRowsPair.lean 4 declarations
TemplateOneSidedCancellationSourceRowsSplitWidth.lean 3 declarations
TemplateOneSidedCancellationSourceRowsSplitWidthWeight.lean 2 declarations
TemplateOneSidedCancellationSourceRowsWeight.lean 2 declarations
TemplateOneSidedCancellationSubstitution.lean 13 declarations
TemplateOneSidedCancellationSurvivingData.lean 3 declarations
TemplateOneSidedCancellationSurvivingExpressions.lean 11 declarations
TemplateOneSidedCancellationSurvivingExpressionsBasic.lean 10 declarations
TemplateOneSidedCancellationSurvivingExpressionsSource.lean 7 declarations
TemplateOneSidedCancellationSurvivingModulus.lean 10 declarations
TemplateOneSidedCancellationSurvivingModulusBasic.lean 12 declarations
TemplateOneSidedCancellationSurvivingModulusBudget.lean 5 declarations
TemplateOneSidedCancellationSurvivingPrimeBound.lean 1 declarations
TemplateOneSidedCancellationSurvivingProfiles.lean 4 declarations
TemplateOneSidedCancellationSurvivingSlice.lean 3 declarations
TemplateOneSidedCancellationTerminalActual.lean 1 declarations
TemplateOneSidedCancellationTerminalData.lean 2 declarations
TemplateOneSidedCancellationTerminalDataBasic.lean 5 declarations
TemplateOneSidedCancellationTerminalDataBudget.lean 2 declarations
TemplateOneSidedCancellationTerminalDataModulus.lean 4 declarations
TemplateOneSidedCancellationTerminalDataSource.lean 2 declarations
TemplateOneSidedCancellationTerminalError.lean 1 declarations
TemplateOneSidedCancellationTerminalPrimeBound.lean 1 declarations
TemplateOneSidedCancellationTerminalSourceBound.lean 1 declarations
TemplateOneSidedCancellationTerminalSourceCore.lean 3 declarations
TemplateOneSidedCancellationTerminalSourceDefs.lean 3 declarations
TemplateOneSidedCancellationTerminalSourceMean.lean 1 declarations
TemplateOneSidedCancellationVariation.lean 3 declarations
TemplateOneSidedCanonicalGuardsCore.lean 3 declarations
TemplateOneSidedCanonicalGuardsCount.lean 6 declarations
TemplateOneSidedCanonicalGuardsGood.lean 5 declarations
TemplateOneSidedCanonicalGuardsLeaf.lean 7 declarations
TemplateOneSidedCanonicalGuardsPivot.lean 6 declarations
TemplateOneSidedCanonicalGuardsSize.lean 4 declarations
TemplateOneSidedCanonicalGuardsSplitWidth.lean 5 declarations
TemplateOneSidedCanonicalGuardsWeight.lean 3 declarations
TemplateOneSidedLeafProfiles.lean 4 declarations
TemplateOneSidedLeafProfilesBasic.lean 6 declarations
TemplateOneSidedLeafProfilesGuards.lean 6 declarations
TemplateOneSidedNumericInputs.lean 2 declarations
TemplateOneSidedNumericInputsAtoms.lean 4 declarations
TemplateOneSidedNumericInputsGrowth.lean 8 declarations
TemplateOneSidedNumericInputsRows.lean 5 declarations
TemplateOneSidedPairwise.lean 9 declarations
TemplateOneSidedPairwiseActual.lean 9 declarations
TemplateOneSidedPairwiseSource.lean 4 declarations
TemplateOneSidedPhase.lean 0 declarations
TemplateOneSidedPhaseAction.lean 10 declarations
TemplateOneSidedPhaseActual.lean 7 declarations
TemplateOneSidedPhaseMatching.lean 4 declarations
TemplateOneSidedPhaseMatchingGraph.lean 10 declarations
TemplateOneSidedPhasePrefix.lean 8 declarations
TemplateOneSidedPhasePrefixMatching.lean 8 declarations
TemplateOneSidedPhasePrefixSource.lean 2 declarations
TemplateOneSidedPhasePriorJoin.lean 1 declarations
TemplateOneSidedPhasePriorJoinActual.lean 2 declarations
TemplateOneSidedPhasePriorJoinBoundedRows.lean 5 declarations
TemplateOneSidedPhasePriorJoinData.lean 4 declarations
TemplateOneSidedPhasePriorJoinEdge.lean 1 declarations
TemplateOneSidedPhasePriorJoinExtension.lean 1 declarations
TemplateOneSidedPhasePriorJoinFullDefs.lean 6 declarations
TemplateOneSidedPhasePriorJoinFullDisintegration.lean 3 declarations
TemplateOneSidedPhasePriorJoinFullDisintegrationBasic.lean 3 declarations
TemplateOneSidedPhasePriorJoinFullDisintegrationSum.lean 1 declarations
TemplateOneSidedPhasePriorJoinFullSourceDefs.lean 5 declarations
TemplateOneSidedPhasePriorJoinFullSupport.lean 2 declarations
TemplateOneSidedPhasePriorJoinMasks.lean 7 declarations
TemplateOneSidedPhasePriorJoinMean.lean 1 declarations
TemplateOneSidedPhasePriorJoinMembership.lean 4 declarations
TemplateOneSidedPhasePriorJoinNorm.lean 2 declarations
TemplateOneSidedPhasePriorJoinPointwise.lean 3 declarations
TemplateOneSidedPhasePriorJoinRows.lean 6 declarations
TemplateOneSidedPhasePriorJoinRowsBasic.lean 4 declarations
TemplateOneSidedPhasePriorJoinRowsExtension.lean 4 declarations
TemplateOneSidedPhasePriorJoinSample.lean 5 declarations
TemplateOneSidedPhasePriorJoinSourceMembership.lean 2 declarations
TemplateOneSidedPhasePriorJoinSourceNorm.lean 3 declarations
TemplateOneSidedPhasePriorJoinSourceRows.lean 2 declarations
TemplateOneSidedPhasePriorJoinSourceSelectedNorm.lean 2 declarations
TemplateOneSidedPhasePriorJoinSourceSelectedNormBasic.lean 3 declarations
TemplateOneSidedPhasePriorJoinSourceSelectedNormEventual.lean 1 declarations
TemplateOneSidedPhaseQuotient.lean 4 declarations
TemplateOneSidedPhaseSplit.lean 6 declarations
TemplateOneSidedPhaseSplitBasic.lean 11 declarations
TemplateOneSidedPhaseSplitNorm.lean 4 declarations
TemplateOneSidedPhaseSurviving.lean 1 declarations
TemplateOneSidedPhaseSurvivingAction.lean 6 declarations
TemplateOneSidedPhaseSurvivingBasic.lean 1 declarations
TemplateOneSidedPhaseSurvivingMatching.lean 2 declarations
TemplateOneSidedPhaseSurvivingPair.lean 6 declarations
TemplateOneSidedPhaseSurvivingPrior.lean 5 declarations
TemplateOneSidedPhaseSurvivingReindex.lean 6 declarations
TemplateOneSidedPhaseSurvivingRetained.lean 1 declarations
TemplateOneSidedPhaseSurvivingRetainedDefs.lean 2 declarations
TemplateOneSidedPhaseSurvivingSample.lean 2 declarations
TemplateOneSidedPhaseSurvivingSampleBasic.lean 3 declarations
TemplateOneSidedPhaseSurvivingSampleDefs.lean 8 declarations
TemplateOneSidedPhaseSurvivingSamplePair.lean 1 declarations
TemplateOneSidedPhaseSurvivingSourceOrder.lean 2 declarations
TemplateOneSidedPhaseSurvivingSplit.lean 6 declarations
TemplateOneSidedPhaseSurvivingSplitDefs.lean 3 declarations
TemplateOneSidedPhaseSurvivingSplitNorm.lean 4 declarations
TemplateOneSidedPhaseSurvivingSquare.lean 3 declarations
TemplateOneSidedPhaseSurvivingUnary.lean 9 declarations
TemplateOneSidedPhaseSurvivingVariables.lean 3 declarations
TemplateOneSidedPhaseTerminal.lean 3 declarations
TemplateOneSidedPhaseTerminalEdge.lean 1 declarations
TemplateOneSidedPhaseTerminalIndexedNorm.lean 5 declarations
TemplateOneSidedPhaseTerminalIndexedNormEventual.lean 1 declarations
TemplateOneSidedPhaseTerminalIndexedNormSource.lean 3 declarations
TemplateOneSidedPhaseTerminalIndexedReindex.lean 2 declarations
TemplateOneSidedPhaseTerminalIndexedSource.lean 4 declarations
TemplateOneSidedPhaseTerminalIndexedUnary.lean 2 declarations
TemplateOneSidedPhaseTerminalMasked.lean 4 declarations
TemplateOneSidedPhaseTerminalMaskedMean.lean 1 declarations
TemplateOneSidedPhaseTerminalMaskedNorm.lean 2 declarations
TemplateOneSidedPhaseTerminalMaskedNormEventual.lean 1 declarations
TemplateOneSidedPhaseTerminalPhaseNorm.lean 3 declarations
TemplateOneSidedPhaseTerminalPriorDefs.lean 5 declarations
TemplateOneSidedPhaseTerminalPriorMean.lean 3 declarations
TemplateOneSidedPhaseTerminalSourceScales.lean 6 declarations
TemplateOneSidedPhaseTerminalSplit.lean 4 declarations
TemplateOneSidedPhaseUnary.lean 7 declarations
TemplateOneSidedPhaseUnitsBasic.lean 10 declarations
TemplateOneSidedPhaseVariables.lean 3 declarations
TemplateOneSidedPrior.lean 5 declarations
TemplateOneSidedPriorBounds.lean 6 declarations
TemplateOneSidedPriorDyadic.lean 6 declarations
TemplateOneSidedPriorRows.lean 10 declarations
TemplateOneSidedPriorSource.lean 13 declarations
TemplateOneSidedRelabel.lean 5 declarations
TemplateOneSidedRelabelExpr.lean 17 declarations
TemplateOneSidedRelabelGuards.lean 17 declarations
TemplateOneSidedRelabelSampled.lean 11 declarations
TemplateOneSidedRelabelSlice.lean 11 declarations
TemplateOneSidedRelabelTemplate.lean 14 declarations
TemplateOneSidedSourceScales.lean 1 declarations
TemplateOneSidedSourceScalesBands.lean 5 declarations
TemplateOneSidedSourceScalesBasic.lean 7 declarations
TemplateOneSidedSourceScalesPair.lean 3 declarations
TemplateOneSidedSourceScalesShells.lean 5 declarations
TemplateOneSidedSourceSyntax.lean 16 declarations
TemplateOneSidedSupportSurviving.lean 6 declarations
TemplateOneSidedSupportSurvivingBudget.lean 0 declarations
TemplateOneSidedSupportSurvivingBudgetBasic.lean 3 declarations
TemplateOneSidedSupportSurvivingBudgetDivisors.lean 6 declarations
TemplateOneSidedSupportSurvivingBudgetFrequency.lean 1 declarations
TemplateOneSidedSupportSurvivingBudgetSource.lean 4 declarations
TemplateOneSidedSupportSurvivingExpressions.lean 9 declarations
TemplateOneSidedSupportSurvivingFamilies.lean 3 declarations
TemplateOneSidedSupportSurvivingOrigins.lean 10 declarations
TemplateOneSidedSupportSurvivingPairwise.lean 4 declarations
TemplateOneSidedSupportTelescoping.lean 1 declarations
TemplateOneSidedSupportTelescopingActual.lean 5 declarations
TemplateOneSidedSupportTelescopingEstimate.lean 1 declarations
TemplateOneSidedSupportTelescopingFamily.lean 6 declarations
TemplateOneSidedSupportTelescopingFinite.lean 6 declarations
TemplateOneSidedSupportTelescopingPairBudget.lean 3 declarations
TemplateOneSidedSupportTelescopingPairLiteral.lean 5 declarations
TemplateOneSidedSupportTelescopingPairReindexed.lean 4 declarations
TemplateOneSidedSupportTelescopingPairReindexedActual.lean 1 declarations
TemplateOneSidedSupportTelescopingPairWeight.lean 5 declarations
TemplateOneSidedSupportTransport.lean 3 declarations
TemplateOneSidedSupportTransportActual.lean 7 declarations
TemplateOneSidedSupportTransportEstimateReindexed.lean 1 declarations
TemplateOneSidedSupportTransportFamilies.lean 7 declarations
TemplateOneSidedSupportTransportPrior.lean 4 declarations
TemplateOneSidedTerminalIntegerPrior.lean 0 declarations
TemplateOneSidedTerminalIntegerPriorAtoms.lean 2 declarations
TemplateOneSidedTerminalIntegerPriorBasic.lean 9 declarations
TemplateOneSidedTerminalIntegerPriorProperties.lean 9 declarations
TemplateOneSidedTerminalSupportRemovalBudget.lean 6 declarations
TemplateOneSidedTerminalSupportRemovalDefs.lean 11 declarations
TemplateOneSidedTerminalSupportRemovalEnd.lean 3 declarations
TemplateOneSidedTerminalSupportRemovalError.lean 1 declarations
TemplateOneSidedTerminalSupportRemovalEstimate.lean 1 declarations
TemplateOneSidedTerminalSupportRemovalFrequency.lean 1 declarations
TemplateOneSidedTerminalSupportRemovalLiteral.lean 5 declarations
TemplateOneSidedTerminalSupportRemovalPhase.lean 2 declarations
TemplateOneSidedWindowRegularity.lean 4 declarations
TemplateOneSidedWindowRegularityBasic.lean 9 declarations
TemplateOneSidedWindowRegularityMasks.lean 2 declarations
TemplateOneSidedWindowRegularityValue.lean 3 declarations
TemplateOutgoingPivot.lean 7 declarations
TemplateOutgoingProduct.lean 2 declarations
TemplateParityActions.lean 1 declarations
TemplateParityActionsAnchors.lean 3 declarations
TemplateParityActionsBasic.lean 6 declarations
TemplateParityActionsPermutation.lean 14 declarations
TemplateParityActionsPrior.lean 5 declarations
TemplatePhaseConjugate.lean 2 declarations
TemplatePhasePivotSplit.lean 2 declarations
TemplatePhaseProduct.lean 3 declarations
TemplatePhaseProducts.lean 10 declarations
TemplatePhaseReindex.lean 2 declarations
TemplatePhaseRowNorm.lean 3 declarations
TemplatePhaseTransport.lean 11 declarations
TemplatePhaseTransportCore.lean 7 declarations
TemplatePivotCollapse.lean 4 declarations
TemplatePivotResidue.lean 6 declarations
TemplatePivotUnits.lean 5 declarations
TemplatePrimeArithmetic.lean 2 declarations
TemplatePrimeCharacterTransport.lean 4 declarations
TemplatePrimeExposure.lean 1 declarations
TemplatePrimeInteger.lean 3 declarations
TemplatePrimeRowUnits.lean 5 declarations
TemplatePrimeWeight.lean 1 declarations
TemplateRegularPhase.lean 3 declarations
TemplateResidueExposure.lean 8 declarations
TemplateRetainedNorm.lean 1 declarations
TemplateRetainedSquareSum.lean 1 declarations
TemplateSchedule.lean 14 declarations
TemplateScheduledAmplitude.lean 5 declarations
TemplateScheduledBounds.lean 4 declarations
TemplateScheduledIteration.lean 1 declarations
TemplateScheduledTransfer.lean 1 declarations
TemplateSharedCharacterTransport.lean 3 declarations
TemplateSourceAmplitude.lean 5 declarations
TemplateSourceFactorialBudget.lean 1 declarations
TemplateSourceIteration.lean 2 declarations
TemplateSourceIterationActual.lean 1 declarations
TemplateSourceParity.lean 2 declarations
TemplateSourceParityUpperExponent.lean 1 declarations
TemplateSourcePivotLoss.lean 1 declarations
TemplateSourcePivotLossActual.lean 3 declarations
TemplateSourcePivotLossBasic.lean 8 declarations
TemplateSourceTerminalNorm.lean 3 declarations
TemplateSourceTerminalSeparationExponent.lean 1 declarations
TemplateSupportRemoval.lean 1 declarations
TemplateSupportRemovalCardinality.lean 3 declarations
TemplateSupportRemovalComplex.lean 2 declarations
TemplateSupportRemovalCoordinates.lean 10 declarations
TemplateSupportRemovalCoprime.lean 4 declarations
TemplateSupportRemovalDegree.lean 2 declarations
TemplateSupportRemovalEstimate.lean 2 declarations
TemplateSupportRemovalFamily.lean 1 declarations
TemplateSupportRemovalFamilyEstimate.lean 2 declarations
TemplateSupportRemovalFamilyHeight.lean 1 declarations
TemplateSupportRemovalFamilyPoint.lean 3 declarations
TemplateSupportRemovalHeightBasic.lean 7 declarations
TemplateSupportRemovalHeightDenominator.lean 3 declarations
TemplateSupportRemovalHeightLog.lean 5 declarations
TemplateSupportRemovalHeightSize.lean 1 declarations
TemplateSupportRemovalHeightTemplate.lean 2 declarations
TemplateSupportRemovalHeightTemplateBasic.lean 6 declarations
TemplateSupportRemovalLeaf.lean 1 declarations
TemplateSupportRemovalLeafFrequency.lean 1 declarations
TemplateSupportRemovalNonzero.lean 3 declarations
TemplateSupportRemovalNumerics.lean 3 declarations
TemplateSupportRemovalPivot.lean 1 declarations
TemplateSupportRemovalPivotFrequency.lean 1 declarations
TemplateSupportRemovalPrior.lean 3 declarations
TemplateSupportRemovalSelected.lean 2 declarations
TemplateSymbolic.lean 18 declarations
TemplateTerminalFrequency.lean 3 declarations
TemplateTerminalGram.lean 4 declarations
TemplateTerminalGramAbsorption.lean 1 declarations
TemplateTerminalGramCardAbsorption.lean 1 declarations
TemplateTerminalGramMean.lean 3 declarations
TemplateTerminalNorm.lean 1 declarations
TemplateTerminalParity.lean 5 declarations
TemplateTerminalRoot.lean 3 declarations
TemplateTerminalRootCard.lean 3 declarations
TemplateTerminalRootNorm.lean 3 declarations
TemplateTerminalUnitRoot.lean 5 declarations
TemplateUnitSupport.lean 3 declarations
TemplateWeight.lean 8 declarations
TemplateWeightProfiles.lean 9 declarations
TemplateWeightedHilbert.lean 9 declarations
TemplateWeightedHilbertComparison.lean 3 declarations
TemplateWordMaps.lean 2 declarations
TemplateWords.lean 9 declarations
TensorKernelEnergy.lean 2 declarations
TensorRamanujanExpansion.lean 3 declarations
TensorUnitFullMean.lean 2 declarations
TensorUnitMean.lean 5 declarations
TensorUnitPolynomial.lean 4 declarations
TransferAlgebra.lean 7 declarations
TransferRows.lean 4 declarations
TranslatedCharacterPoisson.lean 4 declarations
TreeAncestorScheme.lean 5 declarations
TreeArrangementFraction.lean 2 declarations
TreeComparison.lean 1 declarations
TreeComparisonError.lean 3 declarations
TreeCoordinates.lean 13 declarations
TreeLeafIndex.lean 9 declarations
TreeLeafProducts.lean 11 declarations
TreeProductDisintegration.lean 3 declarations
TreeProfile.lean 7 declarations
TreeSplitCoordinates.lean 4 declarations
TreeSplitResidues.lean 9 declarations
TreeTupleProfiles.lean 7 declarations
TupleCRTFourier.lean 8 declarations
TupleCharacterPoisson.lean 9 declarations
TwistCauchy.lean 2 declarations
TypicalEndpoints.lean 2 declarations
TypicalSelection.lean 1 declarations
UniformFinite.lean 5 declarations
UniformMellin.lean 5 declarations
UnitRamanujanProduct.lean 5 declarations
WeightedPhaseExtraction.lean 3 declarations
WordSelection.lean 6 declarations
ZeroVariable.lean 4 declarations