OAI/Geometry/SurfaceImmersion/Correction/PolynomialLocalAmplitude.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Polynomial square-root amplitudes for the actual local metric data.

  1. def OAI.ClosedSurfaceR4.PhaseMean.coefficientBudget line 13
  2. lemma OAI.ClosedSurfaceR4.PhaseMean.coefficientBudget_polynomial line 15
  3. lemma OAI.ClosedSurfaceR4.PhaseMean.inputFactor_le_coefficientBudget line 26
  4. theorem OAI.ClosedSurfaceR4.PhaseMean.polynomial_local_amplitude_bounds line 34