OAI/Geometry/SurfaceImmersion/Atlas/ChartedTrialMajorants.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual charted trial mean satisfies the finite-substitution interface, with majorants chosen before the amplitude scale.

  1. theorem OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.PolynomialSolveData.trialMean_majorants line 22