OAI/MeasureTheory/Falconer/Fourier/
986 declarations, 0 contain sorry, 0 declared as axioms; 184 files
Files
- ActualDistanceLowBand.lean 2 declarations
- ActualSymbolEstimates.lean 3 declarations
- AllDimensionalSpatialFourierIntegration.lean 6 declarations
- AllDimensionalSpatialFourierSeparation.lean 11 declarations
- AmbientSymbols.lean 3 declarations
- AnchorSymbolDropping.lean 5 declarations
- AssemblyCutoff.lean 1 declarations
- BaseJetAmplitude.lean 4 declarations
- BinKernel.lean 7 declarations
- BorelSymbols.lean 4 declarations
- BumpDerivatives.lean 6 declarations
- CellSymbols.lean 9 declarations
- ChartBumps.lean 5 declarations
- ChartDerivatives.lean 15 declarations
- ChartJetOperators.lean 7 declarations
- ChartSymbolControl.lean 4 declarations
- CompactFourierBound.lean 5 declarations
- ComplexMaskJets.lean 12 declarations
- ConeIntegration.lean 4 declarations
- CoordinateIntegral.lean 6 declarations
- DescriptorDerivativeScale.lean 5 declarations
- DescriptorInverseJets.lean 10 declarations
- DescriptorJetMeasurable.lean 3 declarations
- DescriptorJetProduct.lean 5 declarations
- DescriptorJetRemoval.lean 7 declarations
- DescriptorPairDerivativeScale.lean 1 declarations
- DistanceBandKernelBound.lean 3 declarations
- DistanceFourierDifference.lean 5 declarations
- DistanceFrequencyBox.lean 8 declarations
- DistanceFrequencyMajorant.lean 3 declarations
- DistanceKernelSplitting.lean 4 declarations
- DistanceSincCollision.lean 4 declarations
- DistanceSincKernel.lean 7 declarations
- DistanceSincSpectralIdentity.lean 4 declarations
- DyadicTransforms.lean 1 declarations
- EndpointTransform.lean 6 declarations
- EuclideanPolar.lean 2 declarations
- EuclideanSmoothConvolution.lean 6 declarations
- FarCollisionIntegral.lean 2 declarations
- FarIntegralAssembly.lean 1 declarations
- FarTestedIntegral.lean 2 declarations
- FiberSchwartz.lean 11 declarations
- FourStationaryPhases.lean 5 declarations
- FourierBandBound.lean 1 declarations
- FourierBandDecomposition.lean 4 declarations
- FourierConvolution.lean 4 declarations
- FourierEnergy.lean 10 declarations
- FourierLebesgue.lean 9 declarations
- FourierPairing.lean 6 declarations
- FourierSlice.lean 3 declarations
- GaussianRepresentation.lean 8 declarations
- GoodSupportedKernelMajorant.lean 6 declarations
- GraphActualFrequencySupport.lean 2 declarations
- GraphFourPointKernel.lean 7 declarations
- GraphFourSymbolDerivatives.lean 5 declarations
- GraphKernelBounds.lean 6 declarations
- HalfDimensionalFourier.lean 3 declarations
- InheritedSymbolMeasurability.lean 3 declarations
- InheritedSymbolSupport.lean 2 declarations
- IntegratedSmoothing.lean 2 declarations
- InverseClassIntegration.lean 4 declarations
- InverseJetCoefficient.lean 1 declarations
- InverseJetIntegration.lean 4 declarations
- InverseJetShell.lean 5 declarations
- InverseJetState.lean 6 declarations
- InverseJetSupport.lean 9 declarations
- InverseJetSymbols.lean 5 declarations
- InverseJetValues.lean 11 declarations
- InverseMaskJets.lean 42 declarations
- JetAdmissible.lean 3 declarations
- JetChartControl.lean 1 declarations
- JetDerivativeBounds.lean 5 declarations
- JetNormalization.lean 2 declarations
- JetStateAmbient.lean 5 declarations
- JetStateAntipodal.lean 6 declarations
- JetStateBudget.lean 1 declarations
- JetStateBudgetOrder.lean 4 declarations
- JetStateChildren.lean 4 declarations
- JetStateCrossKernel.lean 2 declarations
- JetStateEnvelope.lean 9 declarations
- JetStateFarBand.lean 1 declarations
- JetStateFarExpansion.lean 2 declarations
- JetStateFarKernel.lean 2 declarations
- JetStateFarOriginal.lean 1 declarations
- JetStateFarRemainder.lean 2 declarations
- JetStateFarSupport.lean 3 declarations
- JetStateNear.lean 2 declarations
- JetStateNearFar.lean 1 declarations
- JetStateNoncomparable.lean 2 declarations
- JetStateNoncomparableFull.lean 1 declarations
- JetStateOperations.lean 6 declarations
- JetStateOriginalEnergy.lean 2 declarations
- JetStateSpatialShell.lean 4 declarations
- JetStateStationary.lean 5 declarations
- JointStationaryGeometry.lean 13 declarations
- KernelFourierIdentity.lean 2 declarations
- LaplacianFourier.lean 6 declarations
- LocalStationaryJets.lean 9 declarations
- LowFrequencyKernel.lean 9 declarations
- MaskJetAlgebra.lean 22 declarations
- MaskJetCount.lean 10 declarations
- MaskJetGeometry.lean 13 declarations
- MaskJetIsometry.lean 4 declarations
- MaskJetSeed.lean 19 declarations
- MaskJetSeparation.lean 14 declarations
- MaskedFourier.lean 3 declarations
- MaskedJetBudget.lean 4 declarations
- MaskedStationaryJets.lean 10 declarations
- MatrixCofactorBound.lean 3 declarations
- MeasureKernelConvolution.lean 5 declarations
- MellinGaussian.lean 7 declarations
- MinimalPairSymbol.lean 4 declarations
- NoncomparableOriginalIntegral.lean 3 declarations
- NonstationaryPhase.lean 1 declarations
- NormalizedInverseIntegration.lean 2 declarations
- NormalizedJetDerivatives.lean 4 declarations
- NormalizedSymbolFactors.lean 9 declarations
- OriginalStationaryPower.lean 1 declarations
- OriginalStationaryReplacement.lean 3 declarations
- OscillatoryExpansion.lean 3 declarations
- OscillatoryTaylor.lean 7 declarations
- ParametricJets.lean 4 declarations
- ParentInactiveKernel.lean 1 declarations
- PhaseIntegration.lean 6 declarations
- PlaneFourierNonstationary.lean 2 declarations
- PoleCutoffs.lean 17 declarations
- PoleStationarySupport.lean 11 declarations
- PolicyJetChildren.lean 4 declarations
- PolicyJetData.lean 9 declarations
- PositiveDistanceSpatialKernel.lean 4 declarations
- PositiveFourier.lean 3 declarations
- ProductFilterIntegral.lean 3 declarations
- ProfileDerivativePoint.lean 1 declarations
- ProfileMergeCutoff.lean 1 declarations
- PublishedQuadraticStationary.lean 4 declarations
- QuadraticGaussianPairing.lean 3 declarations
- QuadraticIntegral.lean 4 declarations
- QuadraticJacobian.lean 6 declarations
- QuadraticKernelBounds.lean 3 declarations
- QuadraticStationary.lean 8 declarations
- ReachedMaskJets.lean 6 declarations
- RootFourierError.lean 4 declarations
- RootKernelTerms.lean 2 declarations
- RootNormalizedKernel.lean 3 declarations
- RootPairSymbols.lean 10 declarations
- RootUniformFourier.lean 2 declarations
- RotatedInverseIntegration.lean 5 declarations
- RotatedInverseSymbols.lean 9 declarations
- RotatedMaskedJetShell.lean 1 declarations
- SafeStationaryChart.lean 12 declarations
- ScaledInverseIntegration.lean 4 declarations
- SchwartzFourierMomentBounds.lean 5 declarations
- SchwartzFourierMoments.lean 2 declarations
- SchwartzLpTests.lean 6 declarations
- SeparatedInverseIntegration.lean 5 declarations
- SeparatedJets.lean 17 declarations
- SignedStationary.lean 7 declarations
- SmoothKernel.lean 11 declarations
- SmoothMask.lean 4 declarations
- SmoothMaskDerivatives.lean 2 declarations
- SmoothReciprocal.lean 5 declarations
- SpatialAnnulusKernel.lean 7 declarations
- SpatialFourierIntegration.lean 5 declarations
- SpatialFourierSeparation.lean 11 declarations
- SpatialFourierTests.lean 3 declarations
- SpatialPhasedSymbols.lean 6 declarations
- SpatialSymbols.lean 2 declarations
- StationaryCoefficients.lean 6 declarations
- StationaryFactorShell.lean 1 declarations
- StationaryInverse.lean 17 declarations
- StationaryScales.lean 4 declarations
- StationaryShellIntegrability.lean 1 declarations
- StationaryTransport.lean 10 declarations
- StationaryWeightCancellation.lean 3 declarations
- SymbolOrder.lean 6 declarations
- SymbolProduct.lean 7 declarations
- SymbolProductBounds.lean 3 declarations
- TwoProfileDerivatives.lean 1 declarations
- TwoProfileInverseIntegration.lean 2 declarations
- UniformJetBudget.lean 4 declarations
- UniformSymbolScale.lean 5 declarations
- WeightedDistanceFourier.lean 3 declarations
- WeightedDistanceLowFrequency.lean 3 declarations
- WeightedDistancePositiveKernel.lean 2 declarations