`OAI/NumberTheory/DirichletL/Detector/`

2557 declarations, 0 contain sorry, 0 declared as axioms; 414 files

Files

Basic.lean 6 declarations
Calibration.lean 17 declarations
CalibrationCRT.lean 3 declarations
CalibrationCancellation.lean 2 declarations
CalibrationFourier.lean 7 declarations
CalibrationRemoval.lean 7 declarations
CalibrationSupport.lean 3 declarations
CanonicalPhysicalRows.lean 4 declarations
CanonicalSlots.lean 20 declarations
CentralAllSlots.lean 2 declarations
CentralBranchProduct.lean 2 declarations
CentralClassArithmetic.lean 2 declarations
CentralClassPartition.lean 3 declarations
CentralCubeNorm.lean 3 declarations
CentralDyadicWeight.lean 6 declarations
CentralExponent.lean 12 declarations
CentralMixedMargins.lean 4 declarations
CentralPrimeSum.lean 1 declarations
CentralRepeatedChoices.lean 4 declarations
CentralRepeatedProduct.lean 4 declarations
CentralRepeatedSubset.lean 1 declarations
CentralRepeatedSum.lean 1 declarations
CoefficientDirect.lean 3 declarations
CompensatedRows.lean 4 declarations
CompensatedTriple.lean 5 declarations
Compensation.lean 3 declarations
CompensationActual.lean 6 declarations
Completed.lean 21 declarations
CompletedCRTPhase.lean 8 declarations
CompletedCoefficient.lean 4 declarations
CongruenceScalar.lean 8 declarations
ContourShear.lean 5 declarations
CorrectionBounds.lean 4 declarations
CubicGaussCRT.lean 4 declarations
DetectorBatch.lean 6 declarations
DetectorInverseFields.lean 2 declarations
DetectorInverseMarkedField.lean 1 declarations
DetectorInverseRawField.lean 3 declarations
DetectorMomentData.lean 5 declarations
DetectorMomentFiberGates.lean 2 declarations
DetectorMomentGates.lean 8 declarations
DetectorMomentPrimeGeometry.lean 10 declarations
DetectorPlainMarkedFineField.lean 2 declarations
DetectorPlainUnmarkedField.lean 5 declarations
DetectorPlainUnmarkedRestrictedField.lean 2 declarations
Euler.lean 4 declarations
EulerCoordinates.lean 14 declarations
EulerFinsupp.lean 4 declarations
EulerHolomorphic.lean 5 declarations
EulerMarked.lean 6 declarations
EulerRegion.lean 2 declarations
FinalAssembly.lean 4 declarations
FinalAssemblyArithmetic.lean 1 declarations
FinalAssemblyCertifiedBands.lean 9 declarations
FinalAssemblyChosenData.lean 8 declarations
FinalAssemblyClass.lean 1 declarations
FinalAssemblyCollected.lean 1 declarations
FinalAssemblyCountParameters.lean 2 declarations
FinalAssemblyData.lean 8 declarations
FinalAssemblyFixedHigh.lean 1 declarations
FinalAssemblyHigh.lean 1 declarations
FinalAssemblyIntegral.lean 1 declarations
FinalAssemblyMomentInput.lean 5 declarations
FinalAssemblyMomentMono.lean 3 declarations
FinalAssemblyNormalized.lean 1 declarations
FinalAssemblySource.lean 4 declarations
FinalAssemblySourceCount.lean 3 declarations
FinalAssemblyUnconditional.lean 3 declarations
FiniteProductBounds.lean 47 declarations
FiniteProductX.lean 14 declarations
FixedEuler.lean 8 declarations
FrequencySupport.lean 8 declarations
Gauss.lean 10 declarations
GaussValuation.lean 2 declarations
GaussianCommon.lean 1 declarations
GaussianCompensation.lean 9 declarations
GaussianCompletedSlots.lean 7 declarations
GaussianCompletion.lean 6 declarations
GaussianCoupled.lean 5 declarations
GaussianCrude.lean 5 declarations
GaussianDecomposition.lean 5 declarations
GaussianDensityBudget.lean 5 declarations
GaussianDerivative.lean 8 declarations
GaussianFlow.lean 6 declarations
GaussianLogWindow.lean 7 declarations
GaussianLow.lean 2 declarations
GaussianMellin.lean 6 declarations
GaussianPartition.lean 13 declarations
GaussianPhysicalMass.lean 3 declarations
GaussianPhysicalTail.lean 5 declarations
GaussianPhysicalTuple.lean 3 declarations
GaussianRemoteRows.lean 6 declarations
GaussianSeminorm.lean 13 declarations
GaussianSlots.lean 9 declarations
GaussianSubset.lean 7 declarations
GaussianSummation.lean 2 declarations
GaussianTailBudget.lean 7 declarations
GaussianTuple.lean 7 declarations
GaussianWindows.lean 7 declarations
GlobalCorrection.lean 16 declarations
GlobalHolomorphic.lean 10 declarations
GlobalRegion.lean 1 declarations
GramAnnularCount.lean 3 declarations
GramAnnularLattice.lean 11 declarations
GramBound.lean 1 declarations
GramCanonical.lean 18 declarations
GramCanonicalBlock.lean 2 declarations
GramCanonicalSource.lean 2 declarations
GramCanonicalTrivial.lean 1 declarations
GramClassification.lean 7 declarations
GramCommonActual.lean 4 declarations
GramCommonEnergy.lean 4 declarations
GramCommonLinear.lean 3 declarations
GramCommonParam.lean 14 declarations
GramCommonPhase.lean 3 declarations
GramCommonSource.lean 5 declarations
GramCommonSum.lean 2 declarations
GramEnergyNonzero.lean 2 declarations
GramFiniteGcd.lean 6 declarations
GramFrequency.lean 3 declarations
GramFrequencyConvergence.lean 2 declarations
GramFrequencyMass.lean 3 declarations
GramFrequencySummation.lean 7 declarations
GramGcd.lean 16 declarations
GramGcdSource.lean 5 declarations
GramGlobalExtension.lean 5 declarations
GramIdealDilation.lean 7 declarations
GramIdealMass.lean 3 declarations
GramIdealSummation.lean 9 declarations
GramInfiniteEstimate.lean 2 declarations
GramJoint.lean 5 declarations
GramJointConstruction.lean 46 declarations
GramJointFixed.lean 8 declarations
GramJointMean.lean 4 declarations
GramJointPeriod.lean 3 declarations
GramJointProfile.lean 21 declarations
GramJointSource.lean 2 declarations
GramLatticeDecay.lean 27 declarations
GramLatticeSource.lean 3 declarations
GramLatticeWindow.lean 7 declarations
GramLocalExtension.lean 6 declarations
GramMean.lean 3 declarations
GramMeanLift.lean 1 declarations
GramMobiusLattice.lean 2 declarations
GramMobiusPool.lean 5 declarations
GramNonexceptionalBlock.lean 1 declarations
GramNonzeroFrequency.lean 4 declarations
GramNumerator.lean 6 declarations
GramPeriodicPoisson.lean 109 declarations
GramPhysicalScale.lean 8 declarations
GramPrefactor.lean 4 declarations
GramPrimaryLattice.lean 7 declarations
GramPrimeSeparation.lean 3 declarations
GramResidue.lean 1 declarations
GramScaleLoss.lean 2 declarations
GramShell.lean 4 declarations
GramSourceBlock.lean 2 declarations
GramSourceDivisors.lean 8 declarations
GramSourceEstimate.lean 1 declarations
GramTruncation.lean 6 declarations
GramWeightedFrequency.lean 3 declarations
GramWindowGcd.lean 3 declarations
GramWindowMobius.lean 4 declarations
HighAbsolute.lean 8 declarations
HighDeletion.lean 6 declarations
HighEuler.lean 4 declarations
HighEulerGeneral.lean 2 declarations
HighEulerLocal.lean 4 declarations
HighEulerRational.lean 4 declarations
HighExcludedEuler.lean 8 declarations
HighExcludedLocal.lean 5 declarations
HighLFactorization.lean 1 declarations
HighRowsActual.lean 2 declarations
HighRowsCentralBase.lean 2 declarations
HighRowsCentralCancellation.lean 1 declarations
HighRowsCentralDefect.lean 2 declarations
HighRowsCentralEntry.lean 2 declarations
HighRowsCentralError.lean 1 declarations
HighRowsCentralLower.lean 2 declarations
HighRowsCentralQuotient.lean 2 declarations
HighRowsCentralRamified.lean 2 declarations
HighRowsCentralRamifiedQuotient.lean 2 declarations
HighRowsCentralSelected.lean 1 declarations
HighRowsCentralStrict.lean 2 declarations
HighRowsCentralStrictSelected.lean 3 declarations
HighRowsCentralTerms.lean 1 declarations
HighRowsClosed.lean 6 declarations
HighRowsDiagonal.lean 3 declarations
HighRowsEuler.lean 3 declarations
HighRowsExcluded.lean 1 declarations
HighRowsFamilies.lean 6 declarations
HighRowsFiniteBounds.lean 5 declarations
HighRowsFirstHolomorphic.lean 7 declarations
HighRowsFirstNeighborhood.lean 1 declarations
HighRowsFirstRamified.lean 5 declarations
HighRowsFirstRegion.lean 1 declarations
HighRowsFirstTerms.lean 3 declarations
HighRowsHolomorphic.lean 7 declarations
HighRowsLocal.lean 8 declarations
HighRowsMultiplicative.lean 3 declarations
HighRowsPrime.lean 8 declarations
HighRowsRamified.lean 3 declarations
HighRowsRecurrence.lean 3 declarations
HighRowsRegion.lean 2 declarations
HighRowsScalar.lean 4 declarations
HighRowsScalarBounds.lean 4 declarations
HighRowsSelectedActual.lean 3 declarations
HighRowsSelectedBound.lean 2 declarations
HighRowsSelectedCancellation.lean 1 declarations
HighRowsSelectedError.lean 2 declarations
HighRowsSelectedRamified.lean 5 declarations
HighRowsSelectedTerms.lean 2 declarations
HighRowsSelectedUnramified.lean 6 declarations
HighRowsSeries.lean 3 declarations
HighRowsSharpScalar.lean 5 declarations
HighRowsSummability.lean 6 declarations
HighRowsTail.lean 4 declarations
HighRowsTermBounds.lean 3 declarations
HighRowsUnramified.lean 4 declarations
HighRowsWeights.lean 7 declarations
HighRowsZero.lean 5 declarations
HighSeries.lean 7 declarations
HighValuations.lean 13 declarations
IdealFactorization.lean 22 declarations
IdealLocalEuler.lean 9 declarations
IdealMultiplicative.lean 10 declarations
IdealUnit.lean 5 declarations
InitialFubini.lean 1 declarations
InitialIntegral.lean 6 declarations
InitialMajorant.lean 9 declarations
InitialProduct.lean 1 declarations
InitialRows.lean 6 declarations
InitialScales.lean 6 declarations
InitialSubseries.lean 4 declarations
LiftedFourier.lean 8 declarations
Local.lean 12 declarations
LocalPhysical.lean 8 declarations
LocalSeries.lean 15 declarations
LocalSummation.lean 16 declarations
LocalUnitFrequency.lean 13 declarations
LocalWeights.lean 10 declarations
LowActualEnergies.lean 8 declarations
LowActualIdealLists.lean 12 declarations
LowActualReflectedEnergy.lean 3 declarations
LowCauchy.lean 5 declarations
LowCentralGeometry.lean 6 declarations
LowCentralTuple.lean 2 declarations
LowColumnBounds.lean 6 declarations
LowCommonBound.lean 3 declarations
LowCompensation.lean 4 declarations
LowCompletion.lean 6 declarations
LowCutoff.lean 10 declarations
LowElementRows.lean 19 declarations
LowGaussEnergy.lean 4 declarations
LowGaussianCentral.lean 2 declarations
LowGaussianDyad.lean 4 declarations
LowGaussianRemote.lean 5 declarations
LowGaussianSum.lean 2 declarations
LowGramApplied.lean 1 declarations
LowGramArithmetic.lean 6 declarations
LowGramDiagonal.lean 4 declarations
LowGramExceptional.lean 5 declarations
LowGramFixedCoefficient.lean 8 declarations
LowGramHeight.lean 7 declarations
LowGramIntegrated.lean 2 declarations
LowGramPoisson.lean 3 declarations
LowGramProfile.lean 9 declarations
LowGramScale.lean 4 declarations
LowInverseEnergy.lean 5 declarations
LowInverseNormalize.lean 2 declarations
LowMellin.lean 5 declarations
LowMellinFubini.lean 5 declarations
LowNominalEnergy.lean 1 declarations
LowNominalGeometry.lean 10 declarations
LowNormalized.lean 1 declarations
LowOriginalPools.lean 2 declarations
LowPeriod.lean 12 declarations
LowPeriodFilter.lean 12 declarations
LowPeriodSupport.lean 3 declarations
LowPhysicalInverseBound.lean 1 declarations
LowPrimeFamily.lean 8 declarations
LowPuncture.lean 6 declarations
LowRay.lean 12 declarations
LowRayAmplitude.lean 5 declarations
LowReflectedExponent.lean 3 declarations
LowReflectedLength.lean 1 declarations
LowRemoteMass.lean 5 declarations
LowRow.lean 6 declarations
LowRowMellin.lean 16 declarations
LowSelectedBound.lean 3 declarations
LowSelectedSum.lean 4 declarations
LowSeparated.lean 5 declarations
LowSlotMarks.lean 9 declarations
LowSlotPolynomial.lean 7 declarations
LowSlotScales.lean 4 declarations
LowSlotSplit.lean 11 declarations
LowSlotWeights.lean 7 declarations
LowSourceScales.lean 7 declarations
LowTruePeriodPuncture.lean 16 declarations
LowTupleGram.lean 5 declarations
LowUnselectedMass.lean 3 declarations
LowWindowBound.lean 2 declarations
MarkedEuler.lean 7 declarations
MarkedLocal.lean 5 declarations
MarkedProduct.lean 3 declarations
MarkedRational.lean 2 declarations
MarkedValuations.lean 8 declarations
MellinBoundary.lean 69 declarations
MellinGuarded.lean 4 declarations
MellinPoisson.lean 2 declarations
MellinPowers.lean 1 declarations
MellinScaling.lean 4 declarations
MixedFubini.lean 8 declarations
NestedMellin.lean 3 declarations
NormalProduct.lean 7 declarations
OuterIndex.lean 2 declarations
OuterMellin.lean 2 declarations
PairPhase.lean 3 declarations
Phase.lean 9 declarations
PhaseCancellation.lean 6 declarations
PhasePowers.lean 13 declarations
Physical.lean 16 declarations
PhysicalAnalytic.lean 5 declarations
PhysicalCRT.lean 8 declarations
PhysicalCoefficient.lean 12 declarations
PhysicalCoefficientScaling.lean 1 declarations
PhysicalCrudeMass.lean 8 declarations
PhysicalFourier.lean 8 declarations
PhysicalLocalEuler.lean 5 declarations
PhysicalMellinCoefficient.lean 2 declarations
PhysicalNorms.lean 4 declarations
PhysicalPoisson.lean 4 declarations
PhysicalRadial.lean 2 declarations
PhysicalRawIntegral.lean 3 declarations
PhysicalReopen.lean 3 declarations
PhysicalRows.lean 11 declarations
PrimeConstants.lean 10 declarations
PrimePhase.lean 5 declarations
PrimePower.lean 10 declarations
PrincipalContours.lean 65 declarations
PrincipalEulerIdentity.lean 7 declarations
PrincipalInput.lean 2 declarations
PrincipalNormalized.lean 2 declarations
PrincipalNormalizer.lean 3 declarations
PrincipalPhysical.lean 7 declarations
PrincipalPhysicalRemainder.lean 1 declarations
PrincipalProduct.lean 11 declarations
PrincipalRemainderBounds.lean 25 declarations
PrincipalResidueActual.lean 3 declarations
PrincipalSplit.lean 6 declarations
PrincipalTransport.lean 29 declarations
RadialExchange.lean 4 declarations
RadialIdentity.lean 4 declarations
RadialMellin.lean 35 declarations
RadialSpectral.lean 4 declarations
RawArithmetic.lean 3 declarations
RawIndexGrouping.lean 5 declarations
RawMellinTerm.lean 2 declarations
RawNestedJoin.lean 2 declarations
RawNesting.lean 5 declarations
RawPhysicalIntegral.lean 6 declarations
RawRadialJoin.lean 3 declarations
RawSourceIntegral.lean 7 declarations
RayCharacterFamily.lean 9 declarations
RayNormalization.lean 4 declarations
RayPhaseAmplitude.lean 5 declarations
RayPhaseBins.lean 1 declarations
RayPoolDisjoint.lean 3 declarations
RayPoolGood.lean 5 declarations
RayPoolThresholds.lean 2 declarations
RaySlots.lean 7 declarations
ReciprocityCRT.lean 2 declarations
Row.lean 10 declarations
RowAnalytic.lean 9 declarations
RowInterchange.lean 6 declarations
RowRadicalConductor.lean 22 declarations
RowReflectedAllocation.lean 14 declarations
ScalarTable.lean 4 declarations
ScalarVanishing.lean 2 declarations
SelectedPrimeIndexed.lean 1 declarations
SelectedPrimeSums.lean 7 declarations
Sextic.lean 2 declarations
SixthArray.lean 2 declarations
SixthDecomposition.lean 6 declarations
SixthFrequency.lean 6 declarations
SixthMask.lean 3 declarations
SixthSeries.lean 6 declarations
SourceAmplitudeClasses.lean 1 declarations
SourceBatch.lean 1 declarations
SourceBounds.lean 2 declarations
SourceCoefficient.lean 4 declarations
SourceExclusions.lean 5 declarations
SourceIntegrable.lean 1 declarations
SourceLocal.lean 7 declarations
SourcePrime.lean 7 declarations
SourcePrimeFactor.lean 2 declarations
SourceTriple.lean 4 declarations
SpectralCoefficient.lean 4 declarations
SpectralCompensation.lean 3 declarations
SpectralPoisson.lean 2 declarations
SpectralSeparation.lean 5 declarations
SpectralSupport.lean 2 declarations
SpectralWeights.lean 8 declarations
Transformed.lean 3 declarations
TupleKernel.lean 3 declarations
TupleMellin.lean 3 declarations
TuplePrime.lean 3 declarations
TuplePrincipal.lean 1 declarations
TupleProducts.lean 3 declarations
TupleRows.lean 5 declarations
TupleScaling.lean 2 declarations
UnramifiedScalar.lean 5 declarations
Windows.lean 4 declarations
ZeroIndex.lean 5 declarations