PerturbedSolverTransfer.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Add a fixed polynomial perturbation to an existing geometric solver. The polynomial bound is obtained uniformly from a fixed compact jet range and fixed coordinate profiles, before the map and scales are supplied.

def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.PolynomialSolveData.withPolynomial line 19
Source documentation
Reuse all geometric and reconstruction data. The uniform theorem below provides the polynomial estimate required by this constructor.
```
def withPolynomial {n : ℕ} {G : Base → Space} {hG : ContDiff ℝ ∞ G}
    {φ : Base → ℝ} {K : Compacts Base} {τ : ℝ} {s : ℝ≥0}
    (c₀ : PolynomialSolveData emptyMetricPolynomial 0 G hG φ K τ s)
    (P : Fin 3 → Fin n → Expression) (ε : ℝ) {O : Set LowJet}
    (hO : IsOpen O) (hP : ∀ k j, (P k j).SmoothCoeffs O)
    (hGO : Set.MapsTo (lowJet G) c₀.U O) (D : ℕ → ℝ) (hD : ∀ m, 0 ≤ D m)
    (hpoly : ∀ m Z, supportedWeightedSeminorm
      (chartSupport c₀.e (modeSupport K) c₀.supportChart) s m
      (phaseChartPolynomialOperator hO c₀.openU P hP hG hGO K c₀.supportU
        c₀.smoothPhase τ ε c₀.e c₀.smoothForward c₀.smoothInverse c₀.supportChart Z) ≤
      ε / τ ^ tensorLoss P * D m * supportedWeightedSeminorm
        (chartSupport c₀.e (modeSupport K) c₀.supportChart) s (m + tensorOrder P) Z) :
…
```
Mentions: OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.JetPolynomial.Space, OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.PolynomialSolveData, OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.emptyMetricPolynomial, OAI.ClosedSurfaceR4.JetPolynomial.Expression, OAI.ClosedSurfaceR4.JetPolynomial.LowJet, OAI.ClosedSurfaceR4.JetPolynomial.lowJet, OAI.ClosedSurfaceR4.JetPolynomial.supportedWeightedSeminorm, OAI.ClosedSurfaceR4.JetPolynomial.chartSupport, OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.modeSupport, OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.phaseChartPolynomialOperator, OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.tensorLoss, OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.tensorOrder
theorem OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.uniform_perturbed_solver_transfer line 59