OAI/Geometry/SurfaceImmersion/Correction/ChartedZeroMean.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The actual zero phase of a transported free amplitude. The metric part transforms as a covariant tensor through the phase chart.

  1. lemma OAI.ClosedSurfaceR4.RealModes.phaseZeroTensor_congr line 15
  2. lemma OAI.ClosedSurfaceR4.RealModes.phaseZeroTensor_chart line 21
  3. def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.PolynomialSolveData.metricMeanInChart line 48
  4. def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.PolynomialSolveData.leadingInChart line 54
  5. lemma OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.PolynomialSolveData.freeSeed_zeroPhase line 57
  6. lemma OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.PolynomialSolveData.originalFreeSeed_zeroPhase line 67