OAI/Geometry/IsometricImmersion/Assembly/FlatPatchSum.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLocal.Geometry.patchSeriesWeight line 13
  2. theorem OAI.SmoothLocal.Geometry.patchSeriesWeight_hasSum line 15
  3. theorem OAI.SmoothLocal.Geometry.patchSeriesWeight_pos line 18
  4. def OAI.SmoothLocal.Geometry.flatPatchSum line 25
  5. theorem OAI.SmoothLocal.Geometry.compactSmooth_has_derivative_bounds line 28
  6. theorem OAI.SmoothLocal.Geometry.exists_summable_derivative_majorant line 35
  7. theorem OAI.SmoothLocal.Geometry.flatPatchSum_summable line 56
  8. theorem OAI.SmoothLocal.Geometry.flatPatchSum_norm_le line 65
  9. theorem OAI.SmoothLocal.Geometry.flatPatchSum_contDiff line 73
  10. theorem OAI.SmoothLocal.Geometry.flatPatchSum_iteratedFDeriv line 81
  11. theorem OAI.SmoothLocal.Geometry.flatPatchSum_derivatives_tendstoUniformly line 91
  12. theorem OAI.SmoothLocal.Geometry.flatPatchSum_all_jets_zero line 106
  13. theorem OAI.SmoothLocal.Geometry.hasCompactSupport_of_accumulatingDisk_support line 119
  14. theorem OAI.SmoothLocal.Geometry.accumulatingDisk_flat_sum line 125