OAI/Geometry/SurfaceImmersion/Atlas/CoordinateQuadraticExpansion.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Transport the polynomial quadratic expansion into the same coordinates and phase labels as the metric quadratic expansion.

  1. abbrev OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.coordinatePhase line 13
  2. abbrev OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.coordinateAmplitude line 14
  3. lemma OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.coordinate_phase_value line 16
  4. lemma OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.real_oscillatorySum_coordinates line 22
  5. lemma OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.coordinate_quadratic_phase line 33
  6. def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.coordinateQuadraticPolynomial line 41
  7. def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.coordinateQuadraticMean line 46
  8. def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.coordinateQuadraticCoefficient line 52
  9. theorem OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.coordinate_quadratic_polynomial_expansion line 58