`OAI/NumberTheory/JointDickman/Amplification/`

1791 declarations, 0 contain sorry, 0 declared as axioms; 540 files

Files

ActiveFirstForm.lean 6 declarations
ActiveVolumeBound.lean 2 declarations
ActiveVolumeMajorant.lean 5 declarations
ActualArithmeticFluctuation.lean 3 declarations
ActualArithmeticLimit.lean 4 declarations
ActualArithmeticMean.lean 1 declarations
ActualCandidateProduct.lean 3 declarations
AdditionCutoffScale.lean 2 declarations
AdditionProgressionGeometry.lean 4 declarations
AdditionProgressionInterval.lean 6 declarations
AdditionScaleDichotomy.lean 2 declarations
AdditionSmallBall.lean 1 declarations
AdditivePhaseBridge.lean 3 declarations
AdditivePhaseVariation.lean 3 declarations
AffineLocalFactors.lean 6 declarations
AllLargeHighExpectation.lean 2 declarations
AllLargeHighVanishing.lean 4 declarations
AllLargeLowExpectation.lean 2 declarations
AllLargeLowVanishing.lean 1 declarations
AmplificationArithmeticFeatures.lean 2 declarations
AmplificationBoxFeatures.lean 1 declarations
AmplificationBoxSupport.lean 7 declarations
AmplificationDyadicIdentity.lean 3 declarations
AmplificationEnvelope.lean 3 declarations
AmplificationEnvelopeFirst.lean 2 declarations
AmplificationFairFeatures.lean 1 declarations
AmplificationFirstForm.lean 8 declarations
AmplificationMultiplier.lean 5 declarations
AmplificationPointBounds.lean 5 declarations
AmplificationPositiveMass.lean 1 declarations
AmplificationRegularity.lean 1 declarations
AmplificationRegularityIdentity.lean 6 declarations
AmplificationRegularityLoss.lean 2 declarations
AmplificationReindex.lean 4 declarations
AmplificationScaleSum.lean 3 declarations
AmplificationSquareRate.lean 1 declarations
AmplificationVolumeProducts.lean 6 declarations
AmplificationWeightBound.lean 4 declarations
AmplifiedProfile.lean 3 declarations
AmplitudeParameterVariation.lean 2 declarations
ArithGraph.lean 4 declarations
ArithmeticAmplification.lean 2 declarations
ArithmeticAmplificationBounds.lean 5 declarations
ArithmeticCandidateRoots.lean 6 declarations
ArithmeticCandidateSum.lean 2 declarations
ArithmeticCandidateWeight.lean 2 declarations
ArithmeticFeatureComparison.lean 1 declarations
ArithmeticForcedCost.lean 2 declarations
ArithmeticGraphBounds.lean 4 declarations
ArithmeticGraphCandidateCount.lean 4 declarations
ArithmeticGraphPair.lean 4 declarations
ArithmeticGraphPointCap.lean 3 declarations
ArithmeticGraphSymmetry.lean 3 declarations
ArithmeticInputs.lean 7 declarations
ArithmeticLongFluctuation.lean 1 declarations
ArithmeticModelError.lean 2 declarations
ArithmeticOffDiagonalGraph.lean 3 declarations
ArithmeticPatternMeans.lean 6 declarations
ArithmeticPeriod.lean 10 declarations
ArithmeticProfilePreservation.lean 5 declarations
ArithmeticRootIdentification.lean 3 declarations
ArithmeticRootMask.lean 4 declarations
ArithmeticSquareHits.lean 5 declarations
AtomicProductMeasure.lean 8 declarations
AuxiliaryBandChoice.lean 1 declarations
AuxiliaryBandCount.lean 3 declarations
AuxiliaryBandDensity.lean 1 declarations
AuxiliaryCofactorScales.lean 1 declarations
AuxiliaryCostBound.lean 1 declarations
AuxiliaryCostLimit.lean 4 declarations
AuxiliaryCostSum.lean 2 declarations
AuxiliaryLargeSamples.lean 1 declarations
AuxiliaryLogBins.lean 4 declarations
AuxiliaryLogWeights.lean 3 declarations
AuxiliaryLogarithms.lean 7 declarations
AuxiliaryOdds.lean 3 declarations
AuxiliaryPowerDensity.lean 2 declarations
AuxiliaryPowerSeparation.lean 1 declarations
AuxiliaryRangeScales.lean 1 declarations
AuxiliaryScalarBounds.lean 4 declarations
AuxiliaryScale.lean 11 declarations
AveragedConditionedRoots.lean 1 declarations
AveragedRootFluctuation.lean 3 declarations
BaseCandidateMass.lean 3 declarations
BaseCandidateMassBound.lean 1 declarations
BinAuxiliaryCofactor.lean 1 declarations
BinAwaySpectral.lean 1 declarations
BinCofactorBound.lean 4 declarations
BinCorrelationLimit.lean 1 declarations
BinCorrelationLimitDischarge.lean 1 declarations
BinCounts.lean 8 declarations
BinDecorrelation.lean 3 declarations
BinDecorrelationDischarge.lean 1 declarations
BinDyadicLowFrequency.lean 1 declarations
BinJointEvents.lean 3 declarations
BinJointEventsDischarge.lean 1 declarations
BinLabelAmplification.lean 2 declarations
BinLabels.lean 30 declarations
BinLowFrequency.lean 5 declarations
BinMarginalGenerating.lean 4 declarations
BinMarginalInput.lean 7 declarations
BinMarginalMean.lean 5 declarations
BinPrefixMeans.lean 3 declarations
BinStateExtraction.lean 5 declarations
BinStateLimit.lean 3 declarations
BinWeightedMarginal.lean 5 declarations
BoundedBoxCoarse.lean 1 declarations
BoundedBoxFullModel.lean 1 declarations
BoundedBoxSpatial.lean 1 declarations
CRTMean.lean 1 declarations
CandidateAdditionClasses.lean 3 declarations
CandidateArithmeticPeriod.lean 5 declarations
CandidateCollisionGeometry.lean 4 declarations
CandidateConditionalMean.lean 2 declarations
CandidateCountScale.lean 3 declarations
CandidateCutoffNorm.lean 3 declarations
CandidateExpectedDegree.lean 4 declarations
CandidateFairArithmetic.lean 2 declarations
CandidateFiniteCutoff.lean 4 declarations
CandidateForcedConditional.lean 2 declarations
CandidateForcedEvent.lean 3 declarations
CandidateForcedProbability.lean 4 declarations
CandidateForwardMass.lean 3 declarations
CandidateGraphEncoding.lean 5 declarations
CandidateMatrix.lean 7 declarations
CandidateMeanBridge.lean 3 declarations
CandidateModularRoots.lean 3 declarations
CandidateMultiplicity.lean 3 declarations
CandidateMultiplicityAverage.lean 2 declarations
CandidateMultiplicityBound.lean 1 declarations
CandidatePairSum.lean 2 declarations
CandidateProductMean.lean 3 declarations
CandidateRemainderRemoval.lean 1 declarations
CandidateRepeatConditional.lean 1 declarations
CandidateRepeatEvent.lean 6 declarations
CandidateRepeatProbability.lean 4 declarations
CandidateReverseConditional.lean 1 declarations
CandidateReverseMajorant.lean 2 declarations
CandidateRootErrorCap.lean 3 declarations
CandidateRootGeometry.lean 4 declarations
CandidateRowMajorant.lean 2 declarations
CandidateScalarIdentity.lean 5 declarations
CandidateScalarSum.lean 2 declarations
CandidateWeightCap.lean 1 declarations
CanonicalAffineCost.lean 4 declarations
CanonicalExceptionalSamples.lean 2 declarations
CanonicalTypicalDensity.lean 5 declarations
CellAverageOscillation.lean 4 declarations
CellAverageProfile.lean 2 declarations
CenteredBinSpectral.lean 2 declarations
ChebyshevDischarge.lean 2 declarations
ChernoffParameters.lean 3 declarations
ClippedProfile.lean 3 declarations
CoarseCellUnion.lean 6 declarations
CoarseCenteredWeight.lean 1 declarations
CoarseCompactness.lean 2 declarations
CoarseErrorLimit.lean 4 declarations
CoarseFeatureAverage.lean 3 declarations
CoarseFeatureBounds.lean 3 declarations
CoarseFeaturePolynomial.lean 2 declarations
CoarseGrid.lean 12 declarations
ColumnResponseMean.lean 2 declarations
CompactOscillatorySupport.lean 2 declarations
ComplexPartialSummation.lean 1 declarations
ConditionalAdditionProduct.lean 10 declarations
ConditionalOrientedEvent.lean 1 declarations
ConditionedRootComparison.lean 4 declarations
ConditionedRootErrorLimit.lean 3 declarations
ConditionedRootFluctuation.lean 2 declarations
ConditionedRootTests.lean 4 declarations
ConsecutiveCRT.lean 2 declarations
CorrectionTails.lean 3 declarations
CorrelationPhase.lean 1 import, no declarations
CountMaskDistance.lean 1 declarations
CutBounds.lean 12 declarations
DependentProductMean.lean 2 declarations
DiagonalRemoval.lean 4 declarations
DiscardedRegionBound.lean 1 declarations
DischargedMinorArcBox.lean 1 declarations
DiscreteFirstDerivative.lean 1 import, no declarations
DiscreteSecondDerivative.lean 1 import, no declarations
DyadicBoxRegularity.lean 2 declarations
DyadicChangeScales.lean 3 declarations
DyadicTailSum.lean 6 declarations
EmpiricalRangeTransfer.lean 3 declarations
EndpointConditionalMean.lean 4 declarations
EndpointFourierBounds.lean 3 declarations
EndpointFourierReflection.lean 3 declarations
EndpointFullArcLaw.lean 3 declarations
EndpointFullModel.lean 1 declarations
EndpointIntegralReplacement.lean 1 declarations
EndpointParameterVariation.lean 3 declarations
EndpointRowEnvelope.lean 6 declarations
EndpointRowScale.lean 4 declarations
EndpointSupportSum.lean 3 declarations
ExceptionalProductIntegral.lean 1 declarations
FairAverageContraction.lean 4 declarations
FiniteAdditiveOrthogonality.lean 7 declarations
FiniteConditionalProduct.lean 6 declarations
FiniteCutoffMean.lean 3 declarations
FiniteCutoffProfiles.lean 9 declarations
FiniteEventUnion.lean 1 declarations
FiniteExponentialMaximum.lean 3 declarations
FiniteGraphFluctuation.lean 1 declarations
FiniteGraphRegroup.lean 1 declarations
FiniteHitMass.lean 3 declarations
FiniteHoeffding.lean 4 declarations
FinitePointMass.lean 5 declarations
FinitePowerSaving.lean 1 import, no declarations
FiniteProductMGF.lean 6 declarations
FiniteProductTail.lean 3 declarations
FiniteRampApproximation.lean 2 declarations
FiniteRampMean.lean 5 declarations
FiniteRampWeights.lean 3 declarations
FiniteStatistics.lean 9 declarations
FiniteTripleExtension.lean 1 declarations
FiniteWeightAverages.lean 1 declarations
FiniteWeightCofactorComplete.lean 2 declarations
FiniteWeightCountPrefix.lean 1 declarations
FiniteWeightPhase.lean 2 declarations
FiniteWeightedSquare.lean 3 declarations
FiniteWeightedUnion.lean 2 declarations
FirstFormDiagonal.lean 5 declarations
FirstFormMass.lean 3 declarations
FirstFormPairs.lean 5 declarations
FirstPairMass.lean 2 declarations
FirstPairMassBound.lean 3 declarations
FirstRepresentationSum.lean 2 declarations
FloorErrors.lean 3 declarations
ForwardDifference.lean 1 import, no declarations
FourSubsetFailure.lean 5 declarations
FourierProfileTail.lean 3 declarations
FrozenFullArcIntegral.lean 1 declarations
FrozenSmallArcIntegral.lean 2 declarations
FullArcDenominators.lean 2 declarations
FullCoarseComparison.lean 1 declarations
FullModelLinearity.lean 4 declarations
FullSmallArcModel.lean 2 declarations
FullSpatialComparison.lean 4 declarations
GcdReciprocalMean.lean 3 declarations
GeneratingBinExpansion.lean 3 declarations
GeneratingDegreeExpansion.lean 4 declarations
GeneratingFloorLimit.lean 6 declarations
GeometricArithmeticIdentity.lean 2 declarations
GeometricBoxErrors.lean 3 declarations
GeometricDiscardedArcs.lean 2 declarations
GeometricDyadicPartition.lean 5 declarations
GeometricFeatureBounds.lean 1 declarations
GeometricFullModel.lean 2 declarations
GeometricFullModelBound.lean 1 declarations
GeometricPeriodLaw.lean 3 declarations
GeometricRetainedError.lean 2 declarations
GeometricSampledIntegral.lean 2 declarations
GeometricSeriesError.lean 1 declarations
GraphBoundaryCap.lean 5 declarations
GraphCandidateDecoding.lean 6 declarations
GraphEdgeMajorant.lean 6 declarations
GraphEdgeMeanBound.lean 3 declarations
GraphEdgePeriod.lean 9 declarations
GraphEdgeSwap.lean 3 declarations
GraphEndpointDensity.lean 3 declarations
GraphPairMass.lean 5 declarations
GraphSquareRemoval.lean 5 declarations
GraphTripleSupport.lean 4 declarations
GridMultiplicityBounds.lean 2 declarations
HalaszArithmetic.lean 2 declarations
HalaszMeanLimit.lean 3 declarations
HalaszRealCutoff.lean 2 declarations
HalfArithmetic.lean 6 declarations
HighExclusiveLocalLaw.lean 4 declarations
HighExclusiveThreshold.lean 1 declarations
HighLowThinning.lean 6 declarations
HyperbolaBudget.lean 2 declarations
HyperbolaRounding.lean 7 declarations
IncreasingPartialSummation.lean 2 declarations
IndependentForcedHits.lean 3 declarations
IndependentRegularityLoss.lean 5 declarations
IndependentRootMaximum.lean 2 declarations
IndependentRootMean.lean 6 declarations
IntegerPartialSummation.lean 3 declarations
IntegerRationalSum.lean 2 declarations
IntegralFromSamples.lean 4 declarations
IntegratedSampledError.lean 2 declarations
InteriorAmplificationMass.lean 5 declarations
InteriorRegularity.lean 4 declarations
IntervalRemainder.lean 1 declarations
IntervalSquareBound.lean 2 declarations
IteratedDifferencing.lean 1 import, no declarations
LargeAdditionAvailability.lean 5 declarations
LargeAlternativeBound.lean 1 declarations
LargeAlternativeCount.lean 1 declarations
LargeAlternativeExpectation.lean 2 declarations
LargeAlternativePairs.lean 4 declarations
LargeCardinalityPartition.lean 4 declarations
LargeHighClass.lean 3 declarations
LargeHighVanishing.lean 5 declarations
LargeLowAdditionAvailability.lean 2 declarations
LargeLowClass.lean 2 declarations
LargeLowNumericAddition.lean 1 declarations
LargeLowVanishing.lean 2 declarations
LargeMajorBoxBound.lean 1 declarations
LargeMultiplicityExponent.lean 4 declarations
LargeNumericAddition.lean 2 declarations
LastBandSamples.lean 1 declarations
LatentContributionCap.lean 1 declarations
LatentEdgeSquareBound.lean 1 declarations
LatentRowSquareBound.lean 1 declarations
LatentRowSquareMass.lean 3 declarations
LatentSquareSymmetry.lean 5 declarations
LiftedRationalEquiv.lean 4 declarations
LipschitzRiemannSum.lean 2 declarations
LocalArcIntegral.lean 2 declarations
LogErrorAllCutoffs.lean 2 declarations
LogFrequencyBounds.lean 1 declarations
LogIntervalApproximation.lean 8 declarations
LogIntervalSquareError.lean 1 declarations
LogMassBilinear.lean 7 declarations
LogOscillatoryTest.lean 7 declarations
LogProductBounds.lean 4 declarations
LogScaleBigO.lean 1 declarations
LogScaleComparison.lean 3 declarations
LowAdditionGeometry.lean 3 declarations
LowAlternativeBound.lean 1 declarations
LowAlternativeCount.lean 1 declarations
LowAlternativeExpectation.lean 2 declarations
LowAlternativePairs.lean 2 declarations
LowCardinalityPartition.lean 3 declarations
LowNumericAdditionBound.lean 1 declarations
LowNumericAdditionClass.lean 3 declarations
MajorArcApproximation.lean 2 declarations
MajorArcErrorSum.lean 4 declarations
MajorArcFiniteSum.lean 4 declarations
MajorArcPartition.lean 10 declarations
MajorArcUnfolding.lean 5 declarations
ManuscriptAdditionProduct.lean 8 declarations
MarginalTupleDischarge.lean 2 declarations
MarkovRemainders.lean 3 declarations
MaskedArithmeticFluctuation.lean 10 declarations
MiddleCountPrefix.lean 2 declarations
MinorArcApproximation.lean 2 declarations
MinorArcBoxBound.lean 1 declarations
MinorArcMeasurable.lean 4 declarations
MinorArcRate.lean 2 declarations
MinorArcStrongApproximation.lean 1 declarations
MixedThreeFormLocal.lean 6 declarations
MonotonePartialSummation.lean 1 declarations
MonotoneSumComparison.lean 2 declarations
MovingLimit.lean 6 declarations
MovingMonotoneLimit.lean 1 declarations
MovingThresholds.lean 7 declarations
MultiplicativeExponentialInput.lean 4 declarations
MultiplicityChernoff.lean 1 declarations
MultiplicityMargins.lean 3 declarations
MultiplicityParameters.lean 3 declarations
MultiplicityRates.lean 4 declarations
NativeOrientedEvent.lean 3 declarations
NearCofactorMean.lean 4 declarations
NearbyAdditiveSums.lean 2 declarations
NoChangeConditional.lean 4 declarations
NoChangeProbability.lean 1 declarations
NonzeroGraphAtoms.lean 3 declarations
NumericAdditionBound.lean 1 declarations
NumericAdditionClass.lean 6 declarations
NumericAdditionWeights.lean 3 declarations
NumericRankinExponent.lean 5 declarations
OccupiedRootComparison.lean 5 declarations
OmissionEntropy.lean 2 declarations
OmissionEnvelope.lean 4 declarations
OrderedBinTuples.lean 3 declarations
Ordering.lean 22 declarations
OrientedProbabilityBound.lean 4 declarations
OscillatoryError.lean 1 declarations
OscillatoryTests.lean 10 declarations
OutsideCandidateMass.lean 5 declarations
OutsideCandidateProduct.lean 2 declarations
ParameterEstimates.lean 20 declarations
PeriodCoarseComparison.lean 1 declarations
PeriodCoarseVanishing.lean 1 declarations
PhaseExtension.lean 1 import, no declarations
PolylogHyperbolaBudget.lean 1 declarations
PolylogMultiplicativeSum.lean 4 declarations
PolynomialArithmeticFeatures.lean 4 declarations
PolynomialTermAmplitudeVariation.lean 1 declarations
PositiveArithmeticGraph.lean 1 declarations
PrefixFromIntervals.lean 1 declarations
PrefixOmissions.lean 3 declarations
PrefixViolationSum.lean 5 declarations
PretentiousFrequencySeparation.lean 3 declarations
PrincipalBinRestriction.lean 4 declarations
ProductComparison.lean 25 declarations
ProductLogCells.lean 4 declarations
ProfilePreservation.lean 5 declarations
ProjectedMajorIntegral.lean 2 declarations
PublishedInputs.lean 7 declarations
PublishedRampProfile.lean 3 declarations
RamanujanMultiplicative.lean 6 declarations
RamanujanRoots.lean 5 declarations
RamanujanSum.lean 4 declarations
RamanujanVanishing.lean 4 declarations
RamareIntegralBound.lean 1 declarations
RamareProductIntegral.lean 1 declarations
RampCutoff.lean 7 declarations
RampDensity.lean 6 declarations
RampDensityIntegral.lean 3 declarations
RampLocalLaw.lean 4 declarations
RampProfile.lean 2 declarations
RampedCandidate.lean 7 declarations
RampedCandidateMean.lean 1 declarations
RationalArcSeparation.lean 4 declarations
RationalCandidateRoots.lean 5 declarations
RationalPartialSums.lean 2 declarations
RationalThresholds.lean 4 declarations
RationalThresholdsDischarge.lean 2 declarations
RationalUnitRepresentatives.lean 5 declarations
RealDistanceDivergence.lean 2 declarations
RealMajorIntegrals.lean 1 declarations
ReciprocalDerivatives.lean 1 import, no declarations
ReciprocalTail.lean 2 declarations
RectangleRemainder.lean 2 declarations
ReducedArcLifts.lean 6 declarations
ReducedRationalEquiv.lean 6 declarations
RegularAlternatives.lean 3 declarations
RegularAmplificationMass.lean 5 declarations
RegularOmissionChoices.lean 2 declarations
RegularOmissionEntropy.lean 1 declarations
RegularPairChangeOfMeasure.lean 2 declarations
RegularPrefixChoices.lean 2 declarations
RegularTiltAverage.lean 8 declarations
RegularWeightCap.lean 2 declarations
RegularityChernoffFactors.lean 6 declarations
RegularityUnionBound.lean 5 declarations
RegularizedProductWeight.lean 3 declarations
ReindexedCells.lean 8 declarations
RemainderFailureWeight.lean 1 declarations
RemainderNormalization.lean 2 declarations
RemainderPushforward.lean 4 declarations
RequiredSubsetTail.lean 2 declarations
RescaledMajorIntegral.lean 3 declarations
RestrictedRootComparison.lean 3 declarations
RestrictedRootMass.lean 5 declarations
RetainedErrorSum.lean 4 declarations
RetainedRatioTest.lean 2 declarations
ReverseEndpointTest.lean 9 declarations
ReverseRowEnvelope.lean 3 declarations
RootComparisonScale.lean 2 declarations
RootCutDecay.lean 1 declarations
RootFluctuationMGF.lean 2 declarations
RootSelection.lean 3 declarations
SampledColumnTail.lean 2 declarations
ScaledFourierTail.lean 2 declarations
ScaledIntervalCover.lean 2 declarations
ScaledOscillatoryTests.lean 7 declarations
SchwartzArithmeticFeatures.lean 1 declarations
SchwartzFourierProfile.lean 4 declarations
SecondDerivativeBudget.lean 1 import, no declarations
SecondDerivativeTest.lean 1 import, no declarations
SecondDifference.lean 1 import, no declarations
SecondOrientedProbability.lean 3 declarations
SeparatedCellIntegral.lean 2 declarations
SeparatedIntervalCount.lean 1 import, no declarations
ShrinkingDensity.lean 6 declarations
SiegelBounds.lean 1 import, no declarations
SignedLocalRegularity.lean 2 declarations
SignedPairPushforward.lean 4 declarations
SignedProductGcd.lean 6 declarations
SignedRegularityLoss.lean 11 declarations
SignedRemainderError.lean 1 declarations
SingleRegularityLoss.lean 2 declarations
SingleViolationBounds.lean 4 declarations
SingleViolationSums.lean 2 declarations
SingularFactor.lean 5 declarations
SingularSeries.lean 13 declarations
SingularSeriesApproximation.lean 7 declarations
SingularSeriesTail.lean 5 declarations
SingularSeriesTruncation.lean 3 declarations
SingularTailRate.lean 3 declarations
SmallAdditionCount.lean 4 declarations
SmallArcModel.lean 3 declarations
SmallBilinearVariables.lean 5 declarations
SmallCandidateMultiplicity.lean 6 declarations
SmallMajorArcFiniteSum.lean 2 declarations
SmallMajorArcRescaling.lean 1 declarations
SublevelContinuity.lean 2 declarations
SubsequenceAmplifiedProfile.lean 2 declarations
SubsequencePositiveGraph.lean 1 declarations
SubsetCardEntropy.lean 2 declarations
SubsetCountBounds.lean 2 declarations
SubsetPairTests.lean 5 declarations
SubsetPartition.lean 4 declarations
SubsetThinning.lean 4 declarations
SummedLocalErrors.lean 4 declarations
TailViolationSum.lean 3 declarations
TaylorBounds.lean 1 import, no declarations
ThinningRanges.lean 6 declarations
ThreeFormLocalBound.lean 8 declarations
TiltedAdditionRate.lean 2 declarations
TiltedAdditionTail.lean 3 declarations
TiltedPrefixMeans.lean 3 declarations
TrimmedCandidateRoots.lean 3 declarations
TruncatedMajorRegion.lean 7 declarations
TruncatedUpperVariation.lean 1 declarations
TwistedAuxiliaryCofactor.lean 1 declarations
TwistedBinDistance.lean 3 declarations
TwistedBinInterpolants.lean 6 declarations
TwistedBinLowFrequency.lean 2 declarations
TwistedBinMean.lean 2 declarations
TwistedBinSpectral.lean 1 declarations
TwoFormLocalBound.lean 4 declarations
TwoFormSubtraction.lean 2 declarations
UniformPrefixGrid.lean 2 declarations
UniformPrefixLimit.lean 1 declarations
UnionSelection.lean 2 declarations
UnitProgressionBinAverage.lean 4 declarations
UnoccupiedRootLaw.lean 2 declarations
UnsmoothingPowerBound.lean 1 declarations
VanDerCorput.lean 1 import, no declarations
WeightedAmplification.lean 4 declarations
WeightedArithmeticFeatures.lean 1 declarations
WeightedArithmeticIdentity.lean 2 declarations
WeightedBoxErrors.lean 1 declarations
WeightedCandidateComparison.lean 3 declarations
WeightedCandidateGcd.lean 1 declarations
WeightedCandidateMean.lean 2 declarations
WeightedCandidateMultiplicity.lean 2 declarations
WeightedCandidateProduct.lean 6 declarations
WeightedCauchy.lean 2 declarations
WeightedCountTail.lean 5 declarations
WeightedDiscardedArcs.lean 1 declarations
WeightedEndpointPair.lean 2 declarations
WeightedFourierTruncation.lean 1 declarations
WeightedGeometricError.lean 2 declarations
WeightedPartialSummation.lean 1 declarations
WeightedPeriodCoarse.lean 1 declarations
WeightedPeriodLaw.lean 2 declarations
WeightedPeriodVanishing.lean 1 declarations
WeightedPolynomialBounds.lean 2 declarations
WeightedPolynomialFeatures.lean 4 declarations
WeightedPowerExpansion.lean 5 declarations
WeightedRemainderLaw.lean 5 declarations
ZeroFreeBounds.lean 1 import, no declarations