OAI/Geometry/IsometricImmersion/Energy/WeightPrimitive.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLocal.Weighted.coordinateRectangle line 14
  2. theorem OAI.SmoothLocal.Weighted.coordinateRectangle_isOpen line 17
  3. theorem OAI.SmoothLocal.Weighted.point_mem_rectangle line 23
  4. theorem OAI.SmoothLocal.Weighted.point_eta line 28
  5. theorem OAI.SmoothLocal.Weighted.point_hasDerivAt_t line 32
  6. def OAI.SmoothLocal.Weighted.coordinatePrimitive line 38
  7. theorem OAI.SmoothLocal.Weighted.parameterDerivative_smooth_on_rectangle line 43
  8. theorem OAI.SmoothLocal.Weighted.compact_t_mem_rectangle_interval line 51
  9. theorem OAI.SmoothLocal.Weighted.coefficientFamily_apply_on_rectangle line 55
  10. theorem OAI.SmoothLocal.Weighted.coefficientFamily_contDiffOn_rectangle line 66
  11. theorem OAI.SmoothLocal.Weighted.coefficientFamily_jet_apply_on_rectangle line 91
  12. theorem OAI.SmoothLocal.Weighted.coefficientFamily_jet_contDiffOn_rectangle line 121
  13. theorem OAI.SmoothLocal.Weighted.primitiveFamily_joint_smooth line 141
  14. def OAI.SmoothLocal.Weighted.clampedPrimitive line 180
  15. theorem OAI.SmoothLocal.Weighted.clampedPrimitive_contDiffOn line 183
  16. theorem OAI.SmoothLocal.Weighted.clampedPrimitive_eq_integral line 194
  17. theorem OAI.SmoothLocal.Weighted.coordinatePrimitive_contDiffOn_inner line 208
  18. theorem OAI.SmoothLocal.Weighted.coordinatePrimitive_contDiffOn line 220
  19. theorem OAI.SmoothLocal.Weighted.coordinatePrimitive_initial line 230
  20. theorem OAI.SmoothLocal.Weighted.coordinatePrimitive_partial_t line 234
  21. theorem OAI.SmoothLocal.Weighted.primitive_directedM_partial_t line 264
  22. theorem OAI.SmoothLocal.Weighted.primitive_directedJ line 277