OAI/Geometry/SurfaceImmersion/Correction/UniformRootMean.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform constants for actual square-root trials are chosen before the scales and the supported perturbation operator.

  1. theorem OAI.ClosedSurfaceR4.RealModes.uniform_perturbed_root_mean_bounds line 17