`OAI/NumberTheory/DirichletL/Descent/`

1537 declarations, 0 contain sorry, 0 declared as axioms; 419 files

Files

ActiveCusp.lean 6 declarations
ActiveReflection.lean 1 declarations
ActualChildState.lean 8 declarations
ActualChildStateDepth.lean 3 declarations
ActualChildStateLabels.lean 5 declarations
ActualChildStatePuncture.lean 5 declarations
ActualChildStateRadius.lean 5 declarations
ActualChildStateSupport.lean 5 declarations
ActualChildStateTriples.lean 3 declarations
ActualDepthBudget.lean 8 declarations
ActualProfiles.lean 15 declarations
ActualSecondEnergy.lean 7 declarations
ActualSecondMeasure.lean 4 declarations
ActualSecondProfile.lean 6 declarations
ActualSecondUniform.lean 2 declarations
Basic.lean 24 declarations
Canonical.lean 6 declarations
CanonicalChildSupport.lean 7 declarations
CanonicalCompleteBudget.lean 2 declarations
CanonicalCompleteChildren.lean 1 declarations
CanonicalCompleteNormalized.lean 3 declarations
CanonicalCompleteRank.lean 1 declarations
CanonicalCompleteRankNormalized.lean 1 declarations
CanonicalCompleteState.lean 1 declarations
CanonicalEnergyExistenceData.lean 2 declarations
CanonicalLiveBinRank.lean 1 declarations
CanonicalLongAggregate.lean 2 declarations
CanonicalLongBins.lean 1 declarations
CanonicalLongCaller.lean 1 declarations
CanonicalLongCoefficient.lean 3 declarations
CanonicalLongCosts.lean 3 declarations
CanonicalLongCount.lean 1 declarations
CanonicalLongFinite.lean 1 declarations
CanonicalLongFull.lean 1 declarations
CanonicalLongGeometry.lean 3 declarations
CanonicalLongHeightBin.lean 1 declarations
CanonicalLongIntegral.lean 1 declarations
CanonicalLongKeys.lean 1 declarations
CanonicalLongNormalization.lean 4 declarations
CanonicalLongParent.lean 1 declarations
CanonicalLongSource.lean 6 declarations
CanonicalLongTotal.lean 1 declarations
CanonicalLongUniformTestBin.lean 1 declarations
CanonicalLongWeight.lean 2 declarations
CanonicalLowerMoments.lean 2 declarations
CanonicalPunctureMask.lean 6 declarations
CanonicalPunctureMaskEnergy.lean 3 declarations
CanonicalRankCapChildren.lean 2 declarations
CanonicalRankDepthParameters.lean 3 declarations
CanonicalRankEnergyMonotone.lean 1 declarations
CanonicalRankExistence.lean 4 declarations
CanonicalRankExistenceData.lean 8 declarations
CanonicalRankExistenceInduction.lean 4 declarations
CanonicalRankExistenceSuccessor.lean 1 declarations
CanonicalRankFamilyGates.lean 7 declarations
CanonicalRankMoments.lean 2 declarations
CanonicalRankMonotone.lean 3 declarations
CanonicalRankPuncture.lean 1 declarations
CanonicalReopeningHeight.lean 3 declarations
CanonicalShortFinite.lean 1 declarations
ChildCutoff.lean 10 declarations
ClippedChild.lean 3 declarations
ClippedEnergy.lean 2 declarations
ClippedFourier.lean 4 declarations
ClippedUniform.lean 1 declarations
CommonMeasure.lean 2 declarations
CompleteMarkedPool.lean 3 declarations
CompletePool.lean 3 declarations
CompletedReopening.lean 3 declarations
Completion.lean 15 declarations
CompletionSplit.lean 4 declarations
CompletionSupport.lean 3 declarations
ControlledMultiplier.lean 6 declarations
CubeSource.lean 9 declarations
CubeSupportNorm.lean 2 declarations
CuspCongruence.lean 3 declarations
Decomposition.lean 16 declarations
DensityAssembly.lean 2 declarations
DescentHeight.lean 2 declarations
DescentProfiles.lean 6 declarations
DivisorExtraction.lean 3 declarations
DivisorSum.lean 5 declarations
Dyadic.lean 7 declarations
DyadicBlock.lean 2 declarations
ExtractedGrid.lean 10 declarations
Fibers.lean 7 declarations
FirstActualEnergy.lean 5 declarations
FirstActualPriorityEnergy.lean 2 declarations
FirstActualSecondEnergy.lean 3 declarations
FirstBalancedSource.lean 4 declarations
FirstBlockEnergy.lean 5 declarations
FirstBlocks.lean 8 declarations
FirstCanonicalChildren.lean 2 declarations
FirstCanonicalEnergy.lean 4 declarations
FirstCanonicalPhysical.lean 3 declarations
FirstCanonicalTail.lean 1 declarations
FirstChildWindows.lean 3 declarations
FirstChildWindowsActual.lean 2 declarations
FirstChildWindowsCells.lean 16 declarations
FirstChildWindowsLive.lean 5 declarations
FirstChildWindowsPhysical.lean 7 declarations
FirstCommonChild.lean 5 declarations
FirstCommonColumns.lean 6 declarations
FirstCommonMeasure.lean 6 declarations
FirstCommonProfile.lean 4 declarations
FirstCoupledReindex.lean 2 declarations
FirstCutoffScale.lean 2 declarations
FirstDyadicCell.lean 3 declarations
FirstDyadicFullEnergy.lean 1 declarations
FirstDyadicLiveRadius.lean 2 declarations
FirstDyadicOriginalBranches.lean 1 declarations
FirstDyadicPriorityBudget.lean 1 declarations
FirstDyadicRadius.lean 5 declarations
FirstDyadicRetainedBudget.lean 1 declarations
FirstDyadicRetainedEnergy.lean 1 declarations
FirstDyadicTail.lean 1 declarations
FirstEnergy.lean 6 declarations
FirstFamilyEnergy.lean 5 declarations
FirstFamilySource.lean 4 declarations
FirstFamilyToSecond.lean 1 declarations
FirstFreshEnergy.lean 1 declarations
FirstFreshMeasure.lean 2 declarations
FirstFullRapidTail.lean 2 declarations
FirstGlobalPush.lean 2 declarations
FirstGlobalSourceEnergy.lean 2 declarations
FirstGlobalSourceIndex.lean 7 declarations
FirstGlobalSourcePhysical.lean 2 declarations
FirstGlobalSourceSupport.lean 7 declarations
FirstHeightBudget.lean 3 declarations
FirstLabelCellStep.lean 2 declarations
FirstLabelCellStepChildren.lean 4 declarations
FirstLabelCellStepData.lean 1 declarations
FirstLabelCellStepGates.lean 6 declarations
FirstLabelCellStepPhysicalGates.lean 5 declarations
FirstLabelCellStepSource.lean 10 declarations
FirstLiveActualStep.lean 1 declarations
FirstLiveCaps.lean 3 declarations
FirstLiveColumnScale.lean 3 declarations
FirstLiveCountBudget.lean 6 declarations
FirstLiveExponentCaps.lean 2 declarations
FirstLiveHeightStep.lean 1 declarations
FirstLiveNorms.lean 1 declarations
FirstLiveRadiusPositive.lean 1 declarations
FirstLiveStepScalars.lean 2 declarations
FirstMarkedColumns.lean 6 declarations
FirstMarkedZero.lean 1 declarations
FirstMarkedZeroSource.lean 1 declarations
FirstModeAssembly.lean 3 declarations
FirstModeChild.lean 4 declarations
FirstModeColumns.lean 6 declarations
FirstNominal.lean 3 declarations
FirstOldEnergy.lean 3 declarations
FirstOriginalProfileAssembly.lean 5 declarations
FirstOriginalProfileCellEnergy.lean 3 declarations
FirstOriginalProfileCells.lean 6 declarations
FirstOriginalProfileData.lean 10 declarations
FirstOriginalProfileFiltered.lean 1 declarations
FirstOriginalProfileIdentity.lean 3 declarations
FirstOriginalProfileLiveAggregate.lean 1 declarations
FirstOriginalProfileLiveCount.lean 2 declarations
FirstOriginalProfileLiveEnergy.lean 3 declarations
FirstOriginalProfileLiveIdentity.lean 1 declarations
FirstOriginalProfileLiveParents.lean 2 declarations
FirstOriginalProfileLivePartition.lean 7 declarations
FirstOriginalProfileLiveSource.lean 7 declarations
FirstOriginalProfileLiveSupport.lean 3 declarations
FirstOriginalProfileParents.lean 3 declarations
FirstOriginalProfilePhysical.lean 1 declarations
FirstOriginalProfileScales.lean 4 declarations
FirstOriginalProfileUniform.lean 2 declarations
FirstOriginalProfileWindows.lean 1 declarations
FirstPass.lean 3 declarations
FirstPhysicalCommon.lean 3 declarations
FirstPhysicalCutoff.lean 4 declarations
FirstPhysicalFamily.lean 4 declarations
FirstPhysicalTail.lean 1 declarations
FirstPriorityEnergy.lean 3 declarations
FirstProfileIdentity.lean 3 declarations
FirstProfileUniform.lean 25 declarations
FirstRapidPhysicalTail.lean 1 declarations
FirstRetainedFamily.lean 4 declarations
FirstRetainedPhysical.lean 3 declarations
FirstRowGeometry.lean 2 declarations
FirstSecondHeightCost.lean 11 declarations
FirstSourceSize.lean 3 declarations
FirstSourceTail.lean 1 declarations
FirstStepScalarCaps.lean 2 declarations
FirstTailAbsorption.lean 2 declarations
FirstTailAggregation.lean 3 declarations
FirstToSecond.lean 4 declarations
FirstTwoPassEnergy.lean 1 declarations
FirstTwoPassLowerRank.lean 1 declarations
FirstTwoPassParentEnergy.lean 1 declarations
FirstUnequalEnergy.lean 1 declarations
FirstUnequalMovingEnergy.lean 1 declarations
FirstUnequalPhysicalEnergy.lean 1 declarations
FirstUnequalRetainedEnergy.lean 1 declarations
FirstWholeCanonicalTail.lean 1 declarations
FirstWholeCubePriority.lean 2 declarations
FirstWholeMarkedColumns.lean 3 declarations
FirstWholeTail.lean 1 declarations
FirstZeroSource.lean 2 declarations
FixedSquare.lean 1 declarations
FreshWindows.lean 4 declarations
FullProfile.lean 7 declarations
GeneratorTransport.lean 6 declarations
GlobalCanonicalEnergy.lean 2 declarations
GlobalParentEnergy.lean 2 declarations
GlobalParentSource.lean 7 declarations
GlobalPrincipalMass.lean 8 declarations
GlobalPrincipalMassCount.lean 2 declarations
GlobalPrincipalMassPrefactor.lean 4 declarations
GlobalPrincipalMassSource.lean 2 declarations
GlobalPrincipalMassWeighted.lean 4 declarations
GlobalPriorityAggregate.lean 2 declarations
GlobalPriorityBranches.lean 2 declarations
GlobalPriorityEnergy.lean 1 declarations
GlobalPriorityFilteredAggregate.lean 1 declarations
GlobalPriorityFilteredAggregateUniform.lean 1 declarations
GlobalPriorityFilteredEnergy.lean 1 declarations
GlobalPriorityFilteredEnergyUniform.lean 1 declarations
GlobalPriorityFilteredRays.lean 1 declarations
GlobalPriorityFilteredRaysUniform.lean 1 declarations
GlobalPriorityFilteredStep.lean 1 declarations
GlobalPriorityFilteredStepUniform.lean 1 declarations
GlobalPriorityFixedChildStep.lean 1 declarations
GlobalPriorityFixedChildStepUniform.lean 1 declarations
GlobalPriorityFullAggregate.lean 3 declarations
GlobalPriorityFullBranches.lean 1 declarations
GlobalPriorityMass.lean 1 declarations
GlobalPriorityPhysical.lean 1 declarations
GlobalPriorityRays.lean 1 declarations
GlobalPrioritySource.lean 6 declarations
GlobalPriorityTail.lean 1 declarations
GlobalPriorityTailAggregate.lean 1 declarations
GlobalPriorityTailCollapse.lean 2 declarations
GlobalPriorityTailMass.lean 1 declarations
GlobalPriorityTailPhysical.lean 1 declarations
GlobalPriorityZero.lean 2 declarations
GlobalPriorityZeroPhysical.lean 1 declarations
GlobalRetainedGates.lean 5 declarations
GlobalRetainedGatesBudget.lean 2 declarations
GlobalRetainedGatesCaps.lean 3 declarations
GlobalRetainedGatesChildren.lean 3 declarations
GlobalRetainedGatesGeometry.lean 6 declarations
GlobalRetainedGatesRadius.lean 6 declarations
GlobalRetainedGatesRank.lean 1 declarations
Grid.lean 7 declarations
Hybrid.lean 26 declarations
HybridBound.lean 3 declarations
HybridReduction.lean 5 declarations
IdealMasks.lean 12 declarations
InitializationEnergy.lean 13 declarations
LocalReflection.lean 8 declarations
MarkBounds.lean 3 declarations
MarkedFourier.lean 5 declarations
MarkedPhase.lean 6 declarations
MarkedReflection.lean 6 declarations
MarkedStratum.lean 7 declarations
MarkedTails.lean 4 declarations
MarkedTwists.lean 3 declarations
Marks.lean 10 declarations
MaskedGrid.lean 4 declarations
MixedRow.lean 6 declarations
OriginalBlock.lean 1 declarations
OriginalCellPriority.lean 4 declarations
OriginalZeroPhysical.lean 1 declarations
Overlap.lean 8 declarations
PhysicalBlockBudget.lean 3 declarations
PhysicalExponents.lean 11 declarations
Poisson.lean 9 declarations
PoissonTails.lean 3 declarations
PrincipalChild.lean 6 declarations
PrincipalSelectorMass.lean 2 declarations
PriorityCellBudget.lean 1 declarations
PriorityCellEnergy.lean 1 declarations
PriorityCellEnergyWindowOrder.lean 1 declarations
PriorityCellEnergyWindowOrderUniform.lean 1 declarations
PriorityMovingRadius.lean 1 declarations
PriorityMovingRadiusWindowOrder.lean 1 declarations
PriorityMovingRadiusWindowOrderUniform.lean 1 declarations
PriorityProfile.lean 7 declarations
PriorityRetainedBound.lean 1 declarations
PriorityRetainedMovingRadius.lean 1 declarations
PriorityRetainedMovingRadiusWindowOrder.lean 1 declarations
PriorityRetainedMovingRadiusWindowOrderUniform.lean 1 declarations
PrioritySourceBudget.lean 3 declarations
PrioritySourceEnergy.lean 1 declarations
ProfileIntegral.lean 4 declarations
Quadratic.lean 7 declarations
Quotients.lean 9 declarations
Reconstruction.lean 4 declarations
RecursionParameters.lean 5 declarations
ReflectedDual.lean 3 declarations
ReopenedBinEnergy.lean 1 declarations
ReopenedBins.lean 6 declarations
ReopenedBlocks.lean 2 declarations
ReopenedCommonMeasure.lean 1 declarations
ReopenedIdentification.lean 2 declarations
ReopenedIntegralEnergy.lean 2 declarations
ReopenedMarks.lean 4 declarations
ReopenedOriginalRow.lean 3 declarations
ReopenedPhysicalEnergy.lean 2 declarations
ReopenedPhysicalSplit.lean 4 declarations
ReopenedPriority.lean 2 declarations
ReopenedSeparation.lean 2 declarations
ReopenedSource.lean 4 declarations
ReopenedZeroEnergy.lean 1 declarations
RootWindows.lean 6 declarations
SecondActualMass.lean 3 declarations
SecondAdmissible.lean 6 declarations
SecondAllIntegral.lean 1 declarations
SecondAllModes.lean 3 declarations
SecondAssignedSource.lean 12 declarations
SecondAssignedSum.lean 9 declarations
SecondBalancedPhysical.lean 1 declarations
SecondBalancedSource.lean 3 declarations
SecondBlockEnergy.lean 1 declarations
SecondBlockEnergyWindowOrder.lean 1 declarations
SecondBlockEnergyWindowOrderUniform.lean 1 declarations
SecondCanonicalChild.lean 7 declarations
SecondCanonicalSplit.lean 3 declarations
SecondCanonicalTail.lean 1 declarations
SecondCauchy.lean 6 declarations
SecondCellParameters.lean 8 declarations
SecondCellPhysical.lean 7 declarations
SecondCenterSector.lean 4 declarations
SecondCorrelatedCutoff.lean 3 declarations
SecondCutoffScale.lean 2 declarations
SecondDeletedAllIntegral.lean 1 declarations
SecondDeletedAllModes.lean 3 declarations
SecondDeletedModeEnergy.lean 1 declarations
SecondDeletedMovingEnergy.lean 1 declarations
SecondDeletedMovingEnergyUniform.lean 1 declarations
SecondDeletedMovingMass.lean 1 declarations
SecondDeletedMovingMassUniform.lean 1 declarations
SecondDeletedOriginalBound.lean 1 declarations
SecondDeletedPhysicalEnergy.lean 1 declarations
SecondDeletedPhysicalRecursive.lean 1 declarations
SecondDensityAssembly.lean 2 declarations
SecondEnergy.lean 6 declarations
SecondFiniteMeasure.lean 1 declarations
SecondFixedFamily.lean 6 declarations
SecondFreshAssembly.lean 3 declarations
SecondFreshMeasure.lean 1 declarations
SecondFreshTruncation.lean 1 declarations
SecondFullSource.lean 1 declarations
SecondGenerator.lean 7 declarations
SecondInheritedEnergy.lean 1 declarations
SecondKernelMeasure.lean 5 declarations
SecondMarkedEnergy.lean 3 declarations
SecondMarkedTail.lean 2 declarations
SecondModeCanonical.lean 7 declarations
SecondModeEnergy.lean 1 declarations
SecondModeIntegral.lean 2 declarations
SecondModeParentLists.lean 3 declarations
SecondNormalizedEnergy.lean 6 declarations
SecondOriginalBound.lean 1 declarations
SecondOriginalMass.lean 1 declarations
SecondParentAssembly.lean 6 declarations
SecondParentInput.lean 5 declarations
SecondParentLists.lean 4 declarations
SecondParentRadial.lean 1 declarations
SecondPass.lean 3 declarations
SecondPhysicalEnergy.lean 1 declarations
SecondPhysicalRecursive.lean 1 declarations
SecondPhysicalRows.lean 5 declarations
SecondProfileIdentity.lean 4 declarations
SecondPuncture.lean 12 declarations
SecondPunctureBudget.lean 3 declarations
SecondRapidTail.lean 1 declarations
SecondSectorAssembly.lean 5 declarations
SecondSeparatedColumns.lean 6 declarations
SecondSharpPuncture.lean 6 declarations
SecondSourceAttachment.lean 13 declarations
SecondSourceEncoding.lean 6 declarations
SecondSourceProfile.lean 3 declarations
SecondSourceSize.lean 2 declarations
SecondSourceTuples.lean 7 declarations
SecondSquarefree.lean 11 declarations
SecondSupportedEnergy.lean 5 declarations
SecondTailAbsorption.lean 2 declarations
SecondTailCost.lean 3 declarations
SecondTripleBounds.lean 3 declarations
SecondVariableCutoff.lean 4 declarations
SecondVariablePrincipal.lean 2 declarations
SecondVaryingBalanced.lean 1 declarations
SecondVaryingDensity.lean 2 declarations
SecondVaryingLists.lean 7 declarations
SecondVaryingPhysical.lean 2 declarations
SecondVaryingSupported.lean 1 declarations
SecondWeights.lean 4 declarations
SecondWholeCutoff.lean 3 declarations
SecondWholeKernel.lean 2 declarations
SecondWholeMass.lean 5 declarations
SecondWholeTail.lean 4 declarations
Sharp.lean 3 declarations
ShortCompletionEnergy.lean 2 declarations
ShortReflectedEnergy.lean 4 declarations
ShortReflectedPower.lean 2 declarations
SieveComposition.lean 5 declarations
SlotAssignments.lean 7 declarations
SlotProducts.lean 7 declarations
SourceDepth.lean 3 declarations
SourceHybrid.lean 5 declarations
TripleMass.lean 6 declarations
TwoPassScalar.lean 1 declarations
WholePriorityBranches.lean 4 declarations
WholePriorityCollapse.lean 2 declarations
WholePriorityEnergy.lean 1 declarations
WholePriorityMass.lean 1 declarations
WholePriorityParentBounds.lean 4 declarations
WholePriorityParents.lean 12 declarations
WholePriorityPhysical.lean 4 declarations
WholePriorityPrincipal.lean 2 declarations
WholePriorityRays.lean 1 declarations
WholeRetainedSource.lean 4 declarations
Widths.lean 4 declarations
WindowFourier.lean 17 declarations