OAI/Geometry/SurfaceImmersion/Correction/PolynomialInverseChartJets.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Quantitative derivatives of an inverse chart from its actual inverse Jacobian field. The finite-order budget is polynomial in the field's jets.

  1. def OAI.ClosedSurfaceR4.PhaseGeometry.inverseChartJetBudget line 15
  2. lemma OAI.ClosedSurfaceR4.PhaseGeometry.inverseChartJetBudget_one_le line 20
  3. lemma OAI.ClosedSurfaceR4.PhaseGeometry.inverseChartJetBudget_le_succ line 30
  4. lemma OAI.ClosedSurfaceR4.PhaseGeometry.inverseChartJetBudget_polynomial line 36
  5. theorem OAI.ClosedSurfaceR4.PhaseGeometry.inverse_chart_positive_jets line 46

    Source documentation

    The derivative equation is the ordinary inverse-function identity. No bound on the position of the inverse chart is needed for positive jets.

    theorem inverse_chart_positive_jets
    (e : OpenPartialHomeomorph Base Base)
    (hi : ContDiff ℝ ∞ e.symm) (J : Base → Base →L[ℝ] Base)
    (hJ : ContDiffOn ℝ ∞ J e.source)
    (heq : ∀ y ∈ e.target, fderiv ℝ e.symm y = J (e.symm y))
    {m : ℕ} {B : ℝ} (hB : 0 ≤ B)
    (hjets : ∀ k ≤ m, ∀ x ∈ e.source,
      ‖iteratedFDerivWithin ℝ k J e.source x‖ ≤ B) :
    ∀ j, 1 ≤ j → j ≤ m+1 → ∀ y ∈ e.target,
      ‖iteratedFDerivWithin ℝ j e.symm e.target y‖ ≤ inverseChartJetBudget (m+1) B := by
…

    Mentions: OAI.ClosedSurfaceR4.PhaseGeometry.inverseChartJetBudget