OAI/Geometry/SurfaceImmersion/Correction/CorrectedPolynomialRootMean.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The polynomial mean on actual cutoff square-root trial amplitudes. Its constants are uniform before choosing the oscillation scales.

  1. theorem OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.correctedPolynomialRootMean_bounds line 18