OAI/Geometry/SurfaceImmersion/Correction/AdaptiveCorrectionSequence.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Construction of the correction sequence, and unbounded growth of the finite derivative order despite the absence of uniform high-order input bounds.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.PreparedCorrection.chosenTransition line 32
  2. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.PreparedCorrection.sequence line 35
  3. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.PreparedCorrection.increment line 39
  4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.PreparedCorrection.sequence_succ_map line 42
  5. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.PreparedCorrection.sequence_succ_order line 47
  6. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.PreparedCorrection.sequence_order_monotone line 54
  7. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.PreparedCorrection.increment_smooth line 61
  8. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.PreparedCorrection.sequence_partialMap line 65
  9. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.PreparedCorrection.sequence_size_recurrence line 76
  10. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.PreparedCorrection.sequence_order_tendsto line 91

    Source documentation

    The adaptive order really tends to infinity. The proof uses the actual finite norm of every stage and the all-order affine recurrence.

    theorem sequence_order_tendsto (seed : c.Stage t 0) :
    Tendsto (fun n => (c.sequence hF ht htsmall seed n).order) atTop atTop := by
…
  11. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.PreparedCorrection.increment_eventual_bound line 106
  12. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.PreparedCorrection.sequence_amplitude_tendsto line 114