OAI/Geometry/SmoothYau/SphereMetric/ThreeRobustProfileNormedSpace.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.YauCounterexamples.exists_smooth_local_log line 17
  2. lemma OAI.YauCounterexamples.actual_strict_region_open line 39
  3. lemma OAI.YauCounterexamples.exists_local_strict_ball line 48
  4. lemma OAI.YauCounterexamples.exists_three_local_strict_profile line 58
  5. def OAI.YauCounterexamples.threeProfilePoint line 85
  6. def OAI.YauCounterexamples.threeProfileCenter line 94
  7. lemma OAI.YauCounterexamples.threeProfilePoint_zero line 95
  8. lemma OAI.YauCounterexamples.threeProfilePoint_one line 96
  9. lemma OAI.YauCounterexamples.threeProfilePoint_two line 97
  10. def OAI.YauCounterexamples.threeEnvelopeExponent line 99
  11. lemma OAI.YauCounterexamples.threeEnvelopeExponent_pos line 100
  12. lemma OAI.YauCounterexamples.threeEnvelopeExponent_lt line 102
  13. lemma OAI.YauCounterexamples.threeEnvelopeExponent_mul line 106
  14. theorem OAI.YauCounterexamples.exists_three_profile_seed line 109
  15. theorem OAI.YauCounterexamples.exists_three_amplified_profile line 122
  16. lemma OAI.YauCounterexamples.linearPullbackMetric_trace line 153
  17. lemma OAI.YauCounterexamples.linearPullbackMetric_strict line 161
  18. def OAI.YauCounterexamples.threeNormalEquiv line 184
  19. def OAI.YauCounterexamples.threeNormalMetric line 187
  20. theorem OAI.YauCounterexamples.exists_three_normal_seed line 190
  21. def OAI.YauCounterexamples.threeCouplingRadius line 209
  22. def OAI.YauCounterexamples.threeGlobalRadius line 210
  23. def OAI.YauCounterexamples.threeGlobalLog line 212
  24. lemma OAI.YauCounterexamples.threeGlobalRadius_lower line 214
  25. lemma OAI.YauCounterexamples.threeGlobalRadius_pos line 227
  26. lemma OAI.YauCounterexamples.threeGlobalRadius_le_one line 229
  27. lemma OAI.YauCounterexamples.threeGlobalRadius_continuous line 234
  28. lemma OAI.YauCounterexamples.threeGlobalLog_continuous line 240
  29. lemma OAI.YauCounterexamples.threeGlobalLog_bounds line 242
  30. lemma OAI.YauCounterexamples.three_chart_symm_zero line 249
  31. lemma OAI.YauCounterexamples.three_chart_symm_continuous line 252
  32. lemma OAI.YauCounterexamples.threeRadiusSq_eq_norm line 255
  33. lemma OAI.YauCounterexamples.threeLogEnvelope_eq line 262
  34. lemma OAI.YauCounterexamples.threeGlobalLog_local line 267
  35. def OAI.YauCounterexamples.threeNormalInv line 304
  36. def OAI.YauCounterexamples.threeNormalGlue line 306
  37. lemma OAI.YauCounterexamples.threeNormalGlue_chart line 308
  38. lemma OAI.YauCounterexamples.threeNormalGlue_smooth line 314
  39. lemma OAI.YauCounterexamples.threeNormalGlue_tsupport line 321
  40. lemma OAI.YauCounterexamples.threeNormalGlue_exterior line 336
  41. theorem OAI.YauCounterexamples.exists_three_normal_envelope line 353
  42. theorem OAI.YauCounterexamples.exists_three_global_profile_family line 393
  43. lemma OAI.YauCounterexamples.productWaveFrequency_scaled_bounds line 471
  44. lemma OAI.YauCounterexamples.three_radius_pow_eq_exp line 498
  45. lemma OAI.YauCounterexamples.three_positive_envelope_gap line 502
  46. lemma OAI.YauCounterexamples.three_negative_envelope_gap line 515
  47. lemma OAI.YauCounterexamples.three_metricCoefficients_smooth line 554
  48. theorem OAI.YauCounterexamples.three_metric_first_jet_neighborhood line 563
  49. def OAI.YauCounterexamples.threeNormalMetricOf line 621
  50. def OAI.YauCounterexamples.ThreeCleanBall line 625
  51. lemma OAI.YauCounterexamples.threeNormalInv_clean_eventually line 627
  52. theorem OAI.YauCounterexamples.exists_three_robust_seed line 641
  53. theorem OAI.YauCounterexamples.exists_three_robust_exhaustible_envelopes line 685
  54. theorem OAI.YauCounterexamples.exists_three_robust_global_profile_family line 713