OAI/Geometry/SurfaceImmersion/Atlas/LinearPhaseCutoffBounds.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Quantitative transport of the actual supported cutoff to a linear phase chart, including the inverse frequency factor.

  1. def OAI.ClosedSurfaceR4.JetPolynomial.phaseCutoffBudget line 15
  2. lemma OAI.ClosedSurfaceR4.JetPolynomial.phaseCutoffBudget_polynomial line 17
  3. theorem OAI.ClosedSurfaceR4.JetPolynomial.linear_phase_cutoff_bound line 22