OAI/Geometry/SurfaceImmersion/Correction/AdaptiveCorrectionStep.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

A single adaptive transition, with all admissibility conditions preserved.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.PreparedCorrection.stageRadius line 30
  2. structure OAI.ClosedSurfaceR4.FiniteOrderSmoothing.PreparedCorrection.Stage line 33
  3. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.PreparedCorrection.Stage.defect line 48
  4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.PreparedCorrection.Stage.finiteInput line 51
  5. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.PreparedCorrection.Stage.size line 57
  6. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.PreparedCorrection.Stage.CanAdvance line 60
  7. structure OAI.ClosedSurfaceR4.FiniteOrderSmoothing.PreparedCorrection.Transition line 67
  8. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.PreparedCorrection.transition_nonempty line 82

    Source documentation

    At every stage the order can be held. It is increased as soon as the next finite input bound and the next geometric threshold permit it.

    theorem transition_nonempty (hF : ContMDiff planeModel spaceModel ∞ F)
    {t : ℝ} (ht : 0 < t) (htsmall : t ≤ 1/32) {n : ℕ} (s : c.Stage t n) :
    Nonempty (c.Transition s) := by
…

    Mentions: OAI.ClosedSurfaceR4.planeModel