OAI/Geometry/BallPacking/Necessity/FiniteContinuation.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TwoPointContinuation.coordinateForm line 39
  2. theorem OAI.TwoPointContinuation.coordinateForm_apply line 45
  3. theorem OAI.TwoPointContinuation.alternating_above_dimension line 48
  4. def OAI.TwoPointContinuation.formFlux line 57
  5. theorem OAI.TwoPointContinuation.closedForm_box_flux line 61
  6. def OAI.TwoPointContinuation.pulledCoordinateForm line 89
  7. theorem OAI.TwoPointContinuation.pulledCoordinateForm_differentiable line 94
  8. theorem OAI.TwoPointContinuation.pulledCoordinateForm_closed line 102
  9. theorem OAI.TwoPointContinuation.fderiv_initial_spatial line 113
  10. theorem OAI.TwoPointContinuation.initial_flux line 130
  11. def OAI.TwoPointContinuation.cubeLower line 152
  12. def OAI.TwoPointContinuation.cubeUpper line 153
  13. theorem OAI.TwoPointContinuation.mem_cube_iff line 155
  14. def OAI.TwoPointContinuation.cylinderLower line 161
  15. def OAI.TwoPointContinuation.cylinderUpper line 162
  16. theorem OAI.TwoPointContinuation.mem_cylinder_iff line 164
  17. theorem OAI.TwoPointContinuation.tail_face_norm line 172
  18. theorem OAI.TwoPointContinuation.finite_continuation line 180
  19. theorem OAI.TwoPointContinuation.localized_continuation line 310
  20. theorem OAI.TwoPointContinuation.continuous_localized_continuation line 371
  21. theorem OAI.TwoPointContinuation.finite_rank_approx line 433