PerturbedMeanTransfer.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Transfer actual geometric mean data to a fixed polynomial perturbation. The cutoff, form, local geometry and reconstruction budgets stay the same. Only the polynomial profile and the required input-jet orders change.

lemma OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.empty_tensorOrder line 15
def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.ChartedMeanProfile.withPolynomial line 18
def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.ChartedMeanData.withPolynomial line 57
theorem OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.ChartedMeanProfile.Fits.withPolynomial line 94

theorem OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.uniform_perturbed_mean_transfer line 123

Source documentation

The perturbed mean profile is fixed before the map and scales. The existing mean datum supplies the same cutoff, form and geometric budgets.

theorem uniform_perturbed_mean_transfer {n : ℕ}
    (p₀ : ChartedMeanProfile emptyMetricPolynomial)
    (P : Fin 3 → Fin n → Expression) {O : Set LowJet} (hO : IsOpen O)
    (hP : ∀ k j, (P k j).SmoothCoeffs O) (hQO : p₀.Q ⊆ O)
    (K : Compacts Base) (hKU : (K : Set Base) ⊆ p₀.U)
    (e : OpenPartialHomeomorph SmallModes.Base SmallModes.Base)
    (he : ContDiffOn ℝ ∞ e e.source) (hi : ContDiffOn ℝ ∞ e.symm e.target)
    (hKe : (modeSupport K : Set SmallModes.Base) ⊆ e.source)
    (hebound : ∀ m j, 1 ≤ j → j ≤ m → ∀ x ∈ e.source,
      ‖iteratedFDerivWithin ℝ j e e.source x‖ ≤ p₀.J m)
    (hibound : ∀ m j, 1 ≤ j → j ≤ m + 1 → ∀ x ∈ e.target,
      ‖iteratedFDerivWithin ℝ j e.symm e.target x‖ ≤ p₀.inv (m + 1)) :
…

Mentions: OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.ChartedMeanProfile, OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.emptyMetricPolynomial, OAI.ClosedSurfaceR4.JetPolynomial.Expression, OAI.ClosedSurfaceR4.JetPolynomial.LowJet, OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.SmallModes.Base, OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.modeSupport