OAI/Geometry/SurfaceImmersion/Correction/PositivePolynomialBounds.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The explicit normal-frame budgets have fixed polynomial growth. This keeps their exponents independent of multiplicative input constants.

  1. def OAI.ClosedSurfaceR4.RealModes.HasPolynomialBound line 12

    Source documentation

    An explicit polynomial upper bound on the positive half-line.

    def HasPolynomialBound (f : ℝ → ℝ) : Prop :=
…
  2. lemma OAI.ClosedSurfaceR4.RealModes.polynomialBound_const line 15
  3. lemma OAI.ClosedSurfaceR4.RealModes.polynomialBound_id line 20
  4. lemma OAI.ClosedSurfaceR4.RealModes.HasPolynomialBound.add line 23
  5. lemma OAI.ClosedSurfaceR4.RealModes.HasPolynomialBound.mul line 39
  6. lemma OAI.ClosedSurfaceR4.RealModes.HasPolynomialBound.pow line 54
  7. lemma OAI.ClosedSurfaceR4.RealModes.normalBudget_polynomial line 65
  8. lemma OAI.ClosedSurfaceR4.RealModes.freeNormalBudget_polynomial line 74
  9. lemma OAI.ClosedSurfaceR4.RealModes.reconstructionBudget_polynomial line 85