OAI/Geometry/IsometricImmersion/Caps/EllipticCutoff.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SmoothLocal.Weighted.smoothTransition_deriv_zero_of_nonpos line 18
  2. theorem OAI.SmoothLocal.Weighted.smoothTransition_deriv_zero_of_one_le line 25
  3. theorem OAI.SmoothLocal.Weighted.exists_smoothTransition_derivative_bound line 32
  4. def OAI.SmoothLocal.Weighted.transitionDerivativeBound line 51
  5. theorem OAI.SmoothLocal.Weighted.transitionDerivativeBound_pos line 54
  6. theorem OAI.SmoothLocal.Weighted.smoothTransition_deriv_abs_le line 57
  7. def OAI.SmoothLocal.Weighted.intervalCutoff line 61
  8. theorem OAI.SmoothLocal.Weighted.intervalCutoff_contDiff line 63
  9. theorem OAI.SmoothLocal.Weighted.intervalCutoff_range line 66
  10. theorem OAI.SmoothLocal.Weighted.intervalCutoff_zero line 70
  11. theorem OAI.SmoothLocal.Weighted.intervalCutoff_one line 75
  12. theorem OAI.SmoothLocal.Weighted.intervalCutoff_hasDerivAt line 80
  13. theorem OAI.SmoothLocal.Weighted.intervalCutoff_deriv line 96
  14. theorem OAI.SmoothLocal.Weighted.intervalCutoff_deriv_zero_left line 101
  15. theorem OAI.SmoothLocal.Weighted.intervalCutoff_deriv_zero_right line 106
  16. theorem OAI.SmoothLocal.Weighted.intervalCutoff_deriv_abs_le line 111
  17. theorem OAI.SmoothLocal.Weighted.intervalCutoff_deriv_support line 116
  18. def OAI.SmoothLocal.Weighted.ellipticPhi line 124
  19. theorem OAI.SmoothLocal.Weighted.ellipticPhi_contDiff line 126
  20. theorem OAI.SmoothLocal.Weighted.ellipticPhi_zero line 129
  21. theorem OAI.SmoothLocal.Weighted.ellipticPhi_one line 132
  22. theorem OAI.SmoothLocal.Weighted.ellipticPhi_deriv_abs_le line 135
  23. theorem OAI.SmoothLocal.Weighted.ellipticPhi_deriv_support line 144
  24. def OAI.SmoothLocal.Weighted.threeEdgeCutoff line 152
  25. theorem OAI.SmoothLocal.Weighted.threeEdgeCutoff_contDiff line 156
  26. theorem OAI.SmoothLocal.Weighted.threeEdgeCutoff_range line 162
  27. theorem OAI.SmoothLocal.Weighted.threeEdgeCutoff_one line 176
  28. theorem OAI.SmoothLocal.Weighted.threeEdgeCutoff_zero line 185
  29. theorem OAI.SmoothLocal.Weighted.threeEdgeCutoff_partial line 194
  30. theorem OAI.SmoothLocal.Weighted.abs_mul_two_cutoffs_le line 218
  31. theorem OAI.SmoothLocal.Weighted.threeEdgeCutoff_partial_bounds line 227
  32. theorem OAI.SmoothLocal.Weighted.threeEdgeCutoff_partial_t_support line 254
  33. theorem OAI.SmoothLocal.Weighted.threeEdgeCutoff_partial_s_support line 268
  34. def OAI.SmoothLocal.Weighted.capInnerEdge line 278
  35. def OAI.SmoothLocal.Weighted.capOuterEdge line 279
  36. theorem OAI.SmoothLocal.Weighted.capEdges_bounds line 281
  37. def OAI.SmoothLocal.Weighted.capSpatialCutoff line 295
  38. theorem OAI.SmoothLocal.Weighted.capSpatialCutoff_contDiff line 299
  39. theorem OAI.SmoothLocal.Weighted.capSpatialCutoff_range line 302
  40. theorem OAI.SmoothLocal.Weighted.capSpatialCutoff_one line 306
  41. theorem OAI.SmoothLocal.Weighted.capSpatialCutoff_zero line 315
  42. theorem OAI.SmoothLocal.Weighted.capSpatialCutoff_derivative_bands line 327
  43. theorem OAI.SmoothLocal.Weighted.ellipticPhi_ratio_derivative_bound line 345
  44. def OAI.SmoothLocal.Weighted.ellipticWeight line 379
  45. def OAI.SmoothLocal.Weighted.ellipticGate line 382
  46. def OAI.SmoothLocal.Weighted.ellipticAmplitude line 385
  47. theorem OAI.SmoothLocal.Weighted.ellipticAmplitude_sq line 388
  48. theorem OAI.SmoothLocal.Weighted.edgeDistance_partial line 393
  49. theorem OAI.SmoothLocal.Weighted.ellipticGate_differentiableAt line 401
  50. theorem OAI.SmoothLocal.Weighted.ellipticGate_partial line 412
  51. theorem OAI.SmoothLocal.Weighted.ellipticGate_partial_bound line 435
  52. theorem OAI.SmoothLocal.Weighted.ellipticAmplitude_differentiableAt line 445
  53. theorem OAI.SmoothLocal.Weighted.ellipticAmplitude_partial line 452
  54. theorem OAI.SmoothLocal.Weighted.ellipticWeight_partial line 476
  55. theorem OAI.SmoothLocal.Weighted.amplitude_derivative_algebra_bound line 489
  56. theorem OAI.SmoothLocal.Weighted.ellipticWeight_partial_bound line 522
  57. theorem OAI.SmoothLocal.Weighted.ellipticWeight_contDiffOn line 549
  58. theorem OAI.SmoothLocal.Weighted.ellipticWeight_nonneg line 558
  59. theorem OAI.SmoothLocal.Weighted.ellipticWeight_le_distance_six line 563
  60. theorem OAI.SmoothLocal.Weighted.ellipticWeight_edge_zero line 577
  61. theorem OAI.SmoothLocal.Weighted.ellipticWeight_tendsto_edge_zero line 581
  62. theorem OAI.SmoothLocal.Weighted.ellipticWeight_flux_tendsto_edge_zero line 591
  63. theorem OAI.SmoothLocal.Weighted.ellipticWeight_partial_zero_of_zero line 597
  64. theorem OAI.SmoothLocal.Weighted.ellipticWeight_pos_implies_curvature line 609