`OAI/NumberTheory/JointDickman/Counting/`

894 declarations, 0 contain sorry, 0 declared as axioms; 267 files

Files

AdditionRatioWindow.lean 5 declarations
AmplificationWindows.lean 6 declarations
ArcCoefficientIdentity.lean 9 declarations
ArcWindowUnfolding.lean 2 declarations
ArithmeticBlockAverage.lean 6 declarations
ArithmeticBlockMatrix.lean 5 declarations
ArithmeticBlockMean.lean 1 declarations
ArithmeticBlockMeanDischarge.lean 1 declarations
ArithmeticBlockPrefix.lean 1 declarations
ArithmeticCoefficientHits.lean 4 declarations
ArithmeticCoefficientProbability.lean 7 declarations
ArithmeticLagCorrelations.lean 5 declarations
AuxiliaryBandEnergy.lean 3 declarations
AuxiliaryExceptionalEnergy.lean 2 declarations
AuxiliaryPowerEnergy.lean 3 declarations
BilinearEnergy.lean 0 declarations
BinExceptionalEnergy.lean 1 declarations
BinLabelPositiveEnergy.lean 3 declarations
BinPrincipalShort.lean 1 declarations
BinShortAverages.lean 7 declarations
BlockCandidates.lean 13 declarations
BlockCounting.lean 5 declarations
BlockCutNorm.lean 4 declarations
BlockEndpointLoss.lean 5 declarations
BlockEnergyApproximation.lean 1 declarations
BlockMatrixIndices.lean 2 declarations
BlockOriginSum.lean 1 declarations
BlockPatternTranspose.lean 5 declarations
BlockReindex.lean 4 declarations
BlockSiteComparison.lean 3 declarations
BlockSiteErrorScale.lean 3 declarations
BlockSquareHits.lean 3 declarations
BlockSquarePeriod.lean 5 declarations
CandidateCoefficientFactor.lean 6 declarations
CandidateCoefficientRemoval.lean 2 declarations
CanonicalAffineEnergy.lean 1 declarations
CanonicalFullEnergy.lean 1 declarations
CanonicalWindowCost.lean 1 declarations
CanonicalWindowEnergy.lean 1 declarations
CenteredShortCoefficients.lean 5 declarations
CoarseBinShort.lean 1 declarations
CoarseBinShortDischarge.lean 1 declarations
CoarseCoefficientVariation.lean 4 declarations
CoarseCountingConvolution.lean 1 declarations
CoarseCountingConvolutionDischarge.lean 1 declarations
CoarseCountingRows.lean 1 declarations
CoarseCountingRowsDischarge.lean 1 declarations
CoarseDiscreteShort.lean 2 declarations
CoarseDiscreteShortDischarge.lean 1 declarations
CoarseShiftedShort.lean 3 declarations
CoarseShiftedShortDischarge.lean 1 declarations
CoefficientArcErrorScale.lean 1 declarations
CoefficientCountIndicators.lean 6 declarations
CoefficientCutoffRemoval.lean 1 declarations
CoefficientDensityBound.lean 3 declarations
CoefficientDensityRegularity.lean 1 declarations
CoefficientDigitEvents.lean 7 declarations
CoefficientDomination.lean 1 declarations
CoefficientDyadicBoxes.lean 9 declarations
CoefficientErrorScale.lean 3 declarations
CoefficientEventBound.lean 3 declarations
CoefficientFourierContinuity.lean 3 declarations
CoefficientMinorArc.lean 1 declarations
CoefficientMoments.lean 6 declarations
CoefficientPairBound.lean 1 declarations
CoefficientPairMajorant.lean 1 declarations
CoefficientPartialSum.lean 3 declarations
CoefficientProbabilityLoss.lean 6 declarations
CoefficientProductSupport.lean 3 declarations
CoefficientProfileFreeze.lean 4 declarations
CoefficientRationalArc.lean 1 declarations
CoefficientRegularityLoss.lean 6 declarations
CoefficientRegularization.lean 3 declarations
CoefficientScalePower.lean 1 declarations
CoefficientSubtraction.lean 2 declarations
CoefficientThreeForm.lean 1 declarations
CoefficientTripleBound.lean 1 declarations
CoefficientViolationBounds.lean 4 declarations
CoefficientWeights.lean 10 declarations
CoefficientWindow.lean 1 declarations
ComplexCoefficientLaw.lean 2 declarations
ComplexFiniteShortAverages.lean 7 declarations
ComplexShortIntegrability.lean 1 declarations
ComplexShortIntervalConsequences.lean 8 declarations
ConvolutionTail.lean 6 declarations
CountingApplicationScale.lean 6 declarations
CountingArithmeticCoefficient.lean 2 declarations
CountingArithmeticFeatures.lean 2 declarations
CountingArithmeticMean.lean 4 declarations
CountingBlockTest.lean 1 declarations
CountingBoxFeatures.lean 1 declarations
CountingCandidateApproximation.lean 1 declarations
CountingCandidateComparison.lean 1 declarations
CountingCandidateModel.lean 4 declarations
CountingCoefficientRegularity.lean 3 declarations
CountingCutoffError.lean 4 declarations
CountingDyadicIdentity.lean 3 declarations
CountingEnergyBound.lean 2 declarations
CountingEntryVariation.lean 1 declarations
CountingErrorBound.lean 1 declarations
CountingErrorParameter.lean 1 declarations
CountingErrorRate.lean 4 declarations
CountingFeatureRows.lean 2 declarations
CountingForwardEnergy.lean 1 declarations
CountingForwardEnergyDischarge.lean 1 declarations
CountingForwardRows.lean 4 declarations
CountingKernelBound.lean 1 declarations
CountingLagVariation.lean 2 declarations
CountingModelEnvelope.lean 2 declarations
CountingModelMean.lean 1 declarations
CountingModelMeanDischarge.lean 1 declarations
CountingOriginParameter.lean 4 declarations
CountingParameterVariation.lean 1 declarations
CountingPeriodicEnergy.lean 4 declarations
CountingPeriodicEnergyDischarge.lean 1 declarations
CountingPeriodicModel.lean 7 declarations
CountingPrefixMean.lean 1 declarations
CountingPrefixMeanDischarge.lean 1 declarations
CountingRamp.lean 12 declarations
CountingSampling.lean 1 declarations
CountingSamplingMean.lean 1 declarations
CountingSamplingScale.lean 1 declarations
CountingShift.lean 3 declarations
CountingSiteModel.lean 5 declarations
CountingSiteMoments.lean 1 declarations
CountingSiteTest.lean 3 declarations
CountingSiteTestBound.lean 1 declarations
CountingSlowMean.lean 4 declarations
CountingTensorProfile.lean 5 declarations
CountingUpperVariation.lean 2 declarations
CyclicGeometricEnergy.lean 6 declarations
DilatedWindowEnergy.lean 1 declarations
DischargedCoefficientMinorArc.lean 1 declarations
DiscreteShortEnergy.lean 4 declarations
DistanceLagSum.lean 3 declarations
DyadicScaleWindow.lean 3 declarations
EndpointCoefficientMass.lean 2 declarations
EndpointCoefficientTest.lean 5 declarations
EndpointCountingCutoff.lean 6 declarations
EndpointScaleWindow.lean 1 declarations
EndpointWindowIdentity.lean 1 declarations
EnergyMeanComparison.lean 3 declarations
EntropyWindowStability.lean 1 declarations
FiniteConvolutionShift.lean 5 declarations
FiniteCountingComparison.lean 2 declarations
FiniteCountingMean.lean 1 declarations
FiniteCountingMeanDischarge.lean 1 declarations
FiniteForwardLagSum.lean 1 declarations
FiniteSamplingComparison.lean 1 declarations
FiniteShortComponents.lean 1 declarations
FiniteWeightCofactorWindow.lean 1 declarations
FiniteWeightedCoefficient.lean 5 declarations
FirstCoefficientAverage.lean 4 declarations
FixedResidueBinShort.lean 1 declarations
FixedResidueEnergy.lean 2 declarations
ForwardLagSum.lean 1 declarations
ForwardQuadraticEnergy.lean 4 declarations
FrozenCoefficientLaw.lean 2 declarations
GeometricCoefficientLaw.lean 2 declarations
GeometricWindowKernel.lean 3 declarations
GraphCoefficientMass.lean 4 declarations
GraphCoefficientReindex.lean 7 declarations
GraphCoefficientSupport.lean 3 declarations
GraphCountingSupport.lean 3 declarations
GraphLagMajorant.lean 6 declarations
GraphLagSwap.lean 7 declarations
HankelGammaCoefficients.lean 5 declarations
HighCofactorWindow.lean 1 declarations
HistogramBoxEnergy.lean 2 declarations
HistogramCellCoefficients.lean 5 declarations
HistogramOverlapEnergy.lean 2 declarations
HistogramWindowBounds.lean 2 declarations
HistogramWindowOverlap.lean 2 declarations
HistogramWindows.lean 4 declarations
HyperbolaBlockBound.lean 3 declarations
IndependentLargeCoefficients.lean 1 declarations
IntegratedCoefficientLaw.lean 2 declarations
InteriorAmplificationWindows.lean 7 declarations
IntervalEnergyError.lean 1 declarations
LagEnvelopeMoments.lean 6 declarations
LagEnvelopeTests.lean 1 declarations
LagParameterVariation.lean 1 declarations
LagSquareSum.lean 3 declarations
LargeAdditionWindow.lean 1 declarations
LargeMajorCoefficient.lean 2 declarations
MajorCoefficientBound.lean 2 declarations
MaskedCoefficientErrors.lean 6 declarations
MinorArcSupportWindow.lean 1 declarations
MonotoneBlocks.lean 1 import, no declarations
NearCofactorWindow.lean 1 declarations
NonprincipalBinShort.lean 3 declarations
NonprincipalShortDischarge.lean 1 declarations
NormalizedLagCoefficient.lean 3 declarations
OffDiagonalEnergy.lean 6 declarations
OriginRampAverage.lean 1 declarations
OriginRampShift.lean 2 declarations
OscillatoryCoefficientLaw.lean 2 declarations
PeriodicAverages.lean 11 declarations
PeriodicCandidateCutoff.lean 6 declarations
PeriodicCoefficientLaw.lean 2 declarations
PeriodicCountingBand.lean 3 declarations
PeriodicNonnegative.lean 3 declarations
PeriodicPositiveSums.lean 3 declarations
PeriodicProfileMeans.lean 4 declarations
PeriodicRectangle.lean 1 declarations
PeriodicWindowIntegral.lean 3 declarations
PolynomialTermLagVariation.lean 3 declarations
PositiveBlockEnergy.lean 2 declarations
PositiveFirstFormEnergy.lean 4 declarations
PositiveLagMass.lean 2 declarations
PrefixOmissionWindow.lean 3 declarations
PrescribedCenterShort.lean 3 declarations
PrescribedShortDischarge.lean 2 declarations
PrincipalBinShortDischarge.lean 1 declarations
RealPeriodicMoments.lean 1 declarations
ResidueBoxEnergy.lean 2 declarations
ResidueCoarseShort.lean 2 declarations
ResidueCoarseShortDischarge.lean 2 declarations
ReverseCoefficientMass.lean 3 declarations
SamplingComparisonLimit.lean 1 declarations
SamplingConcentration.lean 20 declarations
SamplingErrorBounds.lean 5 declarations
SamplingErrorEnvelope.lean 3 declarations
SamplingFamilyRate.lean 4 declarations
SamplingLagModel.lean 1 declarations
SamplingMoments.lean 39 declarations
SamplingRateEnvelope.lean 8 declarations
SamplingSkeleton.lean 19 declarations
SamplingTransfer.lean 27 declarations
ScaledCoefficientLaw.lean 1 declarations
ScaledPeriodicMeans.lean 4 declarations
ScaledSamplingComparison.lean 1 declarations
SelectedCoefficientRegularity.lean 2 declarations
ShortAffineBudget.lean 1 declarations
ShortAffineDyadic.lean 2 declarations
ShortAffineLimit.lean 1 declarations
ShortIntervalConsequences.lean 21 declarations
ShortLagRemoval.lean 5 declarations
ShortLagSet.lean 5 declarations
ShortLengthComparison.lean 4 declarations
ShortWindowEnergy.lean 7 declarations
SignedCoefficientSums.lean 7 declarations
SignedLagMass.lean 3 declarations
SingleCoefficientIndicators.lean 4 declarations
SingleCoefficientTilt.lean 3 declarations
SingularSeriesPeriodic.lean 5 declarations
SlowPeriodicMean.lean 3 declarations
SmallArcCoefficientLaw.lean 1 declarations
SmallArcEnergy.lean 2 declarations
SmallMajorCoefficient.lean 2 declarations
SparseCofactorSampling.lean 1 declarations
SubsequencePositiveBlocks.lean 1 declarations
SubsequencePositiveEnergy.lean 1 declarations
SubsetWindowEntropy.lean 2 declarations
TermCoefficientBound.lean 1 declarations
TiltedCoefficient.lean 12 declarations
TiltedCoefficientTriple.lean 3 declarations
TruncatedCoefficientVariation.lean 2 declarations
TwistedExceptionalEnergy.lean 1 declarations
TwistedInterpolantShort.lean 1 declarations
TypicalShortEnergy.lean 5 declarations
UniformCoefficientFreeze.lean 2 declarations
UniformHyperbolaBlock.lean 2 declarations
UnitBinEnergy.lean 2 declarations
UnitProgressionBinShort.lean 4 declarations
WeightedCoefficientLaw.lean 2 declarations
WeightedGeometricCoefficient.lean 1 declarations