OAI/Geometry/SurfaceImmersion/Correction/PolynomialProfileTransfer.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The size and residual factors depend only on numeric coefficient profiles, not on the map, phase, chart, target or scale in a solver record. The pure profiles let a family use those factors without introducing a reference solver at unit scale.

  1. def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.PolynomialSolveData.κProfile line 20
  2. def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.PolynomialSolveData.sizeProfile line 24
  3. def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.PolynomialSolveData.residualProfile line 28
  4. theorem OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.PolynomialSolveData.κProfile_nonneg line 33
  5. theorem OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.PolynomialSolveData.sizeProfile_nonneg line 37
  6. theorem OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.PolynomialSolveData.residualProfile_nonneg line 44
  7. theorem OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.PolynomialSolveData.κ_eq_κProfile line 56
  8. theorem OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.PolynomialSolveData.sizeFactor_eq_sizeProfile line 61
  9. theorem OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.PolynomialSolveData.residualFactor_eq_residualProfile line 66
  10. theorem OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.PolynomialSolveData.factors_eq_of_profiles line 73

    Source documentation

    Solver records at different maps or scales have the same factors when their three numeric profiles agree.

    theorem factors_eq_of_profiles
    {ε' τ' : ℝ} {H : Base → Space} {hH : ContDiff ℝ ∞ H} {ψ : Base → ℝ}
    {L : TopologicalSpace.Compacts Base} {s' : ℝ≥0}
    (d : PolynomialSolveData P ε' H hH ψ L τ' s')
    (hC : c.C = d.C) (hD : c.D = d.D) (hJ : c.J = d.J) (q m : ℕ) :
    c.sizeFactor q m = d.sizeFactor q m ∧
      c.residualFactor q m = d.residualFactor q m := by
…

    Mentions: OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.JetPolynomial.Space, OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.PolynomialSolveData