`OAI/NumberTheory/Jacobsthal/Estimates/`

2480 declarations, 0 contain sorry, 0 declared as axioms; 197 files

Files

ActualCollisionBound.lean 32 declarations
ActualModelTargets.lean 31 declarations
ActualOddPairLink.lean 10 declarations
ActualPatternClass.lean 7 declarations
ActualPointSlopes.lean 30 declarations
ActualRegularAdmission.lean 2 declarations
ActualSourceInverse.lean 9 declarations
ActualUnalignedIncidence.lean 2 declarations
ActualUnitClasses.lean 38 declarations
AdmittedHighRemoval.lean 9 declarations
BivariateCalculus.lean 14 declarations
BivariateMonomialIndex.lean 6 declarations
BonferroniBlocks.lean 32 declarations
BoundaryGateSets.lean 23 declarations
BoundaryRadialCoefficient.lean 10 declarations
BoundaryReferenceConvergence.lean 30 declarations
BoundedLossTerms.lean 6 declarations
CandidateExceptionMass.lean 16 declarations
CandidateLengthBand.lean 1 declarations
CanonicalCorrectionSum.lean 14 declarations
CanonicalCoupledHistories.lean 14 declarations
CanonicalCrossingTail.lean 2 declarations
CanonicalKeyReference.lean 1 declarations
CanonicalPairCylinders.lean 8 declarations
CoefficientHeightChoice.lean 5 declarations
ConditionalPatternCounts.lean 20 declarations
ConsecutivePowerProjection.lean 16 declarations
CorrectionEnvelope.lean 5 declarations
CorrectionFloorRemainder.lean 34 declarations
CorrectionStateSections.lean 12 declarations
CorrectionUniformTruncation.lean 1 declarations
CountErrorRemainder.lean 1 declarations
CoupledBoundaryBounds.lean 2 declarations
DisjointBlockExpansion.lean 50 declarations
DivisibleInflection.lean 17 declarations
EffectiveAvoidance.lean 4 declarations
EffectiveNumerator.lean 5 declarations
EffectiveProgression.lean 6 declarations
EffectiveSurvivors.lean 8 declarations
EndpointSoftConclusion.lean 3 declarations
EvenInverseBands.lean 62 declarations
EvenThresholdVolume.lean 4 declarations
FactorDividesAbscissa.lean 37 declarations
FiniteMonotoneComparison.lean 3 declarations
FinitePairOccurrence.lean 5 declarations
FiniteSampleSpace.lean 7 declarations
FirstIsolatedPosition.lean 2 declarations
FirstOmissionAntichain.lean 4 declarations
FrozenSuffixData.lean 4 declarations
FullEndpointData.lean 17 declarations
FullPatternSurvivors.lean 2 declarations
FullReturnCylinders.lean 16 declarations
FundamentalBlockEstimate.lean 28 declarations
GateIterates.lean 18 declarations
GrowingFarTail.lean 14 declarations
HarmonicChangeOfVariable.lean 4 declarations
HarmonicConditioning.lean 18 declarations
HarmonicLevelBound.lean 4 declarations
HeightBlockCount.lean 5 declarations
HypotheticalIndividualUpper.lean 1 declarations
HypotheticalPairRows.lean 9 declarations
HypotheticalSubbinLower.lean 2 declarations
InitialOddDraw.lean 8 declarations
InvariantFiniteness.lean 25 declarations
InverseWeightGrowth.lean 22 declarations
IsolatedPowerOrdering.lean 1 declarations
IsolatedSourceScales.lean 1 declarations
JointModelCount.lean 7 declarations
JointReturnCylinder.lean 48 declarations
LargeGapCountErrors.lean 22 declarations
LatticeSpacing.lean 2 declarations
LineSubstitution.lean 6 declarations
LiteralSourceList.lean 1 declarations
LocalGraphIff.lean 1 declarations
LocalZeroMass.lean 2 declarations
LogSquaredDecay.lean 3 declarations
LossBounds.lean 37 declarations
LowStateHorizon.lean 16 declarations
MarginalGrowth.lean 4 declarations
MarginalProfiles.lean 10 declarations
MinorizingCostRegularity.lean 6 declarations
MovingLocalReference.lean 42 declarations
NestedDegreeBounds.lean 6 declarations
NestedPartials.lean 2 declarations
NonisolatedSelectedOccurrence.lean 1 declarations
NonquadraticZeroFree.lean 5 declarations
NonstructuredCounts.lean 16 declarations
OmissionSeries.lean 25 declarations
OmissionTiltDecay.lean 3 declarations
OnePairCost.lean 39 declarations
OriginalPairMembership.lean 4 declarations
PVIdentity.lean 11 declarations
PairCollisionCount.lean 33 declarations
PairTraceBridge.lean 7 declarations
PairedBlockContraction.lean 4 declarations
PairedCostGrouping.lean 7 declarations
PairedDeficitPositivity.lean 7 declarations
ParentProductReadout.lean 2 declarations
ParentProgression.lean 6 declarations
PatternCardGrowth.lean 2 declarations
PatternMainTerm.lean 4 declarations
PositionDensities.lean 16 declarations
PositiveGapMajorant.lean 1 declarations
PositiveProgression.lean 7 declarations
PrimitiveThreeQuarters.lean 6 declarations
PrimitiveTransfer.lean 15 declarations
PrincipalLogPower.lean 5 declarations
ProductRestriction.lean 16 declarations
RationalCandidateSets.lean 10 declarations
RawInitialEven.lean 48 declarations
RawInitialIncreasing.lean 7 declarations
RawInitialPacking.lean 11 declarations
RawReturnBound.lean 40 declarations
RawSuppliedPast.lean 17 declarations
RealCriticalPoints.lean 44 declarations
RealProgressionPoints.lean 10 declarations
ReciprocalEnvelope.lean 20 declarations
RecoveryScale.lean 33 declarations
ReducedFractions.lean 8 declarations
ReferenceCutoffRecurrence.lean 16 declarations
ReferenceIsolatedExclusion.lean 12 declarations
ReferenceLocalResidual.lean 7 declarations
ReferenceProductErrors.lean 2 declarations
ReferenceProductsBasics.lean 27 declarations
ReferenceSourceDecomposition.lean 15 declarations
ReferenceWeightedQuadrature.lean 72 declarations
RefinedDiscardBound.lean 1 declarations
RefinementRewardMargin.lean 1 declarations
RegenerativeResolvent.lean 5 declarations
RegularImplicitArc.lean 74 declarations
RegularStripBound.lean 1 declarations
RepeatedPairRow.lean 3 declarations
RepeatedPositionNeighbors.lean 1 declarations
RepeatedSelectedOccurrence.lean 1 declarations
RepeatedStepRowBound.lean 8 declarations
RepresentativeAdmission.lean 5 declarations
ReturnCompletionAlgebra.lean 6 declarations
RichLineHeights.lean 3 declarations
RichLinearFactor.lean 31 declarations
RieszCauchy.lean 5 declarations
RieszIntegrand.lean 10 declarations
RieszTermCalculus.lean 7 declarations
RootCutoffSurvivors.lean 5 declarations
RoughRecursion.lean 40 declarations
ScalarErrorBudget.lean 43 declarations
ScalarFreeGate.lean 48 declarations
ScalarTailRecurrence.lean 25 declarations
ScaledOriginalTail.lean 13 declarations
SecondLossIntegration.lean 2 declarations
SeparatedSampling.lean 4 declarations
SiegelWalfisz.lean 3 declarations
SignedCompletedPowers.lean 5 declarations
SingletonSubsetMass.lean 7 declarations
SmallModelSourceScales.lean 44 declarations
SortedRealGaps.lean 8 declarations
SourceCandidateFreezing.lean 8 declarations
SourceCenteredGap.lean 13 declarations
SourceEdgeClasses.lean 11 declarations
SourceExtensionScale.lean 16 declarations
SourceFirstCrossing.lean 3 declarations
SourceFullPatternDomination.lean 1 declarations
SourceGuardedHardCount.lean 1 declarations
SourceInitialDiscard.lean 6 declarations
SourceLargePairBound.lean 8 declarations
SourceLowRemoval.lean 4 declarations
SourceMarginalRate.lean 4 declarations
SourcePairRemainder.lean 33 declarations
SourceParentBenchmark.lean 9 declarations
SourceReferenceRemainders.lean 15 declarations
SourceRepeatedRates.lean 3 declarations
SourceRichPoints.lean 7 declarations
SourceRichSetContradiction.lean 4 declarations
SourceRootErrorLower.lean 1 declarations
SourceRootReference.lean 27 declarations
SourceSamplePopulation.lean 16 declarations
SourceSquareScale.lean 3 declarations
SourceValueSmallness.lean 1 declarations
SquarefreeHarmonic.lean 44 declarations
StandardBoundaryCoefficient.lean 5 declarations
StrongSourceFamilies.lean 3 declarations
SubbinAggregation.lean 6 declarations
SubbinScaleInheritance.lean 2 declarations
SuccessfulRewardComparison.lean 4 declarations
TwoPowerDivisibility.lean 2 declarations
TwoSidedThresholdHazard.lean 3 declarations
TwoSidedThresholdOccurrence.lean 3 declarations
TwoSidedThresholdStability.lean 4 declarations
UncappedHighRemoval.lean 2 declarations
UniformCollisionError.lean 2 declarations
UniformFailureBudget.lean 5 declarations
UniformJointModel.lean 7 declarations
UniformLower.lean 31 declarations
UnitCyclicBounds.lean 16 declarations
UnlistedLocalMass.lean 1 declarations
UnmarkedTransform.lean 3 declarations
WeightedMonotoneBound.lean 18 declarations
WeightedTwoExceptions.lean 1 declarations