OAI/Geometry/SmoothYau/Spectrum/
467 declarations, 0 contain sorry, 0 declared as axioms; 29 files
Files
- AnisotropicConstant.lean 63 declarations
- AnnularOrthogonalTransverseNonzero.lean 5 declarations
- BilinearCoordinateMatrixPosDef.lean 38 declarations
- BilinearTransverse.lean 13 declarations
- CompactPerturbedEigenvectors.lean 2 declarations
- ContinuousEigenpairLinearization.lean 31 declarations
- ContinuousRealQuadraticCoerciveNear.lean 11 declarations
- CoordinateMetricLaplacianGerm.lean 9 declarations
- FiniteWaveAmplitude.lean 9 declarations
- InverseFrequencyWeightedZero.lean 5 declarations
- JointLocalLaplacian.lean 27 declarations
- NormIteratedFDerivConstMul.lean 22 declarations
- PatchOutput.lean 2 imports, no declarations
- PinnedMetricContinuousSmoothFamily.lean 3 declarations
- PinningFactorGradient.lean 9 declarations
- ProductFrequencyTop.lean 33 declarations
- ProfileFrequencyEnergy.lean 9 declarations
- RealHSmulCommClass.lean 2 imports, no declarations
- ReciprocalIteratedDerivativeBound.lean 8 declarations
- ScalarCompDirectional.lean 34 declarations
- SmoothExtension.lean 14 declarations
- SpectralResolvent.lean 2 declarations
- SphereProjection.lean 40 declarations
- SphericalSimpleEigenpairOpen.lean 2 declarations
- StdGaussianMapInnerUnit.lean 3 declarations
- ThreeCoupledNormedSpace.lean 20 declarations
- TransverseZeroKernel.lean 11 declarations
- UnitSphereProjection.lean 13 declarations
- VaryingSpectralResolventBase.lean 31 declarations