OAI/Geometry/SmoothYau/ProductMetric/FourWaveThreeSmul.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.YauCounterexamples.fourSplitEquiv line 17
  2. def OAI.YauCounterexamples.fourProjThree line 20
  3. def OAI.YauCounterexamples.fourProjCircle line 22
  4. lemma OAI.YauCounterexamples.four_chart_target line 24
  5. lemma OAI.YauCounterexamples.four_chart_symm_three line 31
  6. lemma OAI.YauCounterexamples.four_chart_symm_circle line 34
  7. lemma OAI.YauCounterexamples.four_chart_three line 37
  8. lemma OAI.YauCounterexamples.four_chart_symm_smooth line 39
  9. lemma OAI.YauCounterexamples.circle_chart_symm_smooth line 43
  10. lemma OAI.YauCounterexamples.four_chart_deriv_three line 50
  11. lemma OAI.YauCounterexamples.four_chart_deriv_circle line 77
  12. lemma OAI.YauCounterexamples.four_chartMetricForm line 101
  13. def OAI.YauCounterexamples.fourSplitBasis line 130
  14. lemma OAI.YauCounterexamples.fourSplitBasis_inl line 132
  15. lemma OAI.YauCounterexamples.fourSplitBasis_inr line 135
  16. lemma OAI.YauCounterexamples.fourSplitBasis_Pa line 138
  17. lemma OAI.YauCounterexamples.fourSplitBasis_Pb line 140
  18. lemma OAI.YauCounterexamples.fourSplitBasis_Qa line 142
  19. lemma OAI.YauCounterexamples.fourSplitBasis_Qb line 144
  20. lemma OAI.YauCounterexamples.four_metric_block line 146
  21. lemma OAI.YauCounterexamples.metricCoefficients_differentiable_univ line 157
  22. lemma OAI.YauCounterexamples.laplaceBeltrami_four_lift line 168
  23. lemma OAI.YauCounterexamples.four_lift_regular line 194
  24. def OAI.YauCounterexamples.fourTailHeadLinear line 227
  25. def OAI.YauCounterexamples.fourTailHeadEquiv line 234
  26. def OAI.YauCounterexamples.fourCircleCoord line 235
  27. def OAI.YauCounterexamples.fourWaveEquiv line 236
  28. def OAI.YauCounterexamples.fourProfileCenter line 238
  29. lemma OAI.YauCounterexamples.fourProfileCenter_three line 239
  30. lemma OAI.YauCounterexamples.fourWave_proj line 240
  31. lemma OAI.YauCounterexamples.fourWave_lift line 245
  32. lemma OAI.YauCounterexamples.extrudeSet_tailhead line 250
  33. lemma OAI.YauCounterexamples.extrudeSet_open line 255
  34. lemma OAI.YauCounterexamples.extrudeSet_convex line 258
  35. lemma OAI.YauCounterexamples.extrudeSet_disjoint line 261
  36. def OAI.YauCounterexamples.fourWaveCompact line 267
  37. lemma OAI.YauCounterexamples.fourWaveCompact_isCompact line 270
  38. lemma OAI.YauCounterexamples.fourWaveCompact_mem line 273
  39. lemma OAI.YauCounterexamples.four_signCertificate_bound line 278