OAI/Analysis/Conductivity/Fourier/
695 declarations, 0 contain sorry, 0 declared as axioms; 81 files
Files
- AffineFourierField.lean 8 declarations
- AnalyticDerivativeBounds.lean 6 declarations
- AnalyticNull.lean 11 declarations
- AnalyticNullEuclidean.lean 3 declarations
- AngularFourierConjugacy.lean 18 declarations
- AngularIntegratedTrace.lean 8 declarations
- AngularIntegration.lean 2 declarations
- AngularInverseTensor.lean 13 declarations
- AngularLocalizedMoments.lean 7 declarations
- AngularMeasureExact.lean 6 declarations
- AngularNormalTrace.lean 15 declarations
- AngularPeriodization.lean 19 declarations
- AngularPhaseTranslation.lean 6 declarations
- AngularSignedTrace.lean 4 declarations
- AttachedEndPoisson.lean 13 declarations
- AttachedPeriodicDerivative.lean 3 declarations
- AttachedPeriodicFlux.lean 6 declarations
- AttachedPeriodicGreen.lean 1 declarations
- CascadePeriodicity.lean 14 declarations
- CollarAngularInverse.lean 16 declarations
- CompactifiedFourierTail.lean 11 declarations
- CylinderFourier.lean 13 declarations
- CylinderFourierComplete.lean 14 declarations
- CylinderFourierGraph.lean 4 declarations
- CylinderModeGreen.lean 9 declarations
- CylinderPoissonTrace.lean 6 declarations
- EndPoissonDifferential.lean 15 declarations
- EndPoissonJets.lean 26 declarations
- EndPoissonRepresentative.lean 16 declarations
- EndingJoinMiddleModel.lean 8 declarations
- EndingJoinPeriodicity.lean 2 declarations
- FlatFourierFlux.lean 5 declarations
- FourierEndConcomitant.lean 2 declarations
- FourierEndFlux.lean 1 declarations
- FourierFiniteEnding.lean 1 declarations
- FourierFiniteEndingNormal.lean 1 declarations
- FourierMatchingElliptic.lean 5 declarations
- FourierMatchingFamilyCorrection.lean 4 declarations
- FourierMatchingInterpolation.lean 21 declarations
- FourierMatchingLocalData.lean 9 declarations
- FourierPairFlux.lean 14 declarations
- GeneralModeFiniteEndNormal.lean 12 declarations
- GeneralModeRecombinedEnding.lean 1 declarations
- LeadingFrequencyAlignment.lean 10 declarations
- LinearPhaseDerivativeIntegralBound.lean 2 declarations
- ModeConnector.lean 18 declarations
- PeriodicAveragingSmooth.lean 2 declarations
- PeriodicBandCompactness.lean 9 declarations
- PeriodicFamilyCorrection.lean 7 declarations
- PoissonGreen.lean 2 declarations
- PoissonTraceRate.lean 11 declarations
- PureMode.lean 10 declarations
- PureModeFamilyLocalCorrection.lean 5 declarations
- PureModeWall.lean 9 declarations
- PureModeWallRegion.lean 1 declarations
- RectangularRayTrace.lean 12 declarations
- RectangularTorusAtlas.lean 26 declarations
- RectangularTorusInverse.lean 13 declarations
- SmoothAngularCutoff.lean 12 declarations
- SmoothHarmonicAnalytic.lean 3 declarations
- SmoothPhase.lean 4 declarations
- SpectralAffineCovector.lean 2 declarations
- SpectralExtensionMono.lean 4 declarations
- SpectralExtensionNonemptyNonempty.lean 2 declarations
- SpectralTerminalIntegral.lean 5 declarations
- SpectralTerminalL2.lean 5 declarations
- SpectralTrace.lean 4 declarations
- TorusDirectionalFourier.lean 4 declarations
- TorusFlatMode.lean 15 declarations
- TorusFourierAnalytic.lean 6 declarations
- TorusFourierSmooth.lean 8 declarations
- TorusFourierTranslation.lean 13 declarations
- TorusLeadingRealMode.lean 18 declarations
- TorusNonresonance.lean 9 declarations
- TorusPeriodicDescent.lean 10 declarations
- TorusPoissonContinuous.lean 11 declarations
- TorusPoissonFlow.lean 8 declarations
- TorusSmoothModeJet.lean 10 declarations
- TorusSpectralContinuation.lean 9 declarations
- UndoAngularProperties.lean 7 declarations
- UndoAngularWeakPair.lean 10 declarations