OAI/Geometry/SurfaceImmersion/Correction/PolynomialFreeModes.lean
1 declarations, 0 contain sorry, 0 declared as axioms
Free normal amplitudes for the actual polynomially perturbed metric operator.
- theorem
OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.polynomial_free_mode_boundsline 16