OAI/MathematicalPhysics/DefocusingNLS/Certificates.lean
0 declarations, 0 contain sorry, 0 declared as axioms
Exact arithmetic and complex-analytic certificates for profile matching.
This file declares nothing itself. It gathers the 28 imports below, so a file that imports it gets all of them.
Imports
- OAI.MathematicalPhysics.DefocusingNLS.Certificates.ApproximateNullLimit
- OAI.MathematicalPhysics.DefocusingNLS.Certificates.BoundaryMatchingExclusion
- OAI.MathematicalPhysics.DefocusingNLS.Certificates.CompactFamilyIntegral
- OAI.MathematicalPhysics.DefocusingNLS.Certificates.ComplexPowerBound
- OAI.MathematicalPhysics.DefocusingNLS.Certificates.ContinuousCoordinateStableOrbit
- OAI.MathematicalPhysics.DefocusingNLS.Certificates.ContinuousDiagonalStableOrbit
- OAI.MathematicalPhysics.DefocusingNLS.Certificates.ContinuousHalfLineBound
- OAI.MathematicalPhysics.DefocusingNLS.Certificates.ContinuousSampledFrame
- OAI.MathematicalPhysics.DefocusingNLS.Certificates.CorrectedTorusFrame
- OAI.MathematicalPhysics.DefocusingNLS.Certificates.FreeLimitingModel
- OAI.MathematicalPhysics.DefocusingNLS.Certificates.FreePhysicalGeneralizedExclusion
- OAI.MathematicalPhysics.DefocusingNLS.Certificates.FreeRadialEquation
- OAI.MathematicalPhysics.DefocusingNLS.Certificates.FreeSimpleZeros
- OAI.MathematicalPhysics.DefocusingNLS.Certificates.InteriorDerivativeLipschitz
- OAI.MathematicalPhysics.DefocusingNLS.Certificates.KernelOperatorBound
- OAI.MathematicalPhysics.DefocusingNLS.Certificates.LaguerreRapidDecay
- OAI.MathematicalPhysics.DefocusingNLS.Certificates.LowWeightInterpolation
- OAI.MathematicalPhysics.DefocusingNLS.Certificates.MatchingBasisChange
- OAI.MathematicalPhysics.DefocusingNLS.Certificates.MatchingMatrixSimpleZero
- OAI.MathematicalPhysics.DefocusingNLS.Certificates.MixedFourierLocalization
- OAI.MathematicalPhysics.DefocusingNLS.Certificates.RationalComplexMatrix
- OAI.MathematicalPhysics.DefocusingNLS.Certificates.RectangleHomotopyCount
- OAI.MathematicalPhysics.DefocusingNLS.Certificates.RectangleRouche
- OAI.MathematicalPhysics.DefocusingNLS.Certificates.ScaledLatticeKernel
- OAI.MathematicalPhysics.DefocusingNLS.Certificates.SimilarityLimit
- OAI.MathematicalPhysics.DefocusingNLS.Certificates.TailCone
- OAI.MathematicalPhysics.DefocusingNLS.Certificates.UniformHorizontalExclusion
- OAI.MathematicalPhysics.DefocusingNLS.Certificates.ZeroTailParameterContinuity