All.lean`

GitHub source file

0 declarations, 0 contain sorry, 0 declared as axioms

This file declares nothing itself. It gathers the 152 imports below, so a file that imports it gets all of them.

Imports

OAI.NumberTheory.Ostmann.Arithmetic.ArithmeticPatternNormRate
OAI.NumberTheory.Ostmann.Arithmetic.ArithmeticSlotProducts
OAI.NumberTheory.Ostmann.Arithmetic.BulkKernelCellError
OAI.NumberTheory.Ostmann.Arithmetic.BulkLogPairComparison
OAI.NumberTheory.Ostmann.Arithmetic.BulkLogWeightedCellComparison
OAI.NumberTheory.Ostmann.Arithmetic.BulkPageProjection
OAI.NumberTheory.Ostmann.Arithmetic.BulkStatisticBound
OAI.NumberTheory.Ostmann.Arithmetic.CRTInternalLines
OAI.NumberTheory.Ostmann.Arithmetic.CRTLineProbabilities
OAI.NumberTheory.Ostmann.Arithmetic.CompensatedHistoryRate
OAI.NumberTheory.Ostmann.Arithmetic.ForwardHistoryRate
OAI.NumberTheory.Ostmann.Arithmetic.GlobalHistoryPairDecay
OAI.NumberTheory.Ostmann.Arithmetic.HarmonicGraphCancellation
OAI.NumberTheory.Ostmann.Arithmetic.IdealSmoothHistoryNorm
OAI.NumberTheory.Ostmann.Arithmetic.JointLineComparison
OAI.NumberTheory.Ostmann.Arithmetic.LeafFrequencySupport
OAI.NumberTheory.Ostmann.Arithmetic.LeafModulusRanges
OAI.NumberTheory.Ostmann.Arithmetic.MovingAmplitudeFullHarmonicCost
OAI.NumberTheory.Ostmann.Arithmetic.MovingAmplitudeStep
OAI.NumberTheory.Ostmann.Arithmetic.MovingArithmeticPageDeletion
OAI.NumberTheory.Ostmann.Arithmetic.MovingArithmeticScale
OAI.NumberTheory.Ostmann.Arithmetic.MovingBulkLogVariation
OAI.NumberTheory.Ostmann.Arithmetic.MovingBulkSupport
OAI.NumberTheory.Ostmann.Arithmetic.MovingCompleteIntegerCells
OAI.NumberTheory.Ostmann.Arithmetic.MovingConstructedProductStep
OAI.NumberTheory.Ostmann.Arithmetic.MovingEarlyTemplateCaps
OAI.NumberTheory.Ostmann.Arithmetic.MovingFieldBulkComparison
OAI.NumberTheory.Ostmann.Arithmetic.MovingFirstNodeWindows
OAI.NumberTheory.Ostmann.Arithmetic.MovingFrequencyEnergy
OAI.NumberTheory.Ostmann.Arithmetic.MovingFullPair
OAI.NumberTheory.Ostmann.Arithmetic.MovingJointSquareLoss
OAI.NumberTheory.Ostmann.Arithmetic.MovingMixedResidueRate
OAI.NumberTheory.Ostmann.Arithmetic.MovingNormalizedEnergyBound
OAI.NumberTheory.Ostmann.Arithmetic.MovingOriginalEnergyBound
OAI.NumberTheory.Ostmann.Arithmetic.MovingOriginalGiantComparison
OAI.NumberTheory.Ostmann.Arithmetic.MovingOriginalLogGiantWeight
OAI.NumberTheory.Ostmann.Arithmetic.MovingOriginalPair
OAI.NumberTheory.Ostmann.Arithmetic.MovingPairAdaptiveSupport
OAI.NumberTheory.Ostmann.Arithmetic.MovingPatternGoodMaskedPriors
OAI.NumberTheory.Ostmann.Arithmetic.MovingPatternHalfLogTwoPrimeIntegratedRate
OAI.NumberTheory.Ostmann.Arithmetic.MovingPatternLines
OAI.NumberTheory.Ostmann.Arithmetic.MovingPatternLogLeafBridge
OAI.NumberTheory.Ostmann.Arithmetic.MovingPatternLogTwoPrimeIntegratedRate
OAI.NumberTheory.Ostmann.Arithmetic.MovingPatternMainGain
OAI.NumberTheory.Ostmann.Arithmetic.MovingPatternSameNormArithmetic
OAI.NumberTheory.Ostmann.Arithmetic.MovingPatternSignedArithmetic
OAI.NumberTheory.Ostmann.Arithmetic.MovingPatternSignedMajorant
OAI.NumberTheory.Ostmann.Arithmetic.MovingPatternWholeShellArithmetic
OAI.NumberTheory.Ostmann.Arithmetic.MovingPatternWindowWeightedWholeShell
OAI.NumberTheory.Ostmann.Arithmetic.MovingPatternWindowWholeShellArithmetic
OAI.NumberTheory.Ostmann.Arithmetic.MovingPatternWordArithmetic
OAI.NumberTheory.Ostmann.Arithmetic.MovingPrimeInternalNorm
OAI.NumberTheory.Ostmann.Arithmetic.MovingPrimeResidueRate
OAI.NumberTheory.Ostmann.Arithmetic.MovingRealWeight
OAI.NumberTheory.Ostmann.Arithmetic.MovingRegularOuterComparison
OAI.NumberTheory.Ostmann.Arithmetic.MovingSampleDiagonalRate
OAI.NumberTheory.Ostmann.Arithmetic.MovingSelectedDiagonalDecay
OAI.NumberTheory.Ostmann.Arithmetic.MovingSelectedEarlyDiagonalDecay
OAI.NumberTheory.Ostmann.Arithmetic.MovingSelectedPhaseStatistic
OAI.NumberTheory.Ostmann.Arithmetic.MovingSelectedPrimeEnergy
OAI.NumberTheory.Ostmann.Arithmetic.MovingSelectedPrimeStatistic
OAI.NumberTheory.Ostmann.Arithmetic.MovingSelectedStatistic
OAI.NumberTheory.Ostmann.Arithmetic.MovingSeparatedOuterComparison
OAI.NumberTheory.Ostmann.Arithmetic.MovingSmoothPrimeComparison
OAI.NumberTheory.Ostmann.Arithmetic.MovingSpectatorRangeUnits
OAI.NumberTheory.Ostmann.Arithmetic.MovingSupportedOuterComparison
OAI.NumberTheory.Ostmann.Arithmetic.MovingTaggedPrimeCore
OAI.NumberTheory.Ostmann.Arithmetic.MovingTemplateMatchedBound
OAI.NumberTheory.Ostmann.Arithmetic.MovingTemplateNormalizer
OAI.NumberTheory.Ostmann.Arithmetic.NaturalScheduleEnergy
OAI.NumberTheory.Ostmann.Arithmetic.PeriodicGraphCancellation
OAI.NumberTheory.Ostmann.Arithmetic.PrimeIntegerTransfer
OAI.NumberTheory.Ostmann.Arithmetic.RangedPairAdmissibility
OAI.NumberTheory.Ostmann.Arithmetic.RecursiveArchimedeanCutoff
OAI.NumberTheory.Ostmann.Arithmetic.ReducedCoefficientLift
OAI.NumberTheory.Ostmann.Arithmetic.ResidueProductSupport
OAI.NumberTheory.Ostmann.Arithmetic.SmoothCellRate
OAI.NumberTheory.Ostmann.Characters.AnchorDiagonalTotal
OAI.NumberTheory.Ostmann.Characters.CharacterCompletedOrderOne
OAI.NumberTheory.Ostmann.Characters.CharacterFinalTop
OAI.NumberTheory.Ostmann.Characters.MixedGiantIdealization
OAI.NumberTheory.Ostmann.Characters.PrimeCorrelationBounds
OAI.NumberTheory.Ostmann.Characters.QuartetAllMajorants
OAI.NumberTheory.Ostmann.Characters.QuartetFriendlyBound
OAI.NumberTheory.Ostmann.Construction.BalancedHalfInitialAmplitude
OAI.NumberTheory.Ostmann.Construction.ConstituentFinalComparison
OAI.NumberTheory.Ostmann.Construction.ConstituentFourierBridge
OAI.NumberTheory.Ostmann.Construction.ConstituentMatchingRate
OAI.NumberTheory.Ostmann.Construction.ConstituentOriginalPair
OAI.NumberTheory.Ostmann.Construction.ConstituentSelectedProducts
OAI.NumberTheory.Ostmann.Construction.DiagonalRegularLift
OAI.NumberTheory.Ostmann.Construction.DyadicGraphHistory
OAI.NumberTheory.Ostmann.Construction.FinalArithmeticContradiction
OAI.NumberTheory.Ostmann.Construction.FinalAsymptoticComparison
OAI.NumberTheory.Ostmann.Construction.FinalEnergyCutoff
OAI.NumberTheory.Ostmann.Construction.FinalOneSidedFactor
OAI.NumberTheory.Ostmann.Construction.FiniteMatchedFubini
OAI.NumberTheory.Ostmann.Construction.FiniteScheduledTemplate
OAI.NumberTheory.Ostmann.Construction.FormulaHistoryGraphBound
OAI.NumberTheory.Ostmann.Construction.FrozenOriginalBulk
OAI.NumberTheory.Ostmann.Construction.FullPrimeRatioPair
OAI.NumberTheory.Ostmann.Construction.HarmonicMatchedEnergy
OAI.NumberTheory.Ostmann.Construction.HistoryLineComparison
OAI.NumberTheory.Ostmann.Construction.HistoryResidueData
OAI.NumberTheory.Ostmann.Construction.InitialOutsideTransform
OAI.NumberTheory.Ostmann.Construction.InitialProductSize
OAI.NumberTheory.Ostmann.Construction.InitialWordSupport
OAI.NumberTheory.Ostmann.Construction.IntegerGridSupport
OAI.NumberTheory.Ostmann.Construction.NaturalBadDiagonal
OAI.NumberTheory.Ostmann.Construction.OriginalKernelComparison
OAI.NumberTheory.Ostmann.Construction.OriginalPrimeRestoration
OAI.NumberTheory.Ostmann.Construction.PhaseGiantInitialStatistic
OAI.NumberTheory.Ostmann.Construction.PrimeCutoffFactors
OAI.NumberTheory.Ostmann.Construction.PrimeTupleDiagonal
OAI.NumberTheory.Ostmann.Construction.RepeatedPivotPhase
OAI.NumberTheory.Ostmann.Construction.ScheduledAnchorDiagonalSplit
OAI.NumberTheory.Ostmann.Construction.ScheduledAnchorEnergyBound
OAI.NumberTheory.Ostmann.Construction.ScheduledDistinctSources
OAI.NumberTheory.Ostmann.Construction.ScheduledFinalBound
OAI.NumberTheory.Ostmann.Construction.ScheduledFinalPrimeComparison
OAI.NumberTheory.Ostmann.Construction.ScheduledIntervalStep
OAI.NumberTheory.Ostmann.Construction.ScheduledNonanchorDecay
OAI.NumberTheory.Ostmann.Construction.ScheduledSpectatorComparison
OAI.NumberTheory.Ostmann.Construction.ScheduledSpectatorProducts
OAI.NumberTheory.Ostmann.Construction.SelectedAnchorEnergyBound
OAI.NumberTheory.Ostmann.Construction.SelectedAnchorSupportedEnergy
OAI.NumberTheory.Ostmann.Construction.SelectedCutoffData
OAI.NumberTheory.Ostmann.Construction.SelectedFinalNaturalPrimeComparison
OAI.NumberTheory.Ostmann.Construction.SelectedFinalPrimeComparison
OAI.NumberTheory.Ostmann.Construction.SelectedNodeSources
OAI.NumberTheory.Ostmann.Construction.SelectedNonanchorDecay
OAI.NumberTheory.Ostmann.Construction.SmoothGiantLossBudget
OAI.NumberTheory.Ostmann.Construction.SmoothMatchedPrior
OAI.NumberTheory.Ostmann.Construction.UniformInitialAmplitude
OAI.NumberTheory.Ostmann.Construction.WeightedRegularNorm
OAI.NumberTheory.Ostmann.PaperMain
OAI.NumberTheory.Ostmann.Preliminaries.Reduction
OAI.NumberTheory.Ostmann.Quadratic.CommonCenterFromApproximation
OAI.NumberTheory.Ostmann.Quadratic.KernelPopulationDiscard
OAI.NumberTheory.Ostmann.Quadratic.QuadraticIntervalInverse
OAI.NumberTheory.Ostmann.Quadratic.QuadraticNegligibleError
OAI.NumberTheory.Ostmann.Quadratic.QuadraticSecondCorrections
OAI.NumberTheory.Ostmann.Quadratic.QuadraticVaryingSmooth
OAI.NumberTheory.Ostmann.Quadratic.QuadraticWholeDivisorBound
OAI.NumberTheory.Ostmann.QuadraticCenter.RootSeparation
OAI.NumberTheory.Ostmann.Tree.PairMoment
OAI.NumberTheory.Ostmann.ZeroDensity.ActualPrincipalPNT
OAI.NumberTheory.Ostmann.ZeroDensity.ArithmeticProgressionRows
OAI.NumberTheory.Ostmann.ZeroDensity.BulkAbsoluteDensity
OAI.NumberTheory.Ostmann.ZeroDensity.CharacterContourHeights
OAI.NumberTheory.Ostmann.ZeroDensity.DensityFiniteIntegralEnergy
OAI.NumberTheory.Ostmann.ZeroDensity.NonexceptionalRieszDecay