OAI/Analysis/HotSpots/ClosedChart.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.StrictHotSpots.Rolling.taylor_quadratic line 17
  2. lemma OAI.StrictHotSpots.Rolling.norm_sub_smul_sq line 30
  3. lemma OAI.StrictHotSpots.Rolling.tangent_ball_linear line 36
  4. lemma OAI.StrictHotSpots.Rolling.balls_of_taylor line 47
  5. lemma OAI.StrictHotSpots.Rolling.tangent_ball_mono line 103
  6. lemma OAI.StrictHotSpots.Rolling.nearest_normal_of_balls line 118
  7. lemma OAI.StrictHotSpots.Rolling.near_interior_ball line 147
  8. lemma OAI.StrictHotSpots.Rolling.normals_bound line 179
  9. lemma OAI.StrictHotSpots.Rolling.interior_centers_bound line 205
  10. lemma OAI.StrictHotSpots.HasFDerivAt.eventually_lt_along_ray line 231
  11. lemma OAI.StrictHotSpots.regular_level_uniqueDiffWithinAt line 246
  12. lemma OAI.StrictHotSpots.SmoothBoundary.uniqueDiffOn_closure line 284
  13. lemma OAI.StrictHotSpots.SmoothBoundary.exterior_ball_in_neighborhood line 295
  14. lemma OAI.StrictHotSpots.boundary_level_zero line 341
  15. lemma OAI.StrictHotSpots.SmoothBoundary.local_rolling_balls line 360
  16. lemma OAI.StrictHotSpots.finite_positive_lower line 447
  17. theorem OAI.StrictHotSpots.SmoothBoundary.uniform_rolling_balls line 463
  18. theorem OAI.StrictHotSpots.SmoothBoundary.complex_rolling_balls line 500
  19. lemma OAI.StrictHotSpots.Riemann.boundary_distance_pos line 527
  20. lemma OAI.StrictHotSpots.Riemann.nearest_frontier line 534
  21. lemma OAI.StrictHotSpots.Riemann.compact_core line 555
  22. lemma OAI.StrictHotSpots.Riemann.compact_disk_separation line 576
  23. lemma OAI.StrictHotSpots.Riemann.core_of_ball_subset line 584
  24. theorem OAI.StrictHotSpots.Riemann.domain_distance_le_disk_distance line 595
  25. lemma OAI.StrictHotSpots.Riemann.exterior_ball_distance line 646
  26. theorem OAI.StrictHotSpots.Riemann.schwarz_exterior_ball line 656
  27. theorem OAI.StrictHotSpots.Riemann.bounded_deriv_of_rolling_balls line 695
  28. lemma OAI.StrictHotSpots.Riemann.schwarz_pick_center line 755
  29. theorem OAI.StrictHotSpots.Riemann.disk_distance_le_domain_distance line 782
  30. theorem OAI.StrictHotSpots.Riemann.bounded_inverse_deriv_of_rolling_balls line 844
  31. lemma OAI.StrictHotSpots.Riemann.complex_lipschitz_extension line 877
  32. theorem OAI.StrictHotSpots.Riemann.closed_disk_extension line 901
  33. lemma OAI.StrictHotSpots.Riemann.dist_image_le_on_ball line 933
  34. theorem OAI.StrictHotSpots.Riemann.lipschitz_of_rolling_balls line 945
  35. theorem OAI.StrictHotSpots.Riemann.closed_bilipschitz_extension line 1045
  36. def OAI.StrictHotSpots.Riemann.closedHomeomorph line 1084
  37. lemma OAI.StrictHotSpots.Riemann.closed_extension_frontier line 1097
  38. structure OAI.StrictHotSpots.Conformal.ClosedDiskChart line 1129
  39. theorem OAI.StrictHotSpots.Conformal.exists_closed_disk_chart line 1162
  40. def OAI.StrictHotSpots.Conformal.ClosedDiskChart.diskMap line 1313
  41. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.diskMap_eq line 1327
  42. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.diskMap_smooth line 1331
  43. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.diskMap_inverse_smooth line 1334
  44. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.diskMap_deriv line 1337
  45. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.diskMap_inverse_deriv line 1339
  46. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.continuous_closed line 1341
  47. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.maps_closed line 1342
  48. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.inverse_maps_closed line 1343
  49. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.diskMap_agrees line 1345
  50. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.diskMap_inverse_agrees line 1346
  51. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.maps_boundary line 1348
  52. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.inverse_maps_boundary line 1360
  53. def OAI.StrictHotSpots.Conformal.ClosedDiskChart.boundaryHomeomorph line 1372
  54. def OAI.StrictHotSpots.closedGradient line 1394
  55. lemma OAI.StrictHotSpots.closedGradient_eq line 1397
  56. lemma OAI.StrictHotSpots.closedGradient_continuous line 1402
  57. lemma OAI.StrictHotSpots.continuous_closure_memLp line 1409
  58. lemma OAI.StrictHotSpots.smooth_closure_H1 line 1418
  59. lemma OAI.StrictHotSpots.smooth_closure_zero_H10 line 1427
  60. lemma OAI.StrictHotSpots.closure_directional_smooth line 1433
  61. def OAI.StrictHotSpots.Conformal.ClosedDiskChart.pullDatum line 1447
  62. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.pullDatum_continuous line 1449
  63. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.pullDatum_eq_inner line 1452
  64. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.pullDatum_smooth line 1455
  65. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.pullDatum_grad_norm line 1459
  66. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.pullDatum_bounded_gradient line 1472
  67. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.pullDatum_lipschitz line 1486
  68. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.pullDatum_H1 line 1499