OAI/Geometry/IsometricImmersion/Assembly/SupportedPerturbations.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLocal.Perturbation.modelSquare line 15
  2. theorem OAI.SmoothLocal.Perturbation.modelSquare_isCompact line 17
  3. def OAI.SmoothLocal.Perturbation.patchCompact line 19
  4. abbrev OAI.SmoothLocal.Perturbation.SupportedTensor line 21
  5. theorem OAI.SmoothLocal.Perturbation.supportedTensor_eval_continuous line 24
  6. def OAI.SmoothLocal.Perturbation.symmetricSupportedSubmodule line 36
  7. theorem OAI.SmoothLocal.Perturbation.symmetricSupportedSubmodule_isClosed line 51
  8. abbrev OAI.SmoothLocal.Perturbation.SymmetricPerturbation line 58
  9. def OAI.SmoothLocal.Perturbation.perturbationTensor line 60
  10. theorem OAI.SmoothLocal.Perturbation.perturbationTensor_symmetric line 62
  11. theorem OAI.SmoothLocal.Perturbation.perturbationTensor_contDiff line 65
  12. theorem OAI.SmoothLocal.Perturbation.perturbationTensor_coeff_contDiff line 68
  13. theorem OAI.SmoothLocal.Perturbation.perturbationTensor_tsupport_subset line 73
  14. theorem OAI.SmoothLocal.Perturbation.perturbationTensor_zero_off_patch line 76
  15. def OAI.SmoothLocal.Perturbation.perturbationSeminorm line 79
  16. theorem OAI.SmoothLocal.Perturbation.perturbationSeminorm_continuous line 82
  17. theorem OAI.SmoothLocal.Perturbation.perturbation_derivative_norm_le line 86
  18. theorem OAI.SmoothLocal.Perturbation.supportedTensor_iteratedFDeriv_eval_continuous line 90
  19. def OAI.SmoothLocal.Perturbation.perturbedMetric line 97
  20. def OAI.SmoothLocal.Perturbation.metricPatchSet line 100
  21. theorem OAI.SmoothLocal.Perturbation.perturbedMetric_zero line 104
  22. theorem OAI.SmoothLocal.Perturbation.zero_mem_metricPatchSet line 109
  23. theorem OAI.SmoothLocal.Perturbation.patchBox_subset_modelSquare line 117
  24. theorem OAI.SmoothLocal.Perturbation.perturbedMetric_smoothPositiveOn line 121
  25. theorem OAI.SmoothLocal.Perturbation.constructedModel_zero_mem line 134