OAI/NumberTheory/DirichletL/PrimeRows/
753 declarations, 0 contain sorry, 0 declared as axioms; 182 files
Files
- ActiveGaussFactorization.lean 50 declarations
- Agreement.lean 7 declarations
- BufferedBin.lean 5 declarations
- BufferedContour.lean 5 declarations
- BufferedGrowth.lean 1 declarations
- BufferedHeightGrowth.lean 1 declarations
- BufferedIntegral.lean 2 declarations
- BufferedJoinDecay.lean 2 declarations
- BufferedJoins.lean 1 declarations
- BufferedSlices.lean 2 declarations
- BufferedTransport.lean 2 declarations
- CanonicalCubeBins.lean 3 declarations
- CanonicalCubeChoice.lean 1 declarations
- CanonicalCubeReduction.lean 1 declarations
- CanonicalRayCube.lean 2 declarations
- CanonicalReduction.lean 2 declarations
- CanonicalTails.lean 2 declarations
- CentralCosts.lean 3 declarations
- CentralCube.lean 3 declarations
- CentralError.lean 3 declarations
- CentralErrorSaving.lean 4 declarations
- CentralExpansion.lean 4 declarations
- CentralFiniteError.lean 3 declarations
- CentralHeightCost.lean 2 declarations
- CentralIntegral.lean 3 declarations
- CentralNormalized.lean 1 declarations
- CentralProduct.lean 3 declarations
- CentralRamified.lean 1 declarations
- CentralRectangle.lean 3 declarations
- CentralRowCost.lean 2 declarations
- CentralSlotSum.lean 1 declarations
- CentralSlots.lean 2 declarations
- CentralSplit.lean 6 declarations
- CentralSupportedSplit.lean 7 declarations
- CentralTargetCost.lean 5 declarations
- CentralWTail.lean 1 declarations
- CentralZTail.lean 1 declarations
- Character.lean 11 declarations
- CoarseAmplitude.lean 6 declarations
- CoarsePhysical.lean 5 declarations
- CoarseUniform.lean 3 declarations
- Conductor.lean 5 declarations
- Continuation.lean 10 declarations
- CubeBinPartition.lean 4 declarations
- CubeCalibration.lean 3 declarations
- CubeCommonProfile.lean 3 declarations
- CubeErrorSaving.lean 1 declarations
- CubeFiniteError.lean 2 declarations
- CubeFiniteIntegral.lean 5 declarations
- CubeFixedPrimes.lean 2 declarations
- CubeFloorArithmetic.lean 2 declarations
- CubeFloorCollected.lean 2 declarations
- CubeFloorDyadic.lean 4 declarations
- CubeFloorGlobal.lean 2 declarations
- CubeFloorGlobalIntegral.lean 2 declarations
- CubeFloorNormalized.lean 2 declarations
- CubeFloorSaving.lean 2 declarations
- CubeNormalizer.lean 1 declarations
- CubePhaseBins.lean 1 declarations
- CubePrimeBound.lean 2 declarations
- CubePrimeThresholds.lean 1 declarations
- CubeScale.lean 2 declarations
- CubeSlotExponent.lean 4 declarations
- CubeSupportedWitness.lean 1 declarations
- DetectorBins.lean 4 declarations
- DetectorReady.lean 5 declarations
- DetectorZeros.lean 21 declarations
- DiskControl.lean 8 declarations
- DyadBound.lean 1 declarations
- DyadIntegral.lean 4 declarations
- Euler.lean 8 declarations
- ExhaustivePartition.lean 1 declarations
- FiniteNormalization.lean 3 declarations
- FirstAnalytic.lean 3 declarations
- FirstBoundary.lean 4 declarations
- FirstContinuation.lean 9 declarations
- FirstIntegral.lean 5 declarations
- FirstJoint.lean 1 declarations
- FirstNeighborhood.lean 4 declarations
- FirstProduct.lean 3 declarations
- FirstTail.lean 8 declarations
- FirstTransport.lean 4 declarations
- FirstWGrowth.lean 3 declarations
- FirstWShift.lean 4 declarations
- FixedIntegral.lean 2 declarations
- GeometricTail.lean 4 declarations
- HighFromMoments.lean 1 declarations
- HorizontalIntegral.lean 2 declarations
- Ideal.lean 4 declarations
- IdealGenerators.lean 27 declarations
- IteratedShift.lean 2 declarations
- LargeDyad.lean 1 declarations
- LargeSaving.lean 1 declarations
- LargeTail.lean 2 declarations
- MarkedCompensation.lean 4 declarations
- MarkedContinuation.lean 3 declarations
- MarkedCoordinates.lean 3 declarations
- MarkedEuler.lean 7 declarations
- MarkedExclusions.lean 4 declarations
- MarkedHolomorphic.lean 6 declarations
- MarkedLocal.lean 4 declarations
- MarkedNormalization.lean 7 declarations
- MarkedProduct.lean 5 declarations
- MarkedSubset.lean 4 declarations
- Measurable.lean 14 declarations
- Moments.lean 8 declarations
- NonfloorArithmetic.lean 1 declarations
- NonfloorBudget.lean 5 declarations
- NonfloorClass.lean 2 declarations
- NonfloorCollected.lean 1 declarations
- NonfloorCount.lean 2 declarations
- NonfloorDictionary.lean 3 declarations
- NonfloorDyadic.lean 5 declarations
- NonfloorExponent.lean 2 declarations
- NonfloorIntegral.lean 1 declarations
- NonfloorMoments.lean 1 declarations
- NonfloorNormalized.lean 1 declarations
- NonfloorSourceCount.lean 4 declarations
- NonfloorTransport.lean 2 declarations
- NonprincipalBoundary.lean 4 declarations
- NonprincipalContour.lean 7 declarations
- NonprincipalShift.lean 2 declarations
- NormFiberExtraction.lean 49 declarations
- NormalizedTransport.lean 3 declarations
- NormalizedTransportSaving.lean 2 declarations
- Origin.lean 5 declarations
- OriginalHeightTail.lean 2 declarations
- PhysicalBound.lean 1 declarations
- PhysicalDyad.lean 5 declarations
- PhysicalLargeTail.lean 1 declarations
- PhysicalPartition.lean 3 declarations
- PhysicalSmallTail.lean 1 declarations
- Principal.lean 7 declarations
- PrincipalMask.lean 5 declarations
- Product.lean 8 declarations
- ProfileIntegral.lean 2 declarations
- Ramified.lean 5 declarations
- RationalApproximation.lean 22 declarations
- ReciprocalGrowth.lean 1 declarations
- RestoreCorrection.lean 5 declarations
- RowCount.lean 3 declarations
- RowPartition.lean 13 declarations
- ScalarGrowth.lean 1 declarations
- Selected.lean 4 declarations
- SelectedAgreement.lean 8 declarations
- SelectedAnalytic.lean 5 declarations
- SelectedBounds.lean 3 declarations
- SelectedFirst.lean 6 declarations
- SelectedFirstBounds.lean 4 declarations
- SelectedHolomorphic.lean 3 declarations
- SelectedUnramified.lean 2 declarations
- Series.lean 5 declarations
- SliceIntegral.lean 1 declarations
- SlotSums.lean 1 declarations
- SmallDyad.lean 2 declarations
- SmallPartition.lean 8 declarations
- SmallSum.lean 1 declarations
- SmallTail.lean 1 declarations
- SourceTransport.lean 3 declarations
- TailIntegral.lean 1 declarations
- TailScales.lean 5 declarations
- TargetPrincipal.lean 5 declarations
- TupleBound.lean 1 declarations
- TupleFactor.lean 1 declarations
- TupleGrowth.lean 2 declarations
- TupleSums.lean 1 declarations
- UniformError.lean 1 declarations
- UniformJoins.lean 1 declarations
- UniformSlices.lean 1 declarations
- UniformTail.lean 1 declarations
- Unramified.lean 2 declarations
- Valuation.lean 7 declarations
- WGrowth.lean 1 declarations
- WZTransport.lean 5 declarations
- WeightedTuple.lean 3 declarations
- XBoundary.lean 4 declarations
- XGrowth.lean 1 declarations
- XShift.lean 1 declarations
- ZBoundary.lean 5 declarations
- ZContour.lean 3 declarations
- ZGrowth.lean 1 declarations
- ZShift.lean 3 declarations