OAI/Geometry/QuadricBundles/LaurentCech.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.QuadricCounterexample.LaurentCech.Chart line 11
  2. abbrev OAI.QuadricCounterexample.LaurentCech.Exponent line 12
  3. abbrev OAI.QuadricCounterexample.LaurentCech.LaurentCoefficients line 13
  4. def OAI.QuadricCounterexample.LaurentCech.ScalarAllows line 15
  5. def OAI.QuadricCounterexample.LaurentCech.ChartAllows line 18
  6. def OAI.QuadricCounterexample.LaurentCech.OverlapAllows line 21
  7. lemma OAI.QuadricCounterexample.LaurentCech.scalar_bad_unique line 25
  8. lemma OAI.QuadricCounterexample.LaurentCech.forbidden_coefficient_zero line 29
  9. def OAI.QuadricCounterexample.LaurentCech.badChart line 50
  10. lemma OAI.QuadricCounterexample.LaurentCech.badChart_bad line 53
  11. def OAI.QuadricCounterexample.LaurentCech.correction line 57
  12. lemma OAI.QuadricCounterexample.LaurentCech.correction_apply line 60
  13. theorem OAI.QuadricCounterexample.LaurentCech.split_cocycle line 69
  14. def OAI.QuadricCounterexample.LaurentCech.eval line 99
  15. lemma OAI.QuadricCounterexample.LaurentCech.eval_add line 101
  16. lemma OAI.QuadricCounterexample.LaurentCech.eval_zero line 104
  17. lemma OAI.QuadricCounterexample.LaurentCech.eval_sub line 105
  18. lemma OAI.QuadricCounterexample.LaurentCech.eval_single line 110
  19. def OAI.QuadricCounterexample.LaurentCech.exponent line 113
  20. def OAI.QuadricCounterexample.LaurentCech.ofPolynomial line 114
  21. lemma OAI.QuadricCounterexample.LaurentCech.ofPolynomial_add line 116
  22. lemma OAI.QuadricCounterexample.LaurentCech.ofPolynomial_monomial line 118
  23. lemma OAI.QuadricCounterexample.LaurentCech.eval_ofPolynomial line 121
  24. lemma OAI.QuadricCounterexample.LaurentCech.exponent_injective line 132
  25. lemma OAI.QuadricCounterexample.LaurentCech.ofPolynomial_injective line 137
  26. def OAI.QuadricCounterexample.LaurentCech.shift line 142
  27. lemma OAI.QuadricCounterexample.LaurentCech.shift_injective line 144
  28. lemma OAI.QuadricCounterexample.LaurentCech.eval_shift line 146
  29. lemma OAI.QuadricCounterexample.LaurentCech.exists_shift_nonneg line 157
  30. def OAI.QuadricCounterexample.LaurentCech.naturalExponent line 173
  31. def OAI.QuadricCounterexample.LaurentCech.toPolynomial line 175
  32. lemma OAI.QuadricCounterexample.LaurentCech.ofPolynomial_toPolynomial line 177
  33. lemma OAI.QuadricCounterexample.LaurentCech.baseEval_on_torus_injective line 200
  34. lemma OAI.QuadricCounterexample.LaurentCech.eval_injective_on_torus line 213
  35. def OAI.QuadricCounterexample.LaurentCech.transformExponent line 236
  36. lemma OAI.QuadricCounterexample.LaurentCech.transformExponent_involutive line 239
  37. def OAI.QuadricCounterexample.LaurentCech.transform line 244
  38. lemma OAI.QuadricCounterexample.LaurentCech.transform_involutive line 246
  39. lemma OAI.QuadricCounterexample.LaurentCech.exponent_nonneg line 253
  40. lemma OAI.QuadricCounterexample.LaurentCech.ofPolynomial_nonneg line 255
  41. lemma OAI.QuadricCounterexample.LaurentCech.chartAllows_transform_iff line 259
  42. lemma OAI.QuadricCounterexample.LaurentCech.transform_nonneg_iff line 263
  43. lemma OAI.QuadricCounterexample.LaurentCech.transform_polynomial_support line 268
  44. lemma OAI.QuadricCounterexample.LaurentCech.exists_polynomial_of_chartAllows line 272
  45. def OAI.QuadricCounterexample.LaurentCech.masterCoordinates line 283
  46. def OAI.QuadricCounterexample.LaurentCech.masterFrame line 285
  47. lemma OAI.QuadricCounterexample.LaurentCech.masterCoordinates_nonzero line 287
  48. lemma OAI.QuadricCounterexample.LaurentCech.masterCoordinates_involutive line 291
  49. lemma OAI.QuadricCounterexample.LaurentCech.scalar_transform_eval line 295
  50. lemma OAI.QuadricCounterexample.LaurentCech.eval_transform line 301
  51. lemma OAI.QuadricCounterexample.LaurentCech.eval_transform_polynomial line 312
  52. lemma OAI.QuadricCounterexample.denominator_dvd_power line 323
  53. lemma OAI.QuadricCounterexample.UniformlyRegularOn.exists_power_denominator line 342
  54. lemma OAI.QuadricCounterexample.UniformlyRegularOn.exists_polynomial line 359
  55. def OAI.QuadricCounterexample.LaurentCech.inverseExponent line 374
  56. lemma OAI.QuadricCounterexample.LaurentCech.eval_inverseExponent line 376
  57. lemma OAI.QuadricCounterexample.LaurentCech.torus_mem_overlap line 381
  58. lemma OAI.QuadricCounterexample.LaurentCech.transform_overlap_support line 384
  59. lemma OAI.QuadricCounterexample.LaurentCech.exists_overlap_laurent line 400
  60. def OAI.QuadricCounterexample.LaurentCech.lineFactor line 414
  61. lemma OAI.QuadricCounterexample.LaurentCech.lineFactor_regular line 416
  62. lemma OAI.QuadricCounterexample.LaurentCech.masterFrame_ne_zero line 419
  63. lemma OAI.QuadricCounterexample.LaurentCech.masterCoordinates_change line 423
  64. lemma OAI.QuadricCounterexample.LaurentCech.masterFrame_change line 429
  65. lemma OAI.QuadricCounterexample.LaurentCech.uniformlyRegular_eq_of_torus line 444
  66. theorem OAI.QuadricCounterexample.LaurentCech.split_regular_line_cocycle line 460