OAI/Geometry/SurfaceImmersion/Correction/CorrectedPolynomialMean.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The polynomial quadratic mean for the actual corrected geometric seeds. All constants are chosen before the oscillation and amplitude scales.

  1. theorem OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.correctedPolynomialMean_bounds line 17