`OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/`

610 declarations, 0 contain sorry, 0 declared as axioms; 180 files

Files

BlowupRate.lean 3 declarations
BoundedInnerNull.lean 1 declarations
ClassicalMaximalFlow.lean 2 declarations
ConditionalMain.lean 2 declarations
ContinuousCutoffStableOrbit.lean 3 declarations
ContinuousTorusAssembly.lean 1 declarations
ContinuousTorusCoordinateData.lean 3 declarations
ContinuousTorusCoordinateTransfer.lean 3 declarations
ContinuousTorusDiscreteData.lean 2 declarations
ContinuousTorusFrame.lean 2 declarations
ContinuousTorusLinearStep.lean 2 declarations
ContinuousTorusSequence.lean 1 declarations
CutoffAnnulusUniform.lean 2 declarations
CutoffApproximateMode.lean 9 declarations
CutoffContinuousDiagonalStep.lean 1 declarations
CutoffContinuousLinearization.lean 2 declarations
CutoffContinuousStep.lean 1 declarations
CutoffContourTransfer.lean 1 declarations
CutoffCoordinateInverse.lean 2 declarations
CutoffCoordinateLinearData.lean 1 declarations
CutoffCoordinateOperator.lean 1 declarations
CutoffCoordinateTransfer.lean 1 declarations
CutoffDiagonalLinearStep.lean 1 declarations
CutoffDiagonalTransfer.lean 1 declarations
CutoffDirectionalError.lean 3 declarations
CutoffEndpointContinuity.lean 1 declarations
CutoffFamilyContinuity.lean 13 declarations
CutoffFiniteJets.lean 5 declarations
CutoffForcingHistory.lean 10 declarations
CutoffFourierDefect.lean 10 declarations
CutoffGlobalOrbit.lean 5 declarations
CutoffLaplacian.lean 7 declarations
CutoffLinearizedPropagator.lean 2 declarations
CutoffLocalExistence.lean 1 declarations
CutoffMildEquation.lean 3 declarations
CutoffMildResidual.lean 5 declarations
CutoffMixedTaylor.lean 1 declarations
CutoffModulationTaylor.lean 1 declarations
CutoffMovingPath.lean 4 declarations
CutoffNonlinearStep.lean 1 declarations
CutoffNormalizedEquation.lean 2 declarations
CutoffPathContinuity.lean 3 declarations
CutoffPhysicalTranslation.lean 1 declarations
CutoffPicardResidual.lean 3 declarations
CutoffPointwiseBound.lean 2 declarations
CutoffProfileCompactApproximation.lean 1 declarations
CutoffProfileCoordinateLimit.lean 1 declarations
CutoffProfileEndpoint.lean 3 declarations
CutoffProfileModeDerivative.lean 4 declarations
CutoffProfilePhysicalLimit.lean 3 declarations
CutoffProfileTailAssembly.lean 2 declarations
CutoffProfileTailBound.lean 1 declarations
CutoffRemainderContinuity.lean 1 declarations
CutoffResidualCoefficients.lean 12 declarations
CutoffResidualDuhamel.lean 3 declarations
CutoffResidualJets.lean 11 declarations
CutoffResidualSampling.lean 4 declarations
CutoffResidualScaling.lean 5 declarations
CutoffStableBlowup.lean 3 declarations
CutoffStableOrbit.lean 2 declarations
CutoffStableSequence.lean 1 declarations
CutoffStableTransfer.lean 2 declarations
CutoffStepForcing.lean 4 declarations
CutoffStepLinearization.lean 3 declarations
CutoffStepRemainder.lean 6 declarations
CutoffSymbolSampling.lean 1 declarations
CutoffTimeLipschitz.lean 2 declarations
CutoffTranslationTaylor.lean 1 declarations
CutoffTransport.lean 6 declarations
DiagonalCoordinateStableOrbit.lean 2 declarations
DiagonalCutoffBlowup.lean 1 declarations
DiagonalCutoffStableOrbit.lean 2 declarations
DiagonalRealCoordinates.lean 5 declarations
ExponentialModulationTaylor.lean 2 declarations
FiniteCoordinateComplete.lean 1 declarations
FiniteGaussian.lean 7 declarations
FiniteGeneratorNoJordan.lean 2 declarations
FiniteInvariantInverse.lean 3 declarations
FiniteOperatorConvergence.lean 2 declarations
FiniteSymmetryBackward.lean 4 declarations
FiniteSymmetryCoordinates.lean 5 declarations
FiniteSymmetryDecay.lean 1 declarations
FiniteSymmetryDecomposition.lean 3 declarations
FiniteSymmetryDimension.lean 1 declarations
FixedCutoffProfileBound.lean 2 declarations
FixedCutoffProfileDerivative.lean 4 declarations
FixedCutoffProfileIdentity.lean 1 declarations
FixedCutoffProfileTaylor.lean 2 declarations
FlatStableGraphIntersection.lean 1 declarations
GaussianBlocks.lean 4 declarations
GaussianCounterexample.lean 1 declarations
GaussianEnclosure.lean 14 declarations
GaussianFourier.lean 11 declarations
GaussianFullSupport.lean 5 declarations
GaussianMoments.lean 3 declarations
GaussianRealization.lean 11 declarations
GaussianSmallBalls.lean 6 declarations
GaussianSupport.lean 5 declarations
LocalUniformSubsequence.lean 1 declarations
LocalWeightedCompact.lean 2 declarations
MaximalSobolevEndpoint.lean 9 declarations
MaximalSobolevFlow.lean 12 declarations
MaximalStrongSolution.lean 3 declarations
NormalizedFrameLowerBound.lean 2 declarations
NormalizedStableGraphIntersection.lean 2 declarations
NormedCurveTaylor.lean 1 declarations
OddPowerMixedIncrement.lean 2 declarations
OddPowerNonlinearity.lean 5 declarations
ParameterBoxHomotopy.lean 6 declarations
ParameterChoice.lean 3 declarations
ParameterOpenness.lean 6 declarations
PhysicalCharacterLipschitz.lean 3 declarations
PhysicalCoordinateFrame.lean 4 declarations
PhysicalCoordinateOpen.lean 1 declarations
PhysicalCoordinateStableOrbit.lean 1 declarations
PhysicalCutoffBlowup.lean 2 declarations
PhysicalCutoffOrbit.lean 1 declarations
PhysicalDiagonalCoordinates.lean 1 declarations
PhysicalFourierTest.lean 3 declarations
PhysicalFrameSampling.lean 3 declarations
PhysicalFrameSymbols.lean 5 declarations
PhysicalLowDegreeMoments.lean 4 declarations
PhysicalModeRateBound.lean 2 declarations
PhysicalModulationBound.lean 1 declarations
PhysicalModulationBudget.lean 1 declarations
PhysicalModulationCoordinates.lean 1 declarations
PhysicalModulationParameters.lean 2 declarations
PhysicalModulationRadius.lean 7 declarations
PhysicalModulationTaylor.lean 2 declarations
PhysicalOpenStableOrbit.lean 1 declarations
PhysicalParameterZero.lean 1 declarations
PhysicalQuadraticWeight.lean 1 declarations
PhysicalReferenceModulation.lean 5 declarations
PhysicalStartingChartBounds.lean 3 declarations
PhysicalStartingData.lean 8 declarations
PhysicalStartingFunction.lean 3 declarations
PhysicalStartingInverse.lean 2 declarations
ProjectionCoordinates.lean 6 declarations
RandomSeries.lean 1 declarations
SampledPhysicalFrame.lean 5 declarations
SampledSchwartzFrame.lean 5 declarations
SmallComplexPower.lean 3 declarations
StableCoordinateBackwardBound.lean 1 declarations
StableEndpointContinuity.lean 1 declarations
StableEndpointCoordinateBound.lean 2 declarations
StableFixedPointEndpoint.lean 1 declarations
StableFrameContinuity.lean 5 declarations
StableGraphApplication.lean 1 declarations
StableGraphBackward.lean 8 declarations
StableGraphContinuity.lean 1 declarations
StableGraphContraction.lean 4 declarations
StableGraphCoordinateContinuity.lean 2 declarations
StableGraphCoordinateZero.lean 1 declarations
StableGraphEndpoint.lean 1 declarations
StableGraphForward.lean 7 declarations
StableGraphFrameBounds.lean 15 declarations
StableGraphParameterSelection.lean 2 declarations
StableGraphParameterZero.lean 1 declarations
StableGraphPointSources.lean 10 declarations
StableGraphProjectedRecurrence.lean 2 declarations
StableGraphReconstruction.lean 11 declarations
StableGraphRecurrence.lean 3 declarations
StableGraphSelection.lean 3 declarations
StableGraphSequence.lean 6 declarations
StableGraphSlabGluing.lean 12 declarations
StableGraphSmallRemainder.lean 1 declarations
StableGraphSourceIdentity.lean 5 declarations
StableGraphSplitSource.lean 2 declarations
StableGraphStepDecay.lean 1 declarations
StableGraphWeightedSource.lean 10 declarations
StableProjectionEigenvector.lean 1 declarations
StableSmallRemainderContinuity.lean 1 declarations
StableWeightedContinuity.lean 1 declarations
StableWeightedLocalContinuity.lean 1 declarations
StrongOperatorDerivative.lean 1 declarations
SymmetryRangeGenerator.lean 1 declarations
UnitTorusCoefficients.lean 9 declarations
UnitTorusPhysical.lean 2 declarations
UnitTorusPolynomial.lean 6 declarations
WeightedEnergyEstimate.lean 2 declarations