OAI/Combinatorics/Progressions/Fourier/
1818 declarations, 0 contain sorry, 0 declared as axioms; 180 files
Files
- AffineFrequencyLift.lean 4 declarations
- AffineShortCoefficientMajorArc.lean 3 declarations
- AffineTorusDensityIncrement.lean 5 declarations
- AffineTorusGeometry.lean 8 declarations
- AffineUniformSpectrum.lean 2 declarations
- AllocatedCorrelatedModerateSpectrum.lean 4 declarations
- AllocatedCutoffFourierBudget.lean 1 declarations
- AllocatedErrorFourierBudget.lean 5 declarations
- AllocatedErrorStandardFourier.lean 3 declarations
- AllocatedExternalCandidateSpatialNativeFrequencyTransport.lean 17 declarations
- AllocatedFixedProjectedFourier.lean 1 declarations
- AllocatedGridFourierApproximation.lean 1 declarations
- AllocatedGridSpectrumSize.lean 1 declarations
- AllocatedIdealCoefficientFourier.lean 1 declarations
- AllocatedInactiveGridSpectrum.lean 1 declarations
- AllocatedJetFourierData.lean 10 declarations
- AllocatedMaskedCoefficientFourier.lean 35 declarations
- AllocatedNormalizedTorusCutoff.lean 15 declarations
- AllocatedPointSpectrumCap.lean 3 declarations
- AllocatedPositiveFourierData.lean 1 declarations
- AllocatedProbabilityFourier.lean 2 declarations
- AllocatedProfileErrorStandardFourier.lean 2 declarations
- AllocatedProjectedFourierData.lean 1 declarations
- AllocatedRecoveredTagTorusVariation.lean 5 declarations
- AllocatedResidueSpectrum.lean 4 declarations
- AllocatedSiteBufferFourier.lean 3 declarations
- AllocatedSiteErrorFourierBudget.lean 5 declarations
- AllocatedSiteSpectrumBudget.lean 33 declarations
- AllocatedSupportedResidueSpectrum.lean 7 declarations
- AllocatedSupportedSlicedInactiveSpectrum.lean 1 declarations
- AnchoredCoefficientFourierNormalization.lean 10 declarations
- BohrLocalMomentAlternatives.lean 1 declarations
- BohrLocalizedAverage.lean 2 declarations
- BohrMatchedContraction.lean 1 declarations
- BohrMatchingScales.lean 4 declarations
- BohrNiltestBudget.lean 76 declarations
- BohrTorusApproximation.lean 58 declarations
- BooleanBlockMajorArc.lean 2 declarations
- BooleanCharacterReferenceError.lean 3 declarations
- BoundedFrequencyKernel.lean 5 declarations
- BoxDifferenceCharacter.lean 2 declarations
- CRTConfigurationTorus.lean 4 declarations
- CanonicalDensityFourier.lean 19 declarations
- CharacterCenteredCounting.lean 2 declarations
- CharacterCoordinateScale.lean 15 declarations
- CircleActionFourierMetric.lean 6 declarations
- ClearedSectionFrequency.lean 4 declarations
- CoefficientAmbientFourier.lean 1 declarations
- CoefficientEvaluationTorus.lean 8 declarations
- CoefficientFourierTranslation.lean 5 declarations
- CoefficientResidualCharacter.lean 3 declarations
- CokernelCharacterWitness.lean 4 declarations
- CommonCoveredSiteCharacter.lean 35 declarations
- CommonDependentWordFrequency.lean 3 declarations
- CommonMarkedFrequencyModel.lean 15 declarations
- CommonShiftQuotientFrequency.lean 2 declarations
- ConfigurationCharacters.lean 6 declarations
- ControlledFrequencyExternalTransfer.lean 5 declarations
- ControlledReplicatedFrequency.lean 30 declarations
- ControlledTorusDecomposition.lean 1 declarations
- CoordinatedBohrMatching.lean 3 declarations
- CorrelatedModerateFourierShift.lean 5 declarations
- CrossRowCharacterDifference.lean 4 declarations
- CubicPrimitiveFourierRows.lean 1 declarations
- CyclicAffineCharacterPhase.lean 7 declarations
- CyclicTorusCoordinates.lean 8 declarations
- DilationFrequencyPhase.lean 2 declarations
- DivisibleCharacterExtension.lean 4 declarations
- ElementaryCharacterTail.lean 4 declarations
- EuclideanCoefficientTorus.lean 8 declarations
- EuclideanJetTorus.lean 54 declarations
- ExpandingGramSpectrum.lean 4 declarations
- ExponentialBohrVolume.lean 78 declarations
- FactoredPolynomialCharacter.lean 2 declarations
- FiniteCharacterOrderTail.lean 7 declarations
- FiniteFourierSmoothing.lean 43 declarations
- FiniteSpectrumCutoff.lean 9 declarations
- FixedPrincipalCoefficientSpectrum.lean 34 declarations
- ForecastInactiveCharacterSite.lean 10 declarations
- ForecastInactiveFixedSpectrum.lean 2 declarations
- ForecastInactiveSpectrum.lean 2 declarations
- ForecastSpatialCharacterSplit.lean 6 declarations
- FourierLawTransport.lean 18 declarations
- FourierWeightedCounting.lean 2 declarations
- FrequencyGridIntervals.lean 4 declarations
- FrequencyProjectionBudget.lean 3 declarations
- GowersFourierMultiplier.lean 3 declarations
- HomogeneousGradedProjectionFrequency.lean 12 declarations
- IndependentCharacterEvents.lean 2 declarations
- IntegerBoxCharacterBound.lean 3 declarations
- IntegerPeriodicTorusLift.lean 3 declarations
- IntegerPolynomialTorusPeriod.lean 5 declarations
- IntegerSupportTorus.lean 7 declarations
- JoinedFrequencyQuotientInjectivity.lean 48 declarations
- JoinedFrequencyRefilteredTop.lean 2 declarations
- LatticeCoordinateResidueFourier.lean 15 declarations
- LatticeGaussianMeanFourier.lean 6 declarations
- LatticeTorusFourierCoefficient.lean 5 declarations
- LayeredFourierCharacter.lean 5 declarations
- LocalBohrAlmostPeriodsRelative.lean 26 declarations
- LocalSpectrumBudget.lean 3 declarations
- LogCharacterBudget.lean 10 declarations
- MajorPhaseLowFourierExtraction.lean 10 declarations
- MarkedQuotientFrequencyBounds.lean 2 declarations
- MarkedRealFrequencyCompatibility.lean 2 declarations
- MixedDiscreteFourier.lean 2 declarations
- MixedOriginalPairFrequency.lean 4 declarations
- MonomialCharacterMean.lean 15 declarations
- NativeCharacterCrossFamily.lean 1 declarations
- NativeMixedFourierProfiles.lean 10 declarations
- NativeRoundedBohrModel.lean 1 declarations
- NaturalFrequencyMultiples.lean 2 declarations
- NiltestConjugateFrequency.lean 2 declarations
- NormalizedTwistHighFrequencyRemoval.lean 1 declarations
- NormalizedTwistLocalizedFourierSelection.lean 29 declarations
- NormalizedTwistSingleSiteFourierHaar.lean 27 declarations
- OneSiteFourierAverage.lean 3 declarations
- ParametricQuarterTorusExtension.lean 1 declarations
- PivotAnnihilatorFrequencyCode.lean 16 declarations
- PlateauFourierMode.lean 10 declarations
- PolynomialCharacterRowPhase.lean 8 declarations
- PolynomialSpectrumAccuracy.lean 12 declarations
- PolynomialTorusDensityIncrement.lean 2 declarations
- PolynomialWeightedCubeMajorArc.lean 14 declarations
- PositiveTorusMasks.lean 1 declarations
- PreparedCoefficientTorusCompact.lean 1 declarations
- PrimePowerCharacterDepth.lean 1 declarations
- PrimePowerCharacterScaling.lean 17 declarations
- PrimePowerTaggedCharacterRows.lean 8 declarations
- PrincipalCoefficientResidueSpectrum.lean 13 declarations
- ProductFrequencyKernel.lean 8 declarations
- QuadraticFrequencyCoordinates.lean 17 declarations
- QuadraticLocalFrequency.lean 9 declarations
- QuantitativeBohrBound.lean 4 declarations
- QuarticBohrProgression.lean 57 declarations
- QuarticExchangedFourier.lean 2 declarations
- QuarticOriginalPairFrequency.lean 4 declarations
- RationalBohrWidth.lean 5 declarations
- RationalCharacterIndividualModulus.lean 18 declarations
- RationalFrequencyHeight.lean 1 declarations
- RationalLiftCharacterTwist.lean 8 declarations
- RawCubeFourierBudget.lean 1 declarations
- RawModerateFourierBudget.lean 1 declarations
- RealLayerHorizontalFrequency.lean 6 declarations
- RealQuarterTorusExtension.lean 29 declarations
- RectangularGridCharacter.lean 65 declarations
- RelativeModerateFourierAxis.lean 7 declarations
- RelativeSpectrumDimension.lean 6 declarations
- ResidueFourierProjection.lean 7 declarations
- RetainedCharacterGridSum.lean 5 declarations
- SectionPolynomialCharacter.lean 3 declarations
- SectionRetainedFourier.lean 11 declarations
- SelectedDensityAmbientProductFourier.lean 9 declarations
- SharedFreeFactorizationFrequency.lean 6 declarations
- SiteFourierHaarMean.lean 32 declarations
- SiteFourierPullbackBound.lean 2 declarations
- SiteFourierRegularity.lean 3 declarations
- SmoothModerateFourierAxis.lean 4 declarations
- SquareModeGradedFrequency.lean 3 declarations
- StandardJetFourier.lean 20 declarations
- StepOneFamilyFourier.lean 1 declarations
- TaggedMajorFourierNiltest.lean 1 declarations
- TorusCellBudget.lean 41 declarations
- TorusCircleActions.lean 8 declarations
- TranslatedBohrDifference.lean 26 declarations
- TranslationPhaseCharacterBounds.lean 3 declarations
- UnbalancedBohrShape.lean 17 declarations
- UniformEmbeddedFourier.lean 9 declarations
- UniformScaledRetainedCharacters.lean 58 declarations
- UniformSpectrumAbsoluteCap.lean 24 declarations
- UniformSpectrumLogBounds.lean 17 declarations
- UniformSpectrumSize.lean 8 declarations
- UniformWeightTorusModel.lean 1 declarations
- VerticalFrequencyIdentification.lean 10 declarations
- WeightedBlockTorus.lean 7 declarations
- WeightedFourierExtraction.lean 2 declarations
- WeightedModerateProductFourierTail.lean 1 declarations
- WeightedTranslationBufferedCentralFrequency.lean 7 declarations
- WeightedTranslationTwistedCentralFrequency.lean 8 declarations
- WeightedUniformSpectrumTail.lean 6 declarations