OAI/NumberTheory/DirichletL/Hecke/
1389 declarations, 0 contain sorry, 0 declared as axioms; 182 files
Files
- Boundary.lean 40 declarations
- BoundaryIntegration.lean 5 declarations
- CharacterAnalytic.lean 11 declarations
- CommonProbe.lean 6 declarations
- ConditionalNonvanishing.lean 1 declarations
- Conjugation.lean 3 declarations
- Coordinates.lean 14 declarations
- DeletionBounds.lean 15 declarations
- DeletionDerivative.lean 3 declarations
- DeletionReciprocal.lean 2 declarations
- DetectorAdaptiveCutoff.lean 5 declarations
- DetectorAmplitudeFirst.lean 9 declarations
- DetectorBatch.lean 7 declarations
- DetectorBatchCount.lean 1 declarations
- DetectorBranchBudget.lean 7 declarations
- DetectorBudget.lean 2 declarations
- DetectorClassBudget.lean 4 declarations
- DetectorCoefficientBounds.lean 6 declarations
- DetectorCoefficientTransfer.lean 5 declarations
- DetectorCommonFrequency.lean 2 declarations
- DetectorCountFromMoments.lean 1 declarations
- DetectorDyadicActual.lean 3 declarations
- DetectorDyadicBridge.lean 11 declarations
- DetectorDyadicCutoff.lean 7 declarations
- DetectorDyadicGeometry.lean 5 declarations
- DetectorDyadicLengths.lean 4 declarations
- DetectorDyadicProfiles.lean 14 declarations
- DetectorDyadicSupport.lean 7 declarations
- DetectorDynamicSelection.lean 3 declarations
- DetectorFamilyInclusion.lean 5 declarations
- DetectorFiberEnergy.lean 2 declarations
- DetectorFiberPartition.lean 7 declarations
- DetectorFiberSpikes.lean 1 declarations
- DetectorFinite.lean 10 declarations
- DetectorFixedAmplitudeCount.lean 3 declarations
- DetectorFourier.lean 4 declarations
- DetectorFourierActual.lean 5 declarations
- DetectorFourierSeparation.lean 6 declarations
- DetectorFourierWitness.lean 9 declarations
- DetectorFrequency.lean 1 declarations
- DetectorFrequencyTail.lean 2 declarations
- DetectorHighBatchCount.lean 1 declarations
- DetectorHighCount.lean 1 declarations
- DetectorInverseFiberCount.lean 2 declarations
- DetectorLower.lean 3 declarations
- DetectorNoSlotInverseCount.lean 1 declarations
- DetectorNoSlotPlainCount.lean 1 declarations
- DetectorNormalized.lean 4 declarations
- DetectorPartition.lean 10 declarations
- DetectorPhysicalBins.lean 1 declarations
- DetectorPhysicalSelection.lean 4 declarations
- DetectorPlainFiberCount.lean 1 declarations
- DetectorPrimeFamily.lean 11 declarations
- DetectorProfiles.lean 13 declarations
- DetectorProfilesBounds.lean 6 declarations
- DetectorProfilesCutoffs.lean 6 declarations
- DetectorProfilesUniform.lean 3 declarations
- DetectorRawBranches.lean 6 declarations
- DetectorRawFiber.lean 8 declarations
- DetectorRelativePrime.lean 4 declarations
- DetectorRowCount.lean 4 declarations
- DetectorRowCountCrossing.lean 23 declarations
- DetectorRowCountEndpoint.lean 7 declarations
- DetectorRowCountOptimization.lean 1 declarations
- DetectorRowSpecialization.lean 2 declarations
- DetectorRowwise.lean 4 declarations
- DetectorRowwiseChain.lean 1 declarations
- DetectorRowwiseMarked.lean 1 declarations
- DetectorRowwisePlain.lean 2 declarations
- DetectorRowwisePolynomial.lean 9 declarations
- DetectorSaturation.lean 3 declarations
- DetectorSimultaneous.lean 2 declarations
- DetectorSimultaneousSupport.lean 2 declarations
- DetectorSlotSelection.lean 4 declarations
- DetectorSupportedWitness.lean 3 declarations
- DetectorTail.lean 19 declarations
- DetectorWitnessArithmetic.lean 8 declarations
- DetectorWitnessRows.lean 8 declarations
- DetectorZeros.lean 18 declarations
- Dirichlet.lean 17 declarations
- Dyadic.lean 15 declarations
- DyadicBounded.lean 1 declarations
- DyadicBuffered.lean 3 declarations
- DyadicCentralBudget.lean 5 declarations
- DyadicContour.lean 9 declarations
- DyadicControl.lean 2 declarations
- DyadicEstimates.lean 3 declarations
- DyadicJoins.lean 2 declarations
- DyadicLossBudget.lean 5 declarations
- DyadicMellin.lean 7 declarations
- DyadicPointwise.lean 3 declarations
- DyadicReflectedControl.lean 3 declarations
- DyadicReflectedFamily.lean 4 declarations
- DyadicReflectedPointwise.lean 1 declarations
- DyadicReflection.lean 5 declarations
- DyadicScale.lean 6 declarations
- DyadicScaled.lean 1 declarations
- DyadicScaledReflection.lean 1 declarations
- DyadicSource.lean 1 declarations
- DyadicTailBudget.lean 3 declarations
- Euler.lean 7 declarations
- EulerLog.lean 31 declarations
- ExceptionalRows.lean 6 declarations
- Family.lean 18 declarations
- FamilySeries.lean 4 declarations
- FiniteDeletion.lean 14 declarations
- FiniteEulerFactors.lean 30 declarations
- IdealBridge.lean 19 declarations
- IdealOperations.lean 4 declarations
- InverseAmplificationAggregate.lean 5 declarations
- InverseAmplificationBudget.lean 8 declarations
- InverseAmplificationColumn.lean 3 declarations
- InverseAmplificationConjugation.lean 9 declarations
- InverseAmplificationEndpoint.lean 1 declarations
- InverseAmplificationEnergy.lean 2 declarations
- InverseAmplificationFamily.lean 8 declarations
- InverseAmplificationMask.lean 3 declarations
- InverseAmplificationPowers.lean 4 declarations
- InverseAmplificationPrimePool.lean 5 declarations
- InverseAmplificationProfiles.lean 4 declarations
- InverseAmplificationRaw.lean 2 declarations
- InverseAmplificationRows.lean 9 declarations
- InverseAmplificationRowwise.lean 4 declarations
- InverseAmplificationScale.lean 8 declarations
- InverseAmplificationScaleSup.lean 5 declarations
- LocalEulerIdentities.lean 41 declarations
- LocalRamification.lean 6 declarations
- LogDerivative.lean 8 declarations
- Logarithmic.lean 5 declarations
- LogarithmicActual.lean 6 declarations
- LogarithmicInput.lean 16 declarations
- MaskDescent.lean 5 declarations
- MellinIdentity.lean 5 declarations
- MobiusEulerCorrection.lean 72 declarations
- ModulusRefinement.lean 7 declarations
- Nonvanishing.lean 3 declarations
- NormFiberCharacters.lean 40 declarations
- Operations.lean 6 declarations
- Origin.lean 10 declarations
- Presentation.lean 14 declarations
- PrimeAmplitudeActual.lean 1 declarations
- PrimeAmplitudeBins.lean 9 declarations
- PrimeAmplitudeScale.lean 2 declarations
- PrimeAnnular.lean 7 declarations
- PrimeBin.lean 1 declarations
- PrimeDyadic.lean 13 declarations
- PrimeDyadicBuffered.lean 3 declarations
- PrimeDyadicContour.lean 8 declarations
- PrimeDyadicControl.lean 4 declarations
- PrimeDyadicEstimates.lean 4 declarations
- PrimeDyadicEuler.lean 3 declarations
- PrimeDyadicScale.lean 2 declarations
- PrimeDyadicScaled.lean 1 declarations
- PrimeDyadicSource.lean 1 declarations
- PrimeExtraction.lean 38 declarations
- PrimeNonprincipal.lean 4 declarations
- PrimePowers.lean 8 declarations
- PrimeRay.lean 6 declarations
- PrimeRow.lean 7 declarations
- PrimeScale.lean 4 declarations
- Primitive.lean 17 declarations
- PrimitiveSupremum.lean 7 declarations
- PrincipalResidue.lean 3 declarations
- PrincipalStrip.lean 14 declarations
- RayFamily.lean 9 declarations
- RayPrimes.lean 5 declarations
- RayQuotient.lean 9 declarations
- Reciprocal.lean 13 declarations
- ReciprocalBound.lean 3 declarations
- ReciprocalGrowth.lean 3 declarations
- RowClosure.lean 21 declarations
- RowNonprincipal.lean 5 declarations
- Signal.lean 22 declarations
- SignalBounds.lean 2 declarations
- SignalIdentity.lean 10 declarations
- SignalShift.lean 6 declarations
- Strip.lean 28 declarations
- StripActual.lean 12 declarations
- Theta.lean 27 declarations
- ThetaSeries.lean 6 declarations
- UnitRows.lean 10 declarations
- ZeroSupremum.lean 12 declarations