OAI/Geometry/SurfaceImmersion/Atlas/ChartedTrialAmplitude.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Cutoff square-root trial amplitudes on the actual transported support. These use the original tensor field and the inverse of its phase chart.

  1. def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.PolynomialSolveData.trialAmplitude line 22
  2. lemma OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.PolynomialSolveData.trialAmplitude_apply line 32
  3. theorem OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.PolynomialSolveData.trialAmplitude_bounds line 41