OAI/Geometry/SmoothYau/Estimates/
465 declarations, 0 contain sorry, 0 declared as axioms; 96 files
Files
- ActualRadialCorrugationStrict.lean 4 declarations
- ActualRadialCorrugationStrictShift.lean 7 declarations
- AnisotropicCompositionSmall.lean 12 declarations
- BasisWordEval.lean 3 declarations
- CanonicalCutoffWave.lean 4 declarations
- CanonicalPhaseTripleSmallBall.lean 4 declarations
- ClmMatrixAlgHom.lean 8 declarations
- CoefficientElliptic.lean 3 declarations
- CoefficientEllipticFlux.lean 1 declarations
- CoefficientPerturbationTendsto.lean 11 declarations
- ComplexGaussianRealValue.lean 15 declarations
- ComplexGramTrace.lean 6 declarations
- ComplexGramTraceSecondMul.lean 3 declarations
- ComplexMul.lean 3 declarations
- ContinuousFamilyEventuallyTest.lean 2 declarations
- CorrugationFirstErrorBound.lean 1 declarations
- CosUnitQuadraticGap.lean 2 declarations
- CoupledPowerCoefficientsNonzero.lean 1 declarations
- CriticalTransversePositive.lean 5 declarations
- CutoffPullbackSobolevBound.lean 1 declarations
- DerivExpSmulZero.lean 6 declarations
- DirectionalLinearComp.lean 4 declarations
- EventualProductScalarCorrectionRate.lean 7 declarations
- EventuallyProductScalarFactorRaw.lean 1 declarations
- EventuallyQuantitativeConformalExactification.lean 2 declarations
- ExistsAnnularSimplePinnedFamily.lean 1 declarations
- ExistsBoxIccSubsetOpen.lean 2 declarations
- ExistsCenteredNormalInverse.lean 1 declarations
- ExistsExhaustibleSignedEnvelope.lean 1 declarations
- ExistsPowerRadius.lean 2 declarations
- ExistsPreparationCovector.lean 1 declarations
- ExistsSphericalScalarProducer.lean 3 declarations
- FiniteGaussianSuperpositionSmallBall.lean 1 declarations
- FiniteRegionsWaveSignExpectation.lean 5 declarations
- FiniteSumTsupportSubset.lean 2 declarations
- FixedRadialChoice.lean 7 declarations
- GeneratedCutoffWaveEndpointRatio.lean 16 declarations
- GeneratedPhaseGaussian.lean 1 declarations
- GridPoint.lean 6 declarations
- LinearProdSurjectiveMinor.lean 2 declarations
- LocalIntegrationPartsC1.lean 1 declarations
- LocalZeroAcrossLevel.lean 6 declarations
- LocalizedPacketSignProbability.lean 11 declarations
- LpInverseGramFstContraction.lean 9 declarations
- MiddleBox.lean 5 declarations
- MixedPiolaDivergenceAbs.lean 3 declarations
- NormPowerVariableWeightControl.lean 2 declarations
- NormalFamilyCanonicalSmallBall.lean 1 declarations
- NormalFamilyInverseExtension.lean 1 declarations
- NormalFamilyPhase.lean 3 declarations
- NormalFamilyWaveLocalizedEstimates.lean 1 declarations
- NormalFamilyWaveZero.lean 2 declarations
- ParamComp.lean 2 declarations
- PartialBilinearExtension.lean 7 declarations
- PathExtension.lean 8 declarations
- PhaseDensityInvBound.lean 2 declarations
- PhaseFormMatrix.lean 33 declarations
- PhysicalFiniteSuperpositionComplete.lean 2 declarations
- PhysicalFiniteSuperpositionCompleteSupported.lean 2 declarations
- PhysicalFiniteSuperpositionSmallBall.lean 1 declarations
- PiolaCancellation.lean 1 declarations
- PolynomialGaussianTailTendsto.lean 4 declarations
- PolynomialWaveUniformResidualBound.lean 2 declarations
- PreconditionedInverse.lean 6 declarations
- PreparationWaveSecondGtOne.lean 6 declarations
- ProductSphereFstContraction.lean 7 declarations
- PullbackLintegral.lean 3 declarations
- QuadraticInnerSpace.lean 8 declarations
- QuarticReparameterization.lean 1 declarations
- RadialLeadingTrace.lean 3 declarations
- RadialPrimitiveSquaredIdentity.lean 2 declarations
- RadialSpeedPositiveAnnulus.lean 14 declarations
- RadialTraceAbsorption.lean 1 declarations
- RadialTransitionPositive.lean 2 declarations
- RealImagCovector.lean 5 declarations
- RealPhaseLinear.lean 21 declarations
- RealValueCubic.lean 20 declarations
- RectangularFactorization.lean 2 declarations
- RescaledCommutatorSobolev.lean 3 declarations
- RescaledDifferentialPerturbation.lean 16 declarations
- RoundPowerConjugateProjectionUniform.lean 1 declarations
- RoundPowerDominatedResidualRapid.lean 1 declarations
- ScalarAffineDetNeZero.lean 3 declarations
- ScalarLogFirst.lean 4 declarations
- ScalarPredPowerWeightBound.lean 3 declarations
- SphereImmersionSpans.lean 1 declarations
- SphericalPinFormNorm.lean 16 declarations
- SphericalWitnessesUnbounded.lean 1 declarations
- TestPairSubSquareBound.lean 6 declarations
- ThreeNoncancelNormedSpace.lean 13 declarations
- TransportCorrection.lean 7 declarations
- UniformDifferenceQuotient.lean 2 declarations
- UniformPhysicalWavesEndpointRatios.lean 1 declarations
- UniformPolynomialSmallBall.lean 4 declarations
- VaryingLaplacianMemRealH.lean 2 imports, no declarations
- VaryingPatchCoefficients.lean 6 declarations