`OAI/MathematicalPhysics/DefocusingNLS/Linear/`

2638 declarations, 0 contain sorry, 0 declared as axioms; 634 files

Files

ContinuousYoung.lean 4 declarations
ExpandingApproximateExistence.lean 4 declarations
ExpandingApproximationCircular.lean 3 declarations
ExpandingApproximationCoefficients.lean 1 declarations
ExpandingApproximationLinear.lean 2 declarations
ExpandingApproximationPower.lean 1 declarations
ExpandingApproximationProduct.lean 1 declarations
ExpandingBallScalar.lean 2 declarations
ExpandingBielecki.lean 7 declarations
ExpandingBlowupClock.lean 7 declarations
ExpandingBlowupObservation.lean 5 declarations
ExpandingBlowupTransfer.lean 3 declarations
ExpandingCircularMoment.lean 2 declarations
ExpandingCoefficientCompactness.lean 3 declarations
ExpandingCommutatorCoefficient.lean 5 declarations
ExpandingCompactCommutator.lean 1 declarations
ExpandingCompactDerivativeLimit.lean 1 declarations
ExpandingCompactEnergyError.lean 2 declarations
ExpandingCompactFilterLimit.lean 1 declarations
ExpandingCompactLowCommutator.lean 1 declarations
ExpandingCompactLowProduct.lean 1 declarations
ExpandingCompactMassLimit.lean 1 declarations
ExpandingCompactPhysicalLimit.lean 1 declarations
ExpandingCompactProductLimit.lean 1 declarations
ExpandingCompactWeightIntegral.lean 1 declarations
ExpandingCompactWeightLimit.lean 1 declarations
ExpandingContinuousRealization.lean 3 declarations
ExpandingContinuousStep.lean 1 declarations
ExpandingConvolution.lean 12 declarations
ExpandingCoordinateMap.lean 3 declarations
ExpandingCoordinateSequence.lean 1 declarations
ExpandingDecayingDuhamel.lean 2 declarations
ExpandingDerivativeBounds.lean 4 declarations
ExpandingDerivativeWeight.lean 2 declarations
ExpandingDualForcingBound.lean 3 declarations
ExpandingDuhamel.lean 10 declarations
ExpandingDuhamelContinuity.lean 9 declarations
ExpandingDuhamelDuality.lean 3 declarations
ExpandingDuhamelFamily.lean 8 declarations
ExpandingDuhamelLinear.lean 3 declarations
ExpandingDuhamelRestart.lean 5 declarations
ExpandingEnergyComponents.lean 10 declarations
ExpandingEnergyInner.lean 3 declarations
ExpandingEnergyObservation.lean 1 declarations
ExpandingEnergyScaling.lean 8 declarations
ExpandingEscapedEnergy.lean 1 declarations
ExpandingEvaluation.lean 5 declarations
ExpandingFilteredDerivatives.lean 7 declarations
ExpandingFilteredLimit.lean 5 declarations
ExpandingFilteredPhysicalEnergy.lean 3 declarations
ExpandingFilteredWeakLimit.lean 3 declarations
ExpandingFilteredWeightedLimit.lean 1 declarations
ExpandingFiniteLocalExistence.lean 1 declarations
ExpandingFiniteSlab.lean 4 declarations
ExpandingFixedPhysical.lean 1 declarations
ExpandingFourier.lean 11 declarations
ExpandingFourierJetBound.lean 4 declarations
ExpandingFourierMomentBound.lean 2 declarations
ExpandingFourierTest.lean 4 declarations
ExpandingFourierTestLimit.lean 2 declarations
ExpandingFreeContinuity.lean 8 declarations
ExpandingFreeDuality.lean 2 declarations
ExpandingFreeInverse.lean 6 declarations
ExpandingFreeStep.lean 18 declarations
ExpandingFrequencyCutoff.lean 7 declarations
ExpandingGeneralFilterLimit.lean 2 declarations
ExpandingGlobalTrajectory.lean 6 declarations
ExpandingIdentifiedCompactness.lean 1 declarations
ExpandingInitialData.lean 5 declarations
ExpandingInteractionPicture.lean 3 declarations
ExpandingInversePath.lean 5 declarations
ExpandingLimitRealization.lean 1 declarations
ExpandingLinearization.lean 3 declarations
ExpandingLinearizedPhysicalLimit.lean 2 declarations
ExpandingLocalConvergence.lean 3 declarations
ExpandingLocalDependence.lean 2 declarations
ExpandingLocalizationBound.lean 3 declarations
ExpandingLocalizationEnergy.lean 1 declarations
ExpandingLocalizedWeakLimit.lean 2 declarations
ExpandingLowInterpolation.lean 1 declarations
ExpandingLowMassLimit.lean 2 declarations
ExpandingLowPhysicalEnergy.lean 3 declarations
ExpandingLowerWeightBound.lean 2 declarations
ExpandingMassDerivativeEnergy.lean 3 declarations
ExpandingMassDerivativeNorm.lean 2 declarations
ExpandingMildContraction.lean 9 declarations
ExpandingMildEnergy.lean 2 declarations
ExpandingMildEnergyBalance.lean 3 declarations
ExpandingMildLimit.lean 1 declarations
ExpandingMildStrong.lean 1 declarations
ExpandingModeConverse.lean 3 declarations
ExpandingModeDuhamel.lean 8 declarations
ExpandingModeEquation.lean 8 declarations
ExpandingMomentCommutator.lean 2 declarations
ExpandingMultiplication.lean 11 declarations
ExpandingNearbyTransfer.lean 4 declarations
ExpandingNonlinearStepError.lean 2 declarations
ExpandingNonlinearStrong.lean 2 declarations
ExpandingNonlinearity.lean 11 declarations
ExpandingNonlinearityTransport.lean 9 declarations
ExpandingNonprincipalEnergy.lean 4 declarations
ExpandingNonprincipalObservation.lean 1 declarations
ExpandingObservedFamily.lean 1 declarations
ExpandingOddCommutator.lean 2 declarations
ExpandingOddCommutatorBound.lean 5 declarations
ExpandingOddCompactness.lean 3 declarations
ExpandingOneDimensional.lean 5 declarations
ExpandingOrderedCommutator.lean 5 declarations
ExpandingOrderedConjugate.lean 3 declarations
ExpandingOrderedEnergy.lean 7 declarations
ExpandingOrderedPhysicalSymbol.lean 3 declarations
ExpandingOrderedSymbol.lean 5 declarations
ExpandingPerturbationContinuity.lean 3 declarations
ExpandingPerturbationEquation.lean 2 declarations
ExpandingPerturbationExistence.lean 3 declarations
ExpandingPerturbationReaction.lean 6 declarations
ExpandingPhysicalAmplitude.lean 5 declarations
ExpandingPhysicalCharacter.lean 3 declarations
ExpandingPhysicalClock.lean 7 declarations
ExpandingPhysicalDerivativeBound.lean 1 declarations
ExpandingPhysicalEquation.lean 3 declarations
ExpandingPhysicalFourier.lean 6 declarations
ExpandingPhysicalLocalization.lean 5 declarations
ExpandingPhysicalModeRate.lean 2 declarations
ExpandingPhysicalPath.lean 3 declarations
ExpandingPhysicalPolynomial.lean 3 declarations
ExpandingPhysicalSpaceBound.lean 2 declarations
ExpandingPhysicalTermDerivative.lean 1 declarations
ExpandingPhysicalTimeBound.lean 2 declarations
ExpandingPhysicalTrajectory.lean 9 declarations
ExpandingPicardContinuity.lean 8 declarations
ExpandingPolynomial.lean 9 declarations
ExpandingPolynomialLimit.lean 1 declarations
ExpandingPolynomialMoment.lean 5 declarations
ExpandingPolynomialTimeBound.lean 1 declarations
ExpandingPositivePower.lean 4 declarations
ExpandingPotentialContinuity.lean 5 declarations
ExpandingProductCommutator.lean 3 declarations
ExpandingProductCommutatorBound.lean 3 declarations
ExpandingProductCommutatorLinear.lean 1 declarations
ExpandingProductDerivativeFormula.lean 1 declarations
ExpandingProductDifference.lean 1 declarations
ExpandingProductSmoothRemainder.lean 1 declarations
ExpandingProfileCompactness.lean 1 declarations
ExpandingProfileContinuity.lean 3 declarations
ExpandingProfileDifference.lean 3 declarations
ExpandingProfileEnergy.lean 1 declarations
ExpandingProfileEnergyDerivative.lean 1 declarations
ExpandingProfileEquation.lean 1 declarations
ExpandingProfileInitial.lean 1 declarations
ExpandingProfileLimitEquation.lean 2 declarations
ExpandingProfileObservation.lean 1 declarations
ExpandingProfileOperator.lean 4 declarations
ExpandingProfilePhysicalEquation.lean 1 declarations
ExpandingProfilePhysicalPath.lean 1 declarations
ExpandingProfilePointwise.lean 1 declarations
ExpandingProfilePropagator.lean 10 declarations
ExpandingProfileResponse.lean 2 declarations
ExpandingProfileTimeEquicontinuity.lean 1 declarations
ExpandingProfileUniformBound.lean 1 declarations
ExpandingQuadraticMultiplier.lean 5 declarations
ExpandingQuadraticObservation.lean 1 declarations
ExpandingQuadraticWeight.lean 1 declarations
ExpandingReducedTransfer.lean 1 declarations
ExpandingResidualStability.lean 6 declarations
ExpandingSampleDerivativeFormula.lean 1 declarations
ExpandingScaleTransfer.lean 15 declarations
ExpandingSequentialObservation.lean 1 declarations
ExpandingSlabMild.lean 7 declarations
ExpandingSlabTrajectory.lean 2 declarations
ExpandingSmoothCutoff.lean 8 declarations
ExpandingSmoothFilter.lean 7 declarations
ExpandingSobolevComparison.lean 5 declarations
ExpandingSobolevEquiv.lean 17 declarations
ExpandingSobolevNonlinearity.lean 7 declarations
ExpandingSobolevStrong.lean 2 declarations
ExpandingSobolevWeights.lean 12 declarations
ExpandingSolutionContinuity.lean 3 declarations
ExpandingSpacetimeObservation.lean 4 declarations
ExpandingStableLimitEnergy.lean 1 declarations
ExpandingStableSequence.lean 1 declarations
ExpandingStepExistence.lean 1 declarations
ExpandingStepLipschitz.lean 1 declarations
ExpandingStepMap.lean 2 declarations
ExpandingStepMapContinuity.lean 1 declarations
ExpandingStrongEquation.lean 3 declarations
ExpandingTaylorRemainder.lean 5 declarations
ExpandingTorus.lean 7 declarations
ExpandingTransferContinuity.lean 2 declarations
ExpandingWeakInitialBound.lean 1 declarations
ExpandingWeakLimitPath.lean 1 declarations
ExpandingWeightAddition.lean 6 declarations
ExpandingWeightContinuity.lean 5 declarations
ExpandingWeightIdentification.lean 9 declarations
ExpandingWeightProduct.lean 6 declarations
ExpandingWeightedDuhamel.lean 2 declarations
ExpandingWeightedLocal.lean 3 declarations
FourierAbsolute.lean 5 declarations
FourierBoundedMultiplier.lean 6 declarations
FourierConvolution.lean 9 declarations
FourierCoordinateDerivative.lean 1 declarations
HarmonicRadialLinearCombination.lean 3 declarations
HarmonicRadialNonvanishing.lean 5 declarations
HomogeneousAngularDimension.lean 1 declarations
HomogeneousAngularL2.lean 4 declarations
HomogeneousAngularProjection.lean 6 declarations
HomogeneousAngularUpper.lean 1 declarations
HomogeneousAnnulusBounds.lean 8 declarations
HomogeneousAnnulusScaling.lean 5 declarations
HomogeneousCZero.lean 8 declarations
HomogeneousCanonicalContour.lean 2 declarations
HomogeneousCanonicalLogEstimates.lean 1 declarations
HomogeneousCircleIdentity.lean 2 declarations
HomogeneousCircleProjection.lean 7 declarations
HomogeneousClassicalGenerator.lean 5 declarations
HomogeneousClassicalGreen.lean 5 declarations
HomogeneousClassicalLinearization.lean 2 declarations
HomogeneousCommutatorBound.lean 7 declarations
HomogeneousCommutatorCompact.lean 3 declarations
HomogeneousCommutatorCompletion.lean 3 declarations
HomogeneousCommutatorDecay.lean 2 declarations
HomogeneousCommutatorFourier.lean 2 declarations
HomogeneousCommutatorPotential.lean 1 declarations
HomogeneousCommutatorRows.lean 11 declarations
HomogeneousCommutatorSplit.lean 4 declarations
HomogeneousCommutatorSymbol.lean 4 declarations
HomogeneousCompactErrors.lean 3 declarations
HomogeneousCompactLocalEstimate.lean 1 declarations
HomogeneousCompactObservation.lean 4 declarations
HomogeneousCompactResolvent.lean 2 declarations
HomogeneousComplexCoordinates.lean 11 declarations
HomogeneousComplexDecomposition.lean 1 declarations
HomogeneousComplexFiniteRank.lean 1 declarations
HomogeneousComplexIndependence.lean 3 declarations
HomogeneousComplexPotential.lean 4 declarations
HomogeneousComplexSemigroup.lean 4 declarations
HomogeneousComplexStrongContinuity.lean 1 declarations
HomogeneousComplexification.lean 12 declarations
HomogeneousConjugation.lean 12 declarations
HomogeneousContourDecomposition.lean 2 declarations
HomogeneousContourDomain.lean 2 declarations
HomogeneousContourEigenfunction.lean 3 declarations
HomogeneousContourGenerator.lean 2 declarations
HomogeneousConvolutionBound.lean 4 declarations
HomogeneousConvolutionWeights.lean 8 declarations
HomogeneousDefectComparison.lean 2 declarations
HomogeneousDefectEnergy.lean 19 declarations
HomogeneousDefectExclusion.lean 1 declarations
HomogeneousDerivativeBounds.lean 4 declarations
HomogeneousDerivativeConjugation.lean 6 declarations
HomogeneousDerivativeEnergy.lean 2 declarations
HomogeneousDerivativeTesting.lean 6 declarations
HomogeneousDiagonalCoordinates.lean 1 declarations
HomogeneousDilation.lean 9 declarations
HomogeneousDilationContinuity.lean 5 declarations
HomogeneousDilationDerivative.lean 5 declarations
HomogeneousDoubleCircle.lean 1 declarations
HomogeneousDuhamel.lean 7 declarations
HomogeneousDuhamelDerivative.lean 2 declarations
HomogeneousDuhamelDuality.lean 1 declarations
HomogeneousDuhamelRestart.lean 5 declarations
HomogeneousDyadicPartition.lean 15 declarations
HomogeneousDyadicSeries.lean 6 declarations
HomogeneousEigenfunctionPDE.lean 5 declarations
HomogeneousEnergyComponents.lean 18 declarations
HomogeneousEnergyGenerator.lean 1 declarations
HomogeneousEnergyInterpolation.lean 4 declarations
HomogeneousEnergyObservation.lean 1 declarations
HomogeneousEssentialContraction.lean 1 declarations
HomogeneousEulerBounds.lean 6 declarations
HomogeneousEulerPhysical.lean 2 declarations
HomogeneousEulerRecurrence.lean 5 declarations
HomogeneousEvaluationContinuity.lean 1 declarations
HomogeneousFastTail.lean 3 declarations
HomogeneousFiniteCodimension.lean 1 declarations
HomogeneousFiniteRankAnalytic.lean 4 declarations
HomogeneousFiniteRankCriterion.lean 3 declarations
HomogeneousFiniteRankDiscrete.lean 5 declarations
HomogeneousFiniteRankEigen.lean 3 declarations
HomogeneousFiniteRankFactor.lean 7 declarations
HomogeneousFiniteRankLimit.lean 2 declarations
HomogeneousFiniteRankResolvent.lean 3 declarations
HomogeneousFiniteRankStep.lean 3 declarations
HomogeneousFiniteSemigroup.lean 5 declarations
HomogeneousFixedRadialModes.lean 2 declarations
HomogeneousFourierL1.lean 1 declarations
HomogeneousFourierMeasure.lean 9 declarations
HomogeneousFourierPairing.lean 5 declarations
HomogeneousFourierProduct.lean 4 declarations
HomogeneousFourierTestExt.lean 1 declarations
HomogeneousFreeContinuity.lean 9 declarations
HomogeneousFreeDomain.lean 3 declarations
HomogeneousFreeDuality.lean 4 declarations
HomogeneousFreeEnergy.lean 7 declarations
HomogeneousFreeFourier.lean 11 declarations
HomogeneousFreeGroup.lean 9 declarations
HomogeneousFreeJointContinuity.lean 1 declarations
HomogeneousFreeOperator.lean 11 declarations
HomogeneousFreePhysical.lean 9 declarations
HomogeneousFreeTestBounds.lean 6 declarations
HomogeneousFreeTestDerivative.lean 1 declarations
HomogeneousFrequencySplit.lean 12 declarations
HomogeneousGaugeAngular.lean 5 declarations
HomogeneousGaugeDecay.lean 2 declarations
HomogeneousGeneratorCoordinates.lean 3 declarations
HomogeneousGeneratorEigenvector.lean 3 declarations
HomogeneousGeneratorPerturbation.lean 5 declarations
HomogeneousGluedAverage.lean 2 declarations
HomogeneousGluedCanonicalTail.lean 2 declarations
HomogeneousGluedCutoff.lean 6 declarations
HomogeneousGluedEigenpair.lean 2 declarations
HomogeneousGluedLocalL2.lean 2 declarations
HomogeneousGluedMatchingMode.lean 1 declarations
HomogeneousGluedMode.lean 1 declarations
HomogeneousGluedOrigin.lean 3 declarations
HomogeneousGluedOriginBasis.lean 1 declarations
HomogeneousGluedOriginRegularity.lean 1 declarations
HomogeneousGluedRegularity.lean 3 declarations
HomogeneousGluedTail.lean 2 declarations
HomogeneousHamiltonian.lean 9 declarations
HomogeneousHarmonicAnnularTesting.lean 1 declarations
HomogeneousHarmonicBounded.lean 2 declarations
HomogeneousHarmonicChannels.lean 2 declarations
HomogeneousHarmonicCompleteness.lean 4 declarations
HomogeneousHarmonicDecomposition.lean 2 declarations
HomogeneousHarmonicEigenL2.lean 1 declarations
HomogeneousHarmonicEigenmode.lean 2 declarations
HomogeneousHarmonicFunctional.lean 3 declarations
HomogeneousHarmonicLowerEnergy.lean 1 declarations
HomogeneousHarmonicPairEnergy.lean 2 declarations
HomogeneousHarmonicRadialEquation.lean 6 declarations
HomogeneousHarmonicSeparation.lean 1 declarations
HomogeneousHarmonicSmoothness.lean 4 declarations
HomogeneousHarmonicTestCalculus.lean 6 declarations
HomogeneousHarmonicTestSupport.lean 5 declarations
HomogeneousHarmonicTrace.lean 1 declarations
HomogeneousHarmonicTransport.lean 10 declarations
HomogeneousHarmonicWeakLaplacian.lean 3 declarations
HomogeneousInhomogeneousChannels.lean 5 declarations
HomogeneousInteractionPicture.lean 6 declarations
HomogeneousInvariantSemigroup.lean 5 declarations
HomogeneousInverseWeight.lean 2 declarations
HomogeneousJordanChannels.lean 2 declarations
HomogeneousL2Product.lean 7 declarations
HomogeneousLaplacianDomain.lean 3 declarations
HomogeneousLaplacianFrequency.lean 1 declarations
HomogeneousLinearization.lean 5 declarations
HomogeneousLinearizedBound.lean 3 declarations
HomogeneousLinearizedCommutator.lean 3 declarations
HomogeneousLinearizedCompact.lean 4 declarations
HomogeneousLinearizedDomain.lean 2 declarations
HomogeneousLinearizedEnergy.lean 1 declarations
HomogeneousLinearizedFlow.lean 14 declarations
HomogeneousLinearizedRestart.lean 3 declarations
HomogeneousLinearizedSemigroup.lean 6 declarations
HomogeneousLocalL2.lean 5 declarations
HomogeneousLocalL2Energy.lean 2 declarations
HomogeneousLocalRadialTesting.lean 4 declarations
HomogeneousLocalizationContinuity.lean 3 declarations
HomogeneousLocalizationPhysical.lean 2 declarations
HomogeneousLogCoefficients.lean 10 declarations
HomogeneousLogEquation.lean 4 declarations
HomogeneousLogJetBound.lean 11 declarations
HomogeneousLogJetOperations.lean 6 declarations
HomogeneousLowCompact.lean 2 declarations
HomogeneousLowerOrder.lean 3 declarations
HomogeneousMatchedBoundedPair.lean 1 declarations
HomogeneousMatchedComplexDecomposition.lean 1 declarations
HomogeneousMatchedContour.lean 1 declarations
HomogeneousMatchedGenerator.lean 1 declarations
HomogeneousMatchedHarmonic.lean 1 declarations
HomogeneousMatchedJordanMode.lean 1 declarations
HomogeneousMatchedObservation.lean 1 declarations
HomogeneousMatchedOutgoing.lean 2 declarations
HomogeneousMatchedPotential.lean 1 declarations
HomogeneousMatchedPrincipal.lean 1 declarations
HomogeneousMatchedQuotient.lean 3 declarations
HomogeneousMatchedRadial.lean 1 declarations
HomogeneousMatchedRadialC2.lean 1 declarations
HomogeneousMatchedSpectralStability.lean 1 declarations
HomogeneousMeasurableDuhamel.lean 3 declarations
HomogeneousMeasurableMildContinuity.lean 3 declarations
HomogeneousMildEnergy.lean 3 declarations
HomogeneousNonlinearity.lean 6 declarations
HomogeneousObservationSeparates.lean 2 declarations
HomogeneousOrderedDerivatives.lean 6 declarations
HomogeneousOutgoingComparison.lean 3 declarations
HomogeneousOutgoingDefectEquation.lean 4 declarations
HomogeneousOutgoingDefectZero.lean 1 declarations
HomogeneousOutgoingDerivatives.lean 2 declarations
HomogeneousOutgoingEstimates.lean 6 declarations
HomogeneousOutgoingLogJets.lean 6 declarations
HomogeneousOutgoingMatrix.lean 15 declarations
HomogeneousOutgoingPropagation.lean 4 declarations
HomogeneousOutgoingRadialRows.lean 3 declarations
HomogeneousOutgoingRobin.lean 5 declarations
HomogeneousOutgoingSelection.lean 1 declarations
HomogeneousOutgoingTail.lean 6 declarations
HomogeneousPhysicalC2.lean 3 declarations
HomogeneousPhysicalColumnJets.lean 6 declarations
HomogeneousPhysicalCoordinates.lean 1 declarations
HomogeneousPhysicalDerivative.lean 6 declarations
HomogeneousPhysicalDifferentiation.lean 2 declarations
HomogeneousPhysicalDuality.lean 1 declarations
HomogeneousPhysicalEigenvector.lean 1 declarations
HomogeneousPhysicalFourierJets.lean 3 declarations
HomogeneousPhysicalFrame.lean 4 declarations
HomogeneousPhysicalFreeKernel.lean 2 declarations
HomogeneousPhysicalGeneratorIntegral.lean 4 declarations
HomogeneousPhysicalInjective.lean 5 declarations
HomogeneousPhysicalIntegrable.lean 2 declarations
HomogeneousPhysicalKernelDerivative.lean 6 declarations
HomogeneousPhysicalLaplacian.lean 3 declarations
HomogeneousPhysicalLift.lean 1 declarations
HomogeneousPhysicalMap.lean 8 declarations
HomogeneousPhysicalMeasurable.lean 1 declarations
HomogeneousPhysicalRealSpan.lean 4 declarations
HomogeneousPhysicalSpan.lean 2 declarations
HomogeneousPhysicalWeakLimit.lean 3 declarations
HomogeneousPolarL2.lean 13 declarations
HomogeneousPolarTesting.lean 7 declarations
HomogeneousPolynomialCalculus.lean 11 declarations
HomogeneousPolynomialHarmonic.lean 7 declarations
HomogeneousPolynomialLaplacian.lean 15 declarations
HomogeneousPolynomialMoment.lean 3 declarations
HomogeneousPotentialEnergy.lean 2 declarations
HomogeneousPotentialPicard.lean 8 declarations
HomogeneousPrincipalCommutator.lean 3 declarations
HomogeneousPrincipalPotential.lean 10 declarations
HomogeneousProductCompact.lean 1 declarations
HomogeneousProfileDerivative.lean 3 declarations
HomogeneousProfileSymmetries.lean 3 declarations
HomogeneousQuotientDecay.lean 6 declarations
HomogeneousRadialCompletion.lean 6 declarations
HomogeneousRadialComplexTesting.lean 1 declarations
HomogeneousRadialDefect.lean 8 declarations
HomogeneousRadialIdentification.lean 5 declarations
HomogeneousRadialL2.lean 7 declarations
HomogeneousRadialLaplacianGreen.lean 5 declarations
HomogeneousRadialMeasure.lean 8 declarations
HomogeneousRadialPairL2.lean 4 declarations
HomogeneousRadialPowerCalculus.lean 7 declarations
HomogeneousRadialRiccati.lean 5 declarations
HomogeneousRadialSchwartz.lean 1 declarations
HomogeneousRadialSmoothL2.lean 3 declarations
HomogeneousRadialSquareTest.lean 9 declarations
HomogeneousRadialTestPairing.lean 9 declarations
HomogeneousRadialTesting.lean 4 declarations
HomogeneousRadialWeakTesting.lean 4 declarations
HomogeneousRealCoordinateEvolution.lean 3 declarations
HomogeneousRealPhysicalContour.lean 1 declarations
HomogeneousRealStableCoordinates.lean 9 declarations
HomogeneousRegularBasis.lean 2 declarations
HomogeneousRegularCompleteness.lean 3 declarations
HomogeneousRegularComplexEnergy.lean 2 declarations
HomogeneousRegularCoupling.lean 2 declarations
HomogeneousRegularEnergy.lean 2 declarations
HomogeneousRegularMode.lean 3 declarations
HomogeneousRegularPhysical.lean 3 declarations
HomogeneousRegularPrimitive.lean 6 declarations
HomogeneousRegularSmallBall.lean 1 declarations
HomogeneousRegularStateZero.lean 1 declarations
HomogeneousRegularZero.lean 1 declarations
HomogeneousResolventCircle.lean 13 declarations
HomogeneousResolventMoments.lean 8 declarations
HomogeneousSchrodingerContinuity.lean 2 declarations
HomogeneousSchrodingerDerivative.lean 3 declarations
HomogeneousSchrodingerMultiplier.lean 13 declarations
HomogeneousSchwartzCommutator.lean 3 declarations
HomogeneousSchwartzConvolution.lean 4 declarations
HomogeneousSchwartzFrame.lean 2 declarations
HomogeneousSchwartzObservation.lean 3 declarations
HomogeneousSecondMomentWeight.lean 2 declarations
HomogeneousSemigroupContour.lean 1 declarations
HomogeneousSemigroupDecay.lean 3 declarations
HomogeneousSpecifiedRadialMode.lean 1 declarations
HomogeneousSpectralGrowth.lean 9 declarations
HomogeneousSpectralGrowthEquation.lean 15 declarations
HomogeneousSpectralInterpolation.lean 2 declarations
HomogeneousSpectralLocalizationBarrier.lean 2 declarations
HomogeneousSpectralLocalizationEquation.lean 4 declarations
HomogeneousSpectralLocalizationGauge.lean 9 declarations
HomogeneousSpectralLocalizationGeometry.lean 4 declarations
HomogeneousSpectralLocalizationPotential.lean 3 declarations
HomogeneousSpectralLocalizationRemote.lean 10 declarations
HomogeneousSpectralLocalizationSubunit.lean 10 declarations
HomogeneousSpectralLocalizationWKB.lean 6 declarations
HomogeneousSpectralPower.lean 2 declarations
HomogeneousSphereHarmonicSpan.lean 8 declarations
HomogeneousSpherePolynomial.lean 9 declarations
HomogeneousSymbolBound.lean 2 declarations
HomogeneousSymbolMembership.lean 3 declarations
HomogeneousSymmetryDimension.lean 1 declarations
HomogeneousSymmetryEvolution.lean 4 declarations
HomogeneousSymmetryGenerator.lean 2 declarations
HomogeneousSymmetryIndependence.lean 3 declarations
HomogeneousSymmetryProjection.lean 2 declarations
HomogeneousTaylorRemainder.lean 6 declarations
HomogeneousTimeObservation.lean 1 declarations
HomogeneousTimeOneDecomposition.lean 3 declarations
HomogeneousTopCommutator.lean 5 declarations
HomogeneousTranslation.lean 10 declarations
HomogeneousWeakGenerator.lean 2 declarations
HomogeneousWeakMildIdentification.lean 1 declarations
HomogeneousWeakNorm.lean 1 declarations
HomogeneousWeakObservation.lean 3 declarations
HomogeneousWeakSubsequence.lean 1 declarations
HomogeneousWeightedDuhamel.lean 2 declarations
HomogeneousWeightedObservation.lean 8 declarations
HomogeneousYConvolution.lean 9 declarations
HomogeneousYLocalization.lean 11 declarations
HomogeneousYNorm.lean 3 declarations
HomogeneousYProduct.lean 5 declarations
HomogeneousYSpace.lean 9 declarations
LatticeMomentAlgebra.lean 6 declarations
LocalizationFatou.lean 1 declarations
LocalizationFourierEnergy.lean 6 declarations
LocalizationWeightComparison.lean 3 declarations
ObservationDecay.lean 6 declarations
PeriodicSchwartzPairing.lean 2 declarations
SchrodingerFlow.lean 12 declarations
SchrodingerForcedDuhamel.lean 7 declarations
SchrodingerGenerator.lean 12 declarations
SchrodingerInteraction.lean 6 declarations
SchrodingerNonlinearEquation.lean 6 declarations
SchrodingerTorus.lean 11 declarations
SchwartzAnnulusSampling.lean 5 declarations
SchwartzCommutatorSampling.lean 2 declarations
SchwartzCompactContinuity.lean 5 declarations
SchwartzCoreSampling.lean 2 declarations
SchwartzCutoffAnnulusSampling.lean 3 declarations
SchwartzCutoffDerivative.lean 3 declarations
SchwartzDilationJets.lean 3 declarations
SchwartzDyadicCutoff.lean 9 declarations
SchwartzFourierConvolution.lean 4 declarations
SchwartzFourierPolynomial.lean 5 declarations
SchwartzFrequencyCutoff.lean 8 declarations
SchwartzLatticeSampling.lean 3 declarations
SchwartzLocalConvolution.lean 10 declarations
SchwartzLocalizationKernel.lean 5 declarations
SchwartzLocalizationLimit.lean 2 declarations
SchwartzNonlinearPeriodization.lean 4 declarations
SchwartzNormSquare.lean 4 declarations
SchwartzOuterAnnulusSampling.lean 5 declarations
SchwartzPairingLimit.lean 1 declarations
SchwartzPartialDerivative.lean 4 declarations
SchwartzPartialKernel.lean 6 declarations
SchwartzPeriodization.lean 4 declarations
SchwartzPeriodizationFunction.lean 16 declarations
SchwartzPeriodizationIntegral.lean 8 declarations
SchwartzPeriodizationLimit.lean 1 declarations
SchwartzPeriodizationWeighted.lean 1 declarations
SchwartzPhysicalSampling.lean 9 declarations
SchwartzPoissonSummation.lean 8 declarations
SchwartzPolynomialMoment.lean 2 declarations
SchwartzProductSampling.lean 4 declarations
SchwartzProfileSampling.lean 2 declarations
SchwartzSampleContinuity.lean 2 declarations
SchwartzSampleDerivativeBound.lean 2 declarations
SchwartzSampleLipschitz.lean 2 declarations
SchwartzSampleTranslation.lean 3 declarations
SchwartzSampledNonlinearity.lean 6 declarations
SchwartzSamplingBound.lean 3 declarations
SchwartzSamplingContinuity.lean 4 declarations
SchwartzSamplingDilation.lean 3 declarations
SchwartzSamplingJetBound.lean 4 declarations
SchwartzSamplingLocalBound.lean 3 declarations
SchwartzSamplingSum.lean 6 declarations
SchwartzScaledCutoff.lean 5 declarations
SchwartzSeparatedPeriodization.lean 3 declarations
SchwartzSobolevLocalization.lean 3 declarations
SchwartzTorusSampling.lean 9 declarations
SemigroupGeneratorEigenvector.lean 1 declarations
SemigroupStableBlocks.lean 3 declarations
SemigroupSymmetryFrame.lean 2 declarations
SobolevAmplitude.lean 2 declarations
SobolevCompactStability.lean 2 declarations
SobolevConjugation.lean 10 declarations
SobolevContinuation.lean 5 declarations
SobolevContinuousDependence.lean 2 declarations
SobolevConvolution.lean 14 declarations
SobolevDuhamel.lean 3 declarations
SobolevDuhamelIntegral.lean 6 declarations
SobolevEmbedding.lean 8 declarations
SobolevEvaluationContinuity.lean 1 declarations
SobolevFlowNeighborhood.lean 3 declarations
SobolevForcedEvaluation.lean 3 declarations
SobolevForwardDomain.lean 3 declarations
SobolevForwardDuhamel.lean 3 declarations
SobolevForwardMaximal.lean 1 declarations
SobolevIntervalUniqueness.lean 2 declarations
SobolevLinearization.lean 3 declarations
SobolevLocalContinuousFlow.lean 3 declarations
SobolevLocalFlow.lean 1 declarations
SobolevMultiplication.lean 17 declarations
SobolevNonlinearity.lean 7 declarations
SobolevPhase.lean 7 declarations
SobolevPolynomialBounds.lean 2 declarations
SobolevProductWeights.lean 3 declarations
SobolevResidualStability.lean 2 declarations
SobolevRestartExtension.lean 2 declarations
SobolevSecondDerivativeBounds.lean 4 declarations
SobolevSymmetryFlow.lean 9 declarations
SobolevTaylorRemainder.lean 5 declarations
SobolevTimeTranslation.lean 4 declarations
SobolevTorus.lean 19 declarations
SobolevTranslation.lean 7 declarations
SobolevTranslationEquation.lean 8 declarations
SobolevUniqueness.lean 1 declarations
SobolevWeights.lean 5 declarations
SpacetimeBallObservation.lean 5 declarations
SpacetimeObservationIntegral.lean 1 declarations
SpacetimeStableObservation.lean 2 declarations
TorusCircularPotential.lean 1 declarations
TorusCompactWeightIntegral.lean 1 declarations
TorusConjugation.lean 4 declarations
TorusDerivatives.lean 22 declarations
TorusDiscreteLinearData.lean 1 declarations
TorusDiscreteRadius.lean 4 declarations
TorusFourierIsometry.lean 5 declarations
TorusFourierProduct.lean 2 declarations
TorusFourierTranslation.lean 3 declarations
TorusFrameNormalization.lean 2 declarations
TorusL2Coefficient.lean 2 declarations
TorusL2Product.lean 8 declarations
TorusLinearStep.lean 2 declarations
TorusLinearStepAssembly.lean 4 declarations
TorusOddCommutator.lean 2 declarations
TorusOrderedEnergy.lean 5 declarations
TorusPhysicalL2.lean 3 declarations
TorusPrincipalPotential.lean 8 declarations
TorusProductCommutator.lean 2 declarations
TorusStableBlocks.lean 4 declarations
WeakLinearCoordinates.lean 2 declarations