OAI/Geometry/SurfaceImmersion/Correction/FiniteCombinedMean.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Finite adjustment by the actual combined metric and polynomial mean. The threshold is chosen before the short scale and perturbation operator.

  1. theorem OAI.ClosedSurfaceR4.PhaseMean.finite_combined_mean_adjustment line 20