OAI/Geometry/SurfaceImmersion/Correction/ChartedCombinedMean.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The combined mean of the actual transported free amplitude, with the polynomial evaluated in the original coordinates and the metric transformed as a two-tensor.

  1. def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.PolynomialSolveData.polynomialMeanField line 21
  2. def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.PolynomialSolveData.combinedMeanField line 33
  3. def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.PolynomialSolveData.leadingFieldInChart line 37
  4. def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.PolynomialSolveData.leadingField line 47
  5. lemma OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.PolynomialSolveData.metric_zero_phase_identity line 51
  6. theorem OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.PolynomialSolveData.combined_zero_phase_identity line 69