OAI/Computability/FourierTransform/
1940 declarations, 0 contain sorry, 0 declared as axioms; 88 files
Files
- AddressTables.lean 7 declarations
- ArbitraryLength.lean 26 declarations
- Asymptotics.lean 18 declarations
- BinaryBasis.lean 39 declarations
- BinaryFFT.lean 24 declarations
- BinaryFrames.lean 55 declarations
- BitLayout.lean 30 declarations
- ChineseRemainder.lean 19 declarations
- ChirpConvolution.lean 22 declarations
- ChunkCompiler.lean 31 declarations
- ChunkPrograms.lean 5 declarations
- CirculantUpdates.lean 10 declarations
- ColumnAddresses.lean 16 declarations
- CompilerEnvironment.lean 50 declarations
- ConvolutionProgram.lean 7 declarations
- Cost.lean 20 declarations
- DirectionalWords.lean 29 declarations
- DisjointIntervals.lean 36 declarations
- FourierCompilation.lean 7 declarations
- FourierIdentities.lean 30 declarations
- FourierWords.lean 25 declarations
- FrameLifting.lean 16 declarations
- Goal.lean 23 declarations
- IntegerPrograms.lean 19 declarations
- IntervalEffects.lean 28 declarations
- IntervalPrograms.lean 14 declarations
- LayerCompilation.lean 15 declarations
- LayerPrograms.lean 16 declarations
- LayerWords.lean 49 declarations
- Layout.lean 34 declarations
- LayoutPrograms.lean 10 declarations
- LengthSelection.lean 38 declarations
- LocalCompiler.lean 11 declarations
- LocalPreparation.lean 35 declarations
- LoopBounds.lean 6 declarations
- Main.lean 15 declarations
- MeasuredFit.lean 28 declarations
- MeasuredPrograms.lean 6 declarations
- NetworkInvocation.lean 16 declarations
- NetworkLabels.lean 39 declarations
- NetworkRoles.lean 56 declarations
- NetworkStages.lean 57 declarations
- NewtonFactorization.lean 28 declarations
- PackingPrograms.lean 24 declarations
- ParameterPrograms.lean 8 declarations
- PolynomialBounds.lean 17 declarations
- PolynomialPrograms.lean 33 declarations
- PowerTables.lean 9 declarations
- PrefixTraversal.lean 5 declarations
- PrimeSelection.lean 15 declarations
- ProductMatrix.lean 6 declarations
- ProgramBounds.lean 28 declarations
- ProgramConstruction.lean 38 declarations
- RAM.lean 33 declarations
- RecursionBounds.lean 10 declarations
- RecursiveBatches.lean 20 declarations
- RecursiveContract.lean 4 declarations
- RegisterBounds.lean 13 declarations
- RoleArrays.lean 20 declarations
- RootPreparation.lean 29 declarations
- ScalarNetwork.lean 37 declarations
- ScalarPreparation.lean 15 declarations
- SectorAlgorithm.lean 17 declarations
- SectorIdentities.lean 19 declarations
- SectorPacking.lean 64 declarations
- SectorPrograms.lean 10 declarations
- SynchronizedAlgorithm.lean 8 declarations
- TensorAlgorithm.lean 5 declarations
- TensorCertificate.lean 26 declarations
- TensorFibers.lean 13 declarations
- TensorIndexing.lean 39 declarations
- TensorProgram.lean 4 declarations
- TensorRecursion.lean 4 declarations
- TensorSaving.lean 11 declarations
- ToeplitzCompiler.lean 14 declarations
- ToeplitzIdentities.lean 15 declarations
- ToeplitzLayers.lean 20 declarations
- ToeplitzPreparation.lean 10 declarations
- ToeplitzUpdates.lean 36 declarations
- TransformProgram.lean 16 declarations
- TraversalPrograms.lean 15 declarations
- UniformBounds.lean 18 declarations
- WordCompilation.lean 17 declarations
- WordPrograms.lean 39 declarations
- WorkBounds.lean 49 declarations
- WorkingCompiler.lean 17 declarations
- WorkingPreparation.lean 20 declarations
- WorkingTransform.lean 5 declarations