OAI/Geometry/StableBernstein/Estimates/PuncturedSard.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.StableBernstein.W30.iteratedDeriv_affine_line line 29
  2. theorem OAI.StableBernstein.W30.taylorWithinEval_eq_of_flat line 42
  3. theorem OAI.StableBernstein.W30.flat_taylor_bound_segment line 52
  4. theorem OAI.StableBernstein.W30.flat_taylor_bound_convex line 87
  5. theorem OAI.StableBernstein.W30.flat_taylor_bound_ball line 95
  6. def OAI.Bernstein.Sard.chartExceptionalValues line 113
  7. theorem OAI.Bernstein.Sard.chartExceptionalValues_eq line 117
  8. theorem OAI.Bernstein.Sard.exists_countable_chart_exceptional_cover line 129
  9. theorem OAI.Bernstein.Sard.exceptionalValues_null_of_chart_null line 152
  10. theorem OAI.Bernstein.Sard.chart_fderiv_zero_of_mfderiv_zero line 162
  11. theorem OAI.Bernstein.Sard.criticalValues_null_of_chart_criticalValues_null line 174
  12. theorem OAI.Bernstein.Sard.ae_regularValues_of_chart_criticalValues_null line 186
  13. theorem OAI.Bernstein.Sard.ae_regularValues_of_scalarSard line 201
  14. theorem OAI.StableBernstein.W30.iteratedDeriv_affine_line_local line 220
  15. theorem OAI.StableBernstein.W30.flat_taylor_bound_segment_local line 241
  16. theorem OAI.StableBernstein.W30.flat_taylor_bound_convex_local line 279
  17. theorem OAI.Bernstein.Sard.scalar_sard_one_dimensional line 294
  18. theorem OAI.Bernstein.Sard.scalar_sard_one_dimensional_deriv line 306
  19. theorem OAI.StableBernstein.W30.sixFlat_holderOn_local line 333
  20. theorem OAI.StableBernstein.W30.volume_image_sixFlat_local_eq_zero line 350
  21. theorem OAI.StableBernstein.W30.exists_ball_sixFlat_image_null line 367
  22. theorem OAI.Bernstein.Sard.regular_scalar_range line 403
  23. theorem OAI.Bernstein.Sard.regular_scalar_kernel_dimension line 408
  24. theorem OAI.Bernstein.Sard.exists_smooth_regular_stratum_chart line 416
  25. theorem OAI.Bernstein.Sard.restricted_fderiv_zero line 502
  26. theorem OAI.Bernstein.Sard.regular_stratum_local_image_null line 517
  27. theorem OAI.Bernstein.Sard.contDiffOn_iteratedFDeriv_component line 541
  28. theorem OAI.Bernstein.Sard.derivative_component_stratum_local_image_null line 553
  29. theorem OAI.Bernstein.Sard.scalar_sard_finrank_one line 575
  30. theorem OAI.Bernstein.Sard.exists_regular_iteratedFDeriv_component line 598
  31. theorem OAI.Bernstein.Sard.image_null_of_locally_image_null line 623
  32. theorem OAI.Bernstein.Sard.nonflat_stratum_image_null line 639
  33. def OAI.Bernstein.Sard.sixFlatSet line 668
  34. def OAI.Bernstein.Sard.nonflatCriticalStratum line 671
  35. theorem OAI.Bernstein.Sard.criticalSet_subset_sixFlat_union_strata line 675
  36. theorem OAI.Bernstein.Sard.sixFlatSet_image_null line 704
  37. theorem OAI.Bernstein.Sard.scalar_sard_finrank_eq line 717
  38. theorem OAI.Bernstein.Sard.scalar_sard_finrank_le_six line 762
  39. theorem OAI.Bernstein.Sard.scalar_sard_E6 line 770
  40. theorem OAI.Bernstein.Sard.manifold_ae_regularValues line 777
  41. theorem OAI.Bernstein.Sard.manifold_ae_noncritical_values line 785
  42. def OAI.StableBernstein.W26.puncturedCriticalSet line 808
  43. def OAI.StableBernstein.W26.poleCriticalSet line 811
  44. theorem OAI.StableBernstein.W26.chart_fderiv_zero_of_punctured line 814
  45. theorem OAI.StableBernstein.W26.punctured_critical_values_null line 830
  46. theorem OAI.StableBernstein.W26.pole_critical_values_null line 851
  47. def OAI.StableBernstein.W26.poleCriticalCarrier line 857
  48. theorem OAI.StableBernstein.W26.measurableSet_poleCriticalCarrier line 861
  49. theorem OAI.StableBernstein.W26.poleCriticalCarrier_null line 865
  50. theorem OAI.StableBernstein.W26.mapsTo_poleCriticalCarrier line 872