OAI/MathematicalPhysics/DefocusingNLS/Certificates/
942 declarations, 0 contain sorry, 0 declared as axioms; 172 files
Files
- AnalyticMatchingColumn.lean 7 declarations
- ApproximateNullLimit.lean 1 declarations
- BoundaryCertificateArithmetic.lean 17 declarations
- BoundaryCertificatePositivity.lean 12 declarations
- BoundaryCertificateSemantics.lean 8 declarations
- BoundaryChartCover.lean 1 declarations
- BoundaryDeterminantPositivity.lean 5 declarations
- BoundaryDiagonalCertificate.lean 5 declarations
- BoundaryEnclosureDeterminant.lean 10 declarations
- BoundaryEnclosureInputs.lean 5 declarations
- BoundaryEnclosureState.lean 7 declarations
- BoundaryEnclosureStateLink.lean 9 declarations
- BoundaryEvenCoefficients.lean 3 declarations
- BoundaryEvenPolynomial.lean 4 declarations
- BoundaryFormEvaluation.lean 6 declarations
- BoundaryForwardScaling.lean 7 declarations
- BoundaryHermitianPolynomial.lean 12 declarations
- BoundaryHornerEvaluation.lean 7 declarations
- BoundaryHornerTransform.lean 10 declarations
- BoundaryMatchingExclusion.lean 5 declarations
- BoundaryPolynomial.lean 10 declarations
- BoundaryPolynomialDegree.lean 18 declarations
- BoundaryPolynomialParity.lean 14 declarations
- BoundaryPositiveEvaluation.lean 4 declarations
- BoundaryPositiveForm.lean 7 declarations
- CenteredPolynomial.lean 6 declarations
- CentralOutgoingCount.lean 1 declarations
- CentralZeroTailCount.lean 2 declarations
- CompactFamilyIntegral.lean 2 declarations
- ComplexPowerBound.lean 3 declarations
- ContinuousCoordinateSequence.lean 1 declarations
- ContinuousCoordinateStableOrbit.lean 2 declarations
- ContinuousDiagonalLinearStep.lean 2 declarations
- ContinuousDiagonalStableOrbit.lean 2 declarations
- ContinuousHalfLineBound.lean 3 declarations
- ContinuousSampledFrame.lean 2 declarations
- CorrectedTorusFrame.lean 3 declarations
- ExteriorCertificatePositivity.lean 3 declarations
- ExteriorCertificateRecipe.lean 11 declarations
- ExteriorFormBounds.lean 7 declarations
- ExteriorFormDeterminant.lean 2 declarations
- ExteriorFormPolynomial.lean 6 declarations
- ExteriorForwardDeterminant.lean 3 declarations
- ExteriorHermitianDisk.lean 3 declarations
- ExteriorImaginaryDegree.lean 2 declarations
- ExteriorImaginaryProjection.lean 6 declarations
- ExteriorLeadingCoefficient.lean 3 declarations
- ExteriorPolynomial.lean 10 declarations
- ExteriorPolynomialDegree.lean 7 declarations
- ExteriorPolynomialInequalities.lean 8 declarations
- ExteriorPositiveEvaluation.lean 3 declarations
- ExteriorQuotientBounds.lean 4 declarations
- ExteriorQuotientDisk.lean 2 declarations
- ExteriorRealProjection.lean 8 declarations
- ExteriorSlowCone.lean 2 declarations
- ForwardConeMonotonicity.lean 3 declarations
- ForwardConeTransport.lean 5 declarations
- ForwardHermitianForm.lean 10 declarations
- ForwardMatching.lean 8 declarations
- FreeExterior.lean 1 declarations
- FreeHighAngularSpectrum.lean 2 declarations
- FreeLimitingModel.lean 1 declarations
- FreeLowAngularSpectrum.lean 6 declarations
- FreeMatching.lean 7 declarations
- FreeOutgoingNonvanishing.lean 1 declarations
- FreeOutgoingSpectrum.lean 3 declarations
- FreePhysicalGeneralizedExclusion.lean 1 declarations
- FreePhysicalSymmetryNoChain.lean 1 declarations
- FreeRadialEquation.lean 6 declarations
- FreeRadialProfile.lean 13 declarations
- FreeRadialRegularity.lean 3 declarations
- FreeRootClassification.lean 3 declarations
- FreeSimpleZeros.lean 2 declarations
- FreeSymmetryNoChain.lean 1 declarations
- FreeSymmetryZeros.lean 5 declarations
- HermitianBoundaryForm.lean 5 declarations
- HighAngularActualFlux.lean 5 declarations
- HighAngularArc.lean 11 declarations
- HighAngularArcFluxSign.lean 3 declarations
- HighAngularBoundaryFlux.lean 3 declarations
- HighAngularCertificate.lean 7 declarations
- HighAngularContour.lean 9 declarations
- HighAngularCorrections.lean 6 declarations
- HighAngularFlux.lean 2 declarations
- HighAngularFluxDerivative.lean 4 declarations
- HighAngularFluxLimit.lean 3 declarations
- HighAngularFluxSign.lean 4 declarations
- HighAngularGeometry.lean 9 declarations
- HighAngularInitialFlux.lean 2 declarations
- HighAngularKineticDerivative.lean 5 declarations
- HighAngularMatching.lean 1 declarations
- HighAngularPathEquation.lean 5 declarations
- HighAngularRay.lean 6 declarations
- HighAngularRayDecay.lean 4 declarations
- HighAngularRayFlux.lean 4 declarations
- HighAngularSquare.lean 1 declarations
- HomotopyCone.lean 6 declarations
- HorizontalCompactification.lean 7 declarations
- HorizontalConeIdentity.lean 4 declarations
- HorizontalContinuity.lean 8 declarations
- HorizontalForwardLink.lean 4 declarations
- HorizontalHomogeneity.lean 5 declarations
- HorizontalMatchingExclusion.lean 8 declarations
- HorizontalUniformPositivity.lean 4 declarations
- IntegerPolynomialDisk.lean 3 declarations
- InteriorDerivativeLipschitz.lean 1 declarations
- KernelOperatorBound.lean 2 declarations
- LaguerreHilbert.lean 9 declarations
- LaguerreIntegral.lean 7 declarations
- LaguerreIteratedSlowGrowth.lean 5 declarations
- LaguerreIteratedSlowJet.lean 6 declarations
- LaguerreOrthogonality.lean 12 declarations
- LaguerrePolynomial.lean 12 declarations
- LaguerreProjection.lean 6 declarations
- LaguerreRapidDecay.lean 3 declarations
- LowWeightInterpolation.lean 1 declarations
- MatchingBasisChange.lean 5 declarations
- MatchingBoundary.lean 4 declarations
- MatchingColumns.lean 5 declarations
- MatchingHomotopy.lean 11 declarations
- MatchingMatrixSimpleZero.lean 4 declarations
- MatchingPolynomialDegree.lean 8 declarations
- MatchingSimpleZero.lean 3 declarations
- MixedFourierLocalization.lean 2 declarations
- NearIdentityInverse.lean 1 declarations
- NormalizedForwardJet.lean 5 declarations
- NormalizedMatchingColumns.lean 8 declarations
- NormalizedTailHolomorphy.lean 9 declarations
- OutgoingHalfPlaneCount.lean 5 declarations
- PolynomialAnalyticMultiplicity.lean 2 declarations
- PolynomialDisk.lean 1 declarations
- PolynomialEnclosure.lean 21 declarations
- PolynomialProjection.lean 7 declarations
- PolynomialRectangleCount.lean 2 declarations
- PolynomialRootEnumeration.lean 5 declarations
- RationalComplexMatrix.lean 24 declarations
- RectangleAnalyticFactorization.lean 5 declarations
- RectangleBoundaryIntegral.lean 2 declarations
- RectangleBoundaryLinear.lean 6 declarations
- RectangleBoundaryPrimitive.lean 4 declarations
- RectangleContourDegree.lean 2 declarations
- RectangleDivisorGeometry.lean 6 declarations
- RectangleFiniteFactor.lean 6 declarations
- RectangleHomotopyCount.lean 1 declarations
- RectangleKernelNonzero.lean 3 declarations
- RectangleLogPrimitive.lean 3 declarations
- RectangleRatioSlit.lean 2 declarations
- RectangleRouche.lean 1 declarations
- RectangleRoucheInput.lean 9 declarations
- RectangleZeroDegree.lean 5 declarations
- RegularizedSlowSolution.lean 7 declarations
- RightMatchingExclusion.lean 5 declarations
- RootDiskApplication.lean 10 declarations
- RootDiskArithmetic.lean 19 declarations
- ScaledLatticeKernel.lean 11 declarations
- SegmentInversePrimitive.lean 1 declarations
- SeparatorArithmetic.lean 21 declarations
- SeparatorPolynomials.lean 11 declarations
- SeparatorScaling.lean 5 declarations
- ShiftedSlowGrowth.lean 8 declarations
- ShiftedSlowSolution.lean 5 declarations
- SimilarityLimit.lean 6 declarations
- TailCone.lean 3 declarations
- UniformCutoffLimit.lean 1 declarations
- UniformHorizontalExclusion.lean 1 declarations
- UniformOutgoingCount.lean 2 declarations
- ZeroTailAnalyticCount.lean 3 declarations
- ZeroTailConjugation.lean 6 declarations
- ZeroTailDeterminantPolynomial.lean 2 declarations
- ZeroTailParameterContinuity.lean 6 declarations
- ZeroTailPolynomialRoots.lean 4 declarations
- ZeroTailRecurrenceLink.lean 11 declarations