`OAI/Analysis/LipschitzHilbert/Fourier/`

1549 declarations, 0 contain sorry, 0 declared as axioms; 343 files

Files

ActualBandHigh.lean 1 declarations
ActualCutoffBandHigh.lean 3 declarations
ActualErrorConvolution.lean 2 declarations
ActualScalarBandBounds.lean 2 declarations
AnnularBandL1.lean 2 declarations
AnnularBinMultiplier.lean 2 declarations
AnnularBinPairing.lean 1 declarations
AnnularBoundedSynthesis.lean 4 declarations
AnnularCutoffConstruction.lean 13 declarations
AnnularEnlargement.lean 7 declarations
AnnularFrequencyEnvelope.lean 3 declarations
AnnularL2Resolution.lean 5 declarations
AnnularPVCommutatorSquare.lean 5 declarations
AnnularPVFromNarrow.lean 5 declarations
AnnularPVPartialBound.lean 3 declarations
AnnularPVReconstruction.lean 5 declarations
AnnularPartitionIdentities.lean 6 declarations
AnnularPositiveCutoff.lean 10 declarations
AnnularResolutionSymbols.lean 9 declarations
AnnularSchwartzResolution.lean 5 declarations
AnnularSelector.lean 11 declarations
AnnularSlopePartition.lean 2 declarations
AnnularSquareBound.lean 7 declarations
AnnularSymbolForm.lean 2 declarations
BandAmplitudeError.lean 1 declarations
BandAmplitudeHigh.lean 1 declarations
BandAmplitudeSum.lean 1 declarations
BandAverageComparison.lean 10 declarations
BandFiniteAmplitudeBound.lean 1 declarations
BandL2Pairing.lean 5 declarations
BandMeasurableHigh.lean 1 declarations
BandOrthogonality.lean 4 declarations
BandProjectedHigh.lean 1 declarations
BandRetainedApproximation.lean 1 declarations
BandRetainedDecay.lean 1 declarations
BandToFullProof.lean 1 declarations
BoundedConvolutionComposition.lean 5 declarations
BoundedConvolutionL2.lean 4 declarations
BoundedConvolutionL4.lean 4 declarations
BoundedFrequencyMultiplier.lean 4 declarations
BoundedVerticalMultiplier.lean 6 declarations
CenteredBandProjection.lean 5 declarations
ComplexBandAverage.lean 13 declarations
ComplexLineAverage.lean 10 declarations
ConvolutionBasicL1.lean 2 declarations
ConvolutionLayerTail.lean 2 declarations
ConvolutionPowerTail.lean 10 declarations
ConvolutionThird.lean 5 declarations
CoordinateFourierSupport.lean 4 declarations
CovariantLineMotion.lean 3 declarations
DemodulatedVertical.lean 8 declarations
DominatedKernelAverage.lean 1 declarations
DyadicAnnularSeparation.lean 1 declarations
DyadicAnnularVariation.lean 4 declarations
DyadicCommutatorCutoff.lean 8 declarations
DyadicKernelTelescoping.lean 3 declarations
DyadicLineBad.lean 5 declarations
DyadicLineCarleson.lean 2 declarations
DyadicLineCount.lean 9 declarations
DyadicLineCountableTail.lean 1 declarations
DyadicLineFiniteTail.lean 1 declarations
DyadicLineMaximal.lean 3 declarations
DyadicLineNesting.lean 7 declarations
DyadicLineResolution.lean 10 declarations
DyadicLineRootCount.lean 7 declarations
DyadicLineRoots.lean 6 declarations
DyadicProjectionCarleson.lean 4 declarations
DyadicResolutionSymbol.lean 7 declarations
DyadicSmoothCutoff.lean 9 declarations
ErrorLineConcentration.lean 4 declarations
FiniteBandDerivative.lean 6 declarations
FiniteBandMultiplier.lean 5 declarations
FiniteLineAverage.lean 3 declarations
FiniteLineCells.lean 6 declarations
FiniteNormalizedKernelForm.lean 1 declarations
FiniteSeparatedSymbolBound.lean 1 declarations
FiniteSeparatedSymbolBoundL1.lean 1 declarations
FiniteTimeKernelMoment.lean 8 declarations
FiniteUnitSymbolPairing.lean 2 declarations
FiniteUnitSymbolPairingL1.lean 2 declarations
FiniteVerticalBins.lean 10 declarations
FourierAveragingConvolution.lean 9 declarations
FourierAveragingKernel.lean 9 declarations
FourierAveragingMeasure.lean 11 declarations
FourierAveragingMixture.lean 4 declarations
FourierAveragingScale.lean 5 declarations
FourierAveragingTail.lean 6 declarations
FourierHomogeneity.lean 6 declarations
FourierKernelFirstMoment.lean 7 declarations
FrequencyKernelTranslations.lean 4 declarations
FrequencyProfileNormalization.lean 4 declarations
GeneralAnnularComparison.lean 5 declarations
GeneralAnnularErrors.lean 2 declarations
GeneralAnnularVariation.lean 2 declarations
GlobalAnnularVariation.lean 6 declarations
GlobalBandLocalization.lean 2 declarations
GlobalBandOperator.lean 4 declarations
GlobalBandPrincipalValue.lean 4 declarations
HighFrequencyAverage.lean 2 declarations
HilbertAnnularVariation.lean 4 declarations
HilbertCutoffDerivative.lean 4 declarations
HilbertCutoffNormalization.lean 3 declarations
HilbertCutoffProfile.lean 13 declarations
HilbertFiniteSymbol.lean 6 declarations
HilbertFourierGain.lean 1 declarations
KernelAverageBound.lean 1 declarations
KernelAverageEnergy.lean 1 declarations
KernelAverageL1.lean 2 declarations
KernelDifferencePairing.lean 4 declarations
KernelPairing.lean 6 declarations
L1FactoredConvolution.lean 2 declarations
L1FourierConvolution.lean 3 declarations
L1FrequencyMultiplier.lean 6 declarations
L1MultiplierLinearity.lean 6 declarations
LatticeCoefficientConvolution.lean 1 declarations
LineAnnularSum.lean 3 declarations
LineBandedCommutatorEnergy.lean 1 declarations
LineBoundedCommutatorL2.lean 8 declarations
LineCommutatorCoefficientLimit.lean 2 declarations
LineCommutatorDerivative.lean 5 declarations
LineCommutatorEnergy.lean 4 declarations
LineCommutatorLinearity.lean 7 declarations
LineCompositionLimit.lean 3 declarations
LineConjugationBound.lean 4 declarations
LineConjugationDerivative.lean 2 declarations
LineConvolutionContinuity.lean 2 declarations
LineConvolutionEnergy.lean 6 declarations
LineConvolutionFourth.lean 3 declarations
LineConvolutionL4.lean 5 declarations
LineConvolutionLocal.lean 2 declarations
LineConvolutionPairing.lean 3 declarations
LineCountSlab.lean 3 declarations
LineCounting.lean 1 declarations
LineDerivativeCommutatorL2.lean 9 declarations
LineDyadicReconstructionEnergy.lean 4 declarations
LineDyadicSpectrum.lean 4 declarations
LineDyadicTelescoping.lean 5 declarations
LineFrequencyProjection.lean 11 declarations
LineGeometricSchur.lean 6 declarations
LineHighLowEnergy.lean 3 declarations
LineHighLowSpectrum.lean 5 declarations
LineHighLowSum.lean 6 declarations
LineKernelCancellation.lean 5 declarations
LineKernelDecay.lean 5 declarations
LineKernelMaximal.lean 2 declarations
LineKernelOscillation.lean 4 declarations
LineKernelScaling.lean 4 declarations
LineLatticeEnvelope.lean 6 declarations
LineLocalizedMultiplier.lean 4 declarations
LineLowHighCommutator.lean 4 declarations
LineLowHighSpectrum.lean 2 declarations
LineLowHighSum.lean 2 declarations
LineLowpassCell.lean 4 declarations
LineLpDerivative.lean 3 declarations
LineMollification.lean 6 declarations
LineNeighborhoodMoments.lean 1 declarations
LineProductSpectrum.lean 7 declarations
LineProjectionDerivative.lean 2 declarations
LineProjectionFourth.lean 4 declarations
LineProjectionKernel.lean 4 declarations
LineProjectionLipschitz.lean 3 declarations
LineSamplingDecay.lean 5 declarations
LineSamplingEnergy.lean 7 declarations
LineSamplingGenerator.lean 9 declarations
LineSamplingHomeomorph.lean 7 declarations
LineSamplingInverse.lean 8 declarations
LineSamplingInverseDerivative.lean 4 declarations
LineSamplingKernelCommutator.lean 2 declarations
LineSamplingSchwartz.lean 10 declarations
LineSamplingStrongDerivative.lean 6 declarations
LineSchwartzCommutatorEstimate.lean 2 declarations
LineSchwartzPairing.lean 4 declarations
LineSmoothCarleson.lean 3 declarations
LineTiling.lean 5 declarations
LineWeightAverage.lean 3 declarations
LocalAnnularVariation.lean 6 declarations
LocalizedAnnularVariation.lean 3 declarations
LocalizedBandOperator.lean 3 declarations
LocalizedBandStrong.lean 7 declarations
LocalizedSymbolIdentity.lean 2 declarations
LocalizedSymbolOperator.lean 2 declarations
LongLineVariation.lean 1 declarations
LongPositiveConvolution.lean 1 declarations
MeasureClassKernel.lean 6 declarations
ModulatedInverse.lean 5 declarations
ModulatedInverseL1.lean 1 declarations
NarrowBandCutoff.lean 14 declarations
NegativeBandOperator.lean 2 declarations
NormalizedBandProjection.lean 8 declarations
NormalizedBandSymbol.lean 9 declarations
NormalizedBasicConvolution.lean 1 declarations
NormalizedConvolutionForm.lean 4 declarations
NormalizedHighConvolution.lean 1 declarations
NormalizedReverseConvolution.lean 1 declarations
NormalizedSymbolBasicL1.lean 1 declarations
NormalizedSymbolFamily.lean 10 declarations
NormalizedSymbolForm.lean 3 declarations
NormalizedSymbolFormL1.lean 3 declarations
NormalizedSymbolHighL1.lean 1 declarations
NormalizedSymbolRepresentation.lean 5 declarations
NormalizedSymbolReverseL1.lean 1 declarations
PVCommutatorSymbolLinearity.lean 4 declarations
PartitionedAnnularBasicL1.lean 1 declarations
PartitionedAnnularForm.lean 2 declarations
PartitionedAnnularFormL1.lean 2 declarations
PartitionedAnnularHighL1.lean 1 declarations
PartitionedAnnularReverseL1.lean 1 declarations
PartitionedBandForm.lean 2 declarations
PartitionedBandFormL1.lean 2 declarations
PartitionedFrequencyL1.lean 1 declarations
PartitionedFrequencySymbol.lean 6 declarations
PartitionedSymbolIdentity.lean 3 declarations
PhysicalPlanarJet.lean 3 declarations
PlanarCovariantJet.lean 9 declarations
PlanarModulatedJet.lean 6 declarations
PlanarPositiveConvolution.lean 3 declarations
PlanarSchwartzDecay.lean 7 declarations
PlanarSchwartzInversion.lean 5 declarations
PlanarSchwartzSlice.lean 7 declarations
PlanarSliceFourier.lean 3 declarations
PlanarSliceFourierBasic.lean 8 declarations
PlanarSliceFourierDerivative.lean 14 declarations
PlanarSliceFourierSupport.lean 5 declarations
PlaneLineWeakL1.lean 6 declarations
PlaneVerticalLipschitz.lean 2 declarations
PolynomialLineFamily.lean 10 declarations
PositiveConvolution.lean 9 declarations
PositiveConvolutionOscillation.lean 2 declarations
PositiveLineKernel.lean 6 declarations
PositiveLineMaximal.lean 10 declarations
ProductPVLinear.lean 4 declarations
ProductPVVerticalDecay.lean 2 declarations
Projection.lean 17 declarations
ProjectionFiberGeometry.lean 3 declarations
PublishedBandReductionInput.lean 1 declarations
RectangularFrequencyCutoff.lean 6 declarations
ReferenceLineCount.lean 5 declarations
ReflectedBandProjection.lean 6 declarations
RescaledAnnularSymbol.lean 3 declarations
RescaledPartitionedSymbol.lean 4 declarations
RestrictedSchwartzSizes.lean 4 declarations
ScalarBandKernel.lean 2 declarations
ScalarLineVariation.lean 8 declarations
ScaledAnnularVariation.lean 3 declarations
ScaledConvolutionLimits.lean 3 declarations
ScaledFrequencyWindows.lean 7 declarations
ScaledWindowFourier.lean 3 declarations
SchwartzBandEnergy.lean 4 declarations
SchwartzBandPrimitive.lean 3 declarations
SchwartzConjugation.lean 5 declarations
SchwartzDilation.lean 8 declarations
SchwartzGlobalLipschitz.lean 2 declarations
SchwartzProfileBounds.lean 2 declarations
SchwartzVerticalProjection.lean 5 declarations
SeparatedSymbolFourier.lean 9 declarations
SeparatedSymbolOperator.lean 3 declarations
SeparatedSymbolPairing.lean 1 declarations
SeparatedSymbolPairingL1.lean 1 declarations
SharpBandHigh.lean 2 declarations
SharpBandHighAll.lean 2 declarations
SharpBandMeasurableRestricted.lean 4 declarations
SharpBandRestrictedLog.lean 2 declarations
SharpBandScalarEndpoints.lean 2 declarations
SharpBandUniformHigh.lean 1 declarations
SharpKernelComparison.lean 6 declarations
SharpKernelL1.lean 1 declarations
SharpKernelSymmetrization.lean 1 declarations
SharpVerticalCommutator.lean 6 declarations
ShiftedLineAverage.lean 4 declarations
ShortKernelPairing.lean 1 declarations
ShortLineVariation.lean 1 declarations
ShortPositiveConvolution.lean 1 declarations
ShortSlopeLinearity.lean 3 declarations
ShortVerticalDifference.lean 5 declarations
ShortVerticalDifferenceL1.lean 1 declarations
ShortVerticalError.lean 5 declarations
SignedAnnularOperator.lean 7 declarations
SignedAnnularSymbol.lean 11 declarations
SimpleFourierPairing.lean 13 declarations
SincMask.lean 6 declarations
SincMaskFourier.lean 9 declarations
SincMaskMotion.lean 8 declarations
SincMaskSchwartz.lean 21 declarations
SincMaskSpectrum.lean 4 declarations
SincMaskedLine.lean 7 declarations
SkippedLineAverage.lean 6 declarations
SmoothPrincipalValueLinear.lean 5 declarations
SmoothSlopeSymbol.lean 14 declarations
SquareLineConcentration.lean 16 declarations
StripProjection.lean 2 declarations
SymbolAverageBound.lean 1 declarations
SymbolSlice.lean 10 declarations
SymbolWeights.lean 10 declarations
TileEnvelopeKernel.lean 5 declarations
UniformLineMoments.lean 2 declarations
UnitConvolutionParameter.lean 5 declarations
UnitConvolutionWeight.lean 2 declarations
UnitConvolutionWeightL1.lean 2 declarations
UnitSymbolPairing.lean 1 declarations
UnitSymbolPairingL1.lean 1 declarations
VariableEndpointKernel.lean 7 declarations
VariationLineBMO.lean 3 declarations
VerticalBernstein.lean 3 declarations
VerticalBinAdjoint.lean 2 declarations
VerticalBinCommutator.lean 3 declarations
VerticalBinCost.lean 4 declarations
VerticalBinEnergy.lean 6 declarations
VerticalBinKernel.lean 9 declarations
VerticalBinLpEnergy.lean 7 declarations
VerticalBinLpReconstruction.lean 4 declarations
VerticalBinPlateau.lean 7 declarations
VerticalBinProfile.lean 12 declarations
VerticalBinReconstruction.lean 3 declarations
VerticalBinVector.lean 9 declarations
VerticalCommutatorAverage.lean 2 declarations
VerticalCommutatorEnergy.lean 1 declarations
VerticalConvolutionL1.lean 8 declarations
VerticalConvolutionL2.lean 3 declarations
VerticalConvolutionLp.lean 9 declarations
VerticalConvolutionPVLimit.lean 3 declarations
VerticalDifferenceEnergy.lean 1 declarations
VerticalErrorSources.lean 3 declarations
VerticalHorizontalCutoff.lean 4 declarations
VerticalInverseMultiplier.lean 2 declarations
VerticalKernelMoment.lean 4 declarations
VerticalL2Projection.lean 6 declarations
VerticalMoment.lean 4 declarations
VerticalNeighborhood.lean 2 declarations
VerticalProjectionAlgebra.lean 4 declarations
VerticalProjectionDerivative.lean 4 declarations
VerticalSamplingCommutator.lean 3 declarations
VerticalSamplingDifference.lean 2 declarations
VerticalSamplingGeometry.lean 7 declarations
VerticalSamplingMihlin.lean 4 declarations
VerticalSecantEnergy.lean 4 declarations
VerticalSelfAdjoint.lean 2 declarations
VerticalSlopeCommutation.lean 3 declarations
VerticalSymbolBound.lean 2 declarations
VerticalWeight.lean 3 declarations
VerticalWindowRescaling.lean 6 declarations
VerticalWindowRescalingL1.lean 1 declarations
WitnessLineAverage.lean 6 declarations
WitnessProjection.lean 2 declarations