OAI/NumberTheory/PrimePackets/
3475 declarations, 0 contain sorry, 0 declared as axioms; 143 files
Files
- AdelicAmbient.lean 21 declarations
- AdelicAveraging.lean 14 declarations
- AdelicBasisRepresentation.lean 4 declarations
- AdelicCanonicalAllowed.lean 7 declarations
- AdelicCanonicalAllowedStatement.lean 1 declarations
- AdelicChoices.lean 4 declarations
- AdelicCompactness.lean 105 declarations
- AdelicContinuity.lean 13 declarations
- AdelicDescent.lean 8 declarations
- AdelicDiagonalizer.lean 1 declarations
- AdelicDiagonalizerDefinitions.lean 5 declarations
- AdelicFibers.lean 4 declarations
- AdelicFinal.lean 5 declarations
- AdelicFinalStatement.lean 2 declarations
- AdelicFlow.lean 8 declarations
- AdelicFull.lean 1 declarations
- AdelicFullStatement.lean 1 declarations
- AdelicGeneralPacket.lean 2 declarations
- AdelicGeneralPacketDefinitions.lean 1 declarations
- AdelicHaarAveraging.lean 2 declarations
- AdelicHaarExistence.lean 4 declarations
- AdelicLattices.lean 10 declarations
- AdelicMonomial.lean 3 declarations
- AdelicPacket.lean 15 declarations
- AdelicPacketEquality.lean 3 declarations
- AdelicPacketPoints.lean 16 declarations
- AdelicPatch.lean 21 declarations
- AdelicProbability.lean 3 declarations
- AdelicRealIdentity.lean 6 declarations
- AdelicReduction.lean 6 declarations
- AdelicRepresentation.lean 14 declarations
- AdelicScalar.lean 2 declarations
- AmbientLeaves.lean 18 declarations
- AnalyticLogarithms.lean 26 declarations
- ArtinEuler.lean 6 declarations
- ArtinSeries.lean 28 declarations
- AtomMass.lean 15 declarations
- CharacterPairs.lean 21 declarations
- ConditionalFibers.lean 33 declarations
- ConditionalObservations.lean 10 declarations
- ConditionalOrbitEntropy.lean 5 declarations
- ConditionalProbabilityExpectation.lean 2 declarations
- ConditionalShannon.lean 6 declarations
- ConditionalSigmaEntropy.lean 3 declarations
- CongruenceLattices.lean 35 declarations
- CoordinateLattices.lean 49 declarations
- CosetMeromorphic.lean 20 declarations
- CuspMass.lean 19 declarations
- DiscriminantBounds.lean 15 declarations
- DisintegrationEntropy.lean 3 declarations
- DivisorBounds.lean 32 declarations
- EntropyGeneratingSupremum.lean 1 declarations
- EntropyMixtures.lean 30 declarations
- ErgodicDecomposition.lean 16 declarations
- FiniteGeneratingObservations.lean 12 declarations
- FrobeniusConductor.lean 5 declarations
- FrobeniusCoset.lean 13 declarations
- FrobeniusNonprincipal.lean 1 declarations
- FrobeniusOrder.lean 2 declarations
- FrobeniusSplitting.lean 6 declarations
- FrobeniusSurjective.lean 8 declarations
- FrobeniusTower.lean 1 declarations
- FunctionalEquation.lean 29 declarations
- FutureConditionalEntropy.lean 3 declarations
- FutureEntropyIncrements.lean 7 declarations
- GaussianMellin.lean 28 declarations
- GeneratingObservationEntropy.lean 2 declarations
- HaarBounds.lean 25 declarations
- HaarUniqueness.lean 27 declarations
- IdealClasses.lean 38 declarations
- IdealCoefficients.lean 34 declarations
- IdealNorms.lean 37 declarations
- IdealSupport.lean 36 declarations
- IdealThetaFlow.lean 36 declarations
- IdealThetaXi.lean 32 declarations
- IntegerEmbeddings.lean 47 declarations
- IntervalGeometry.lean 14 declarations
- IntervalSieve.lean 64 declarations
- IntrinsicLeaves.lean 31 declarations
- InverseEntropy.lean 23 declarations
- KernelEntropy.lean 21 declarations
- KernelScaling.lean 29 declarations
- KernelSupport.lean 1 declarations
- LatticeDuality.lean 22 declarations
- LatticeTheta.lean 48 declarations
- LeafAnchors.lean 34 declarations
- LeafNormalization.lean 30 declarations
- LeafPeriods.lean 31 declarations
- LeafSupport.lean 39 declarations
- LeafTransitions.lean 25 declarations
- LocalEuler.lean 19 declarations
- LocalModels.lean 50 declarations
- LocalMoments.lean 30 declarations
- Main.lean 5 imports, no declarations
- MangoldtBounds.lean 34 declarations
- MellinGrowth.lean 28 declarations
- MonomialArtin.lean 30 declarations
- MonomialSeries.lean 3 declarations
- NormalClosure.lean 31 declarations
- ObservationConditionalProbability.lean 7 declarations
- ObservationCovers.lean 17 declarations
- ObservationRefinement.lean 6 declarations
- ObservationSigmaAlgebra.lean 5 declarations
- OrbitProbability.lean 22 declarations
- PacketAlgebra.lean 251 declarations
- PacketMoments.lean 63 declarations
- PenaltyEuler.lean 20 declarations
- PeriodicTheta.lean 39 declarations
- PermutationArtin.lean 13 declarations
- PowerfulIdeals.lean 33 declarations
- PrimeFactors.lean 27 declarations
- PrimeSums.lean 18 declarations
- PrincipalUnits.lean 16 declarations
- ProjectivePeriods.lean 37 declarations
- RadialIntegrals.lean 35 declarations
- RationalLattices.lean 41 declarations
- RayCharacter.lean 39 declarations
- RayContinuation.lean 11 declarations
- RayDescent.lean 15 declarations
- RayEuler.lean 28 declarations
- RayFrobenius.lean 9 declarations
- RayRealization.lean 13 declarations
- RayUnramified.lean 18 declarations
- RealMellin.lean 18 declarations
- RootCharts.lean 50 declarations
- RootInvariance.lean 24 declarations
- RootLeaves.lean 23 declarations
- RootOverlaps.lean 38 declarations
- RootRelations.lean 34 declarations
- RootSubgroups.lean 22 declarations
- ScalingCovariance.lean 25 declarations
- ShannonEntropy.lean 26 declarations
- SieveConvolution.lean 26 declarations
- SplitEuler.lean 13 declarations
- SubquadraticGrowth.lean 22 declarations
- ThetaReflection.lean 31 declarations
- ThetaTails.lean 37 declarations
- UnitOrbitIntegrals.lean 19 declarations
- XiBoundary.lean 42 declarations
- ZeroReflection.lean 46 declarations
- ZeroSeparation.lean 20 declarations
- ZetaDerivatives.lean 21 declarations
- ZetaResidues.lean 384 declarations