OAI/Geometry/SurfaceImmersion/Correction/PolynomialFrameEnvelope.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A single polynomial envelope for the actual reconstruction coefficients and free normal. Its degree is chosen before any geometric bounds.

  1. lemma OAI.ClosedSurfaceR4.SmallModes.ReconstructionCoefficientBound.mono_const line 16
  2. theorem OAI.ClosedSurfaceR4.RealModes.polynomial_frame_envelope line 31