OAI/Algebra/AffineCancellation/CylinderShift.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

Polynomial stabilization without division by the distinguished coordinate.

  1. structure OAI.ComplexCancellation.Cylinder.Point line 12
  2. def OAI.ComplexCancellation.Cylinder.Point.x line 21
  3. def OAI.ComplexCancellation.Cylinder.Point.equation line 22
  4. def OAI.ComplexCancellation.Cylinder.Point.cubicDiff line 25
  5. lemma OAI.ComplexCancellation.Cylinder.Point.cubicDiff_spec line 27
  6. lemma OAI.ComplexCancellation.Cylinder.Point.cubicDiff_add line 32
  7. def OAI.ComplexCancellation.Cylinder.Point.shift line 38

    Source documentation

    A finite exponential shift fixing p, x, y, z and translating u by -p²w.

    def shift (q : Point R) (w : R) : Point R :=
…

    Mentions: OAI.ComplexCancellation.Cylinder.Point

  8. lemma OAI.ComplexCancellation.Cylinder.Point.shift_p line 44
  9. lemma OAI.ComplexCancellation.Cylinder.Point.shift_u line 45
  10. lemma OAI.ComplexCancellation.Cylinder.Point.shift_x line 47
  11. lemma OAI.ComplexCancellation.Cylinder.Point.shift_zero line 57
  12. lemma OAI.ComplexCancellation.Cylinder.Point.shift_add line 61
  13. lemma OAI.ComplexCancellation.Cylinder.Point.shift_equation line 91
  14. lemma OAI.ComplexCancellation.Cylinder.Point.shift_neg_shift line 103
  15. structure OAI.ComplexCancellation.Cylinder.Frame line 112
  16. def OAI.ComplexCancellation.Cylinder.Frame.x₀ line 120
  17. def OAI.ComplexCancellation.Cylinder.Frame.f₁ line 121
  18. def OAI.ComplexCancellation.Cylinder.Frame.f₀ line 122
  19. def OAI.ComplexCancellation.Cylinder.Frame.j₁ line 123
  20. def OAI.ComplexCancellation.Cylinder.Frame.j₀ line 124
  21. def OAI.ComplexCancellation.Cylinder.Frame.f line 125
  22. def OAI.ComplexCancellation.Cylinder.Frame.j line 126
  23. def OAI.ComplexCancellation.Cylinder.Frame.point line 127
  24. def OAI.ComplexCancellation.Cylinder.Frame.Q line 128
  25. def OAI.ComplexCancellation.Cylinder.Frame.c line 130
  26. def OAI.ComplexCancellation.Cylinder.Frame.q₁ line 131
  27. def OAI.ComplexCancellation.Cylinder.Frame.q₂ line 133
  28. def OAI.ComplexCancellation.Cylinder.Frame.Q₁ line 135
  29. lemma OAI.ComplexCancellation.Cylinder.Frame.Q_expand line 137
  30. lemma OAI.ComplexCancellation.Cylinder.Frame.equation_point line 141
  31. def OAI.ComplexCancellation.Cylinder.Frame.root line 155
  32. def OAI.ComplexCancellation.Cylinder.Frame.h line 156
  33. def OAI.ComplexCancellation.Cylinder.Frame.e line 158
  34. def OAI.ComplexCancellation.Cylinder.Frame.L line 160
  35. def OAI.ComplexCancellation.Cylinder.Frame.W line 161
  36. lemma OAI.ComplexCancellation.Cylinder.Frame.e_certificate line 164
  37. lemma OAI.ComplexCancellation.Cylinder.Frame.coordinate_equation line 172
  38. lemma OAI.ComplexCancellation.Cylinder.Frame.h_coordinates line 178
  39. lemma OAI.ComplexCancellation.Cylinder.Frame.e_coordinates line 185
  40. def OAI.ComplexCancellation.Cylinder.Point.frame line 195
  41. def OAI.ComplexCancellation.Cylinder.Point.linear line 197
  42. lemma OAI.ComplexCancellation.Cylinder.Point.point_frame line 200
  43. lemma OAI.ComplexCancellation.Cylinder.Frame.frame_point line 217
  44. lemma OAI.ComplexCancellation.Cylinder.Frame.linear_point line 226