OAI/Geometry/SurfaceImmersion/Correction/ChartedFreeSeed.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The free geometric amplitude in the original coordinates. The same actual polynomial operator is conjugated into the phase chart, and the resulting amplitude is transported back with controlled derivative loss.

  1. lemma OAI.ClosedSurfaceR4.RealModes.RealModeDomain.of_complex line 15
  2. abbrev OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.PolynomialSolveData.chartCompact line 40
  3. abbrev OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.PolynomialSolveData.realMap line 42
  4. theorem OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.PolynomialSolveData.realDomain line 44
  5. def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.PolynomialSolveData.operator line 46
  6. def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.PolynomialSolveData.freeSeed line 51
  7. def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.PolynomialSolveData.originalFreeSeed line 56
  8. lemma OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.PolynomialSolveData.originalFreeSeed_sub line 62
  9. theorem OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.PolynomialSolveData.originalFreeSeed_bound line 67