OAI/Geometry/SurfaceImmersion/Correction/ChartedMeanData.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Fixed geometric and jet bounds for the actual mean map of one phase.

  1. structure OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.ChartedMeanData line 12
  2. def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.ChartedMeanData.amplitude line 39
  3. def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.ChartedMeanData.mean line 42
  4. def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.ChartedMeanData.leading line 45
  5. def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.ChartedMeanData.freeAmplitude line 48
  6. theorem OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.ChartedMeanData.majorants line 51
  7. lemma OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.ChartedMeanData.zero_phase_identity line 60