PolynomialPerturbationBounds.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Finite polynomial perturbations have one fixed short-scale exponent.

def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.order line 14
def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.loss line 15
def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.conjugated line 17
lemma OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.conjugatedVariation_smooth line 21

theorem OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.compact_conjugated_bound line 36

Source documentation

The perturbation parameter enters linearly in the bound, and the single short-scale loss works at every requested output order.

theorem compact_conjugated_bound {U : Set Base} {O K : Set LowJet}
    (hU : IsOpen U) (hO : IsOpen O) (hK : IsCompact K) (hKO : K ⊆ O)
    (P : Fin n → Expression) (hP : ∀ l, (P l).SmoothCoeffs O)
    (m : ℕ) (B Q : ℝ) (hB : 1 ≤ B) (hQ : 0 ≤ Q) :
    ∃ D : ℝ, 0 ≤ D ∧ ∀ (G : Base → Space) (φ : Fin 3 → Base → ℝ)
      (H : DirectionFields) (s τ ε : ℝ) (C : Fin 3 → ℝ),
      0 < τ → 0 < s → τ ≤ s → s ≤ 1 → 0 ≤ ε → ε ≤ 1 → (∀ j, 0 < C j) →
      ContDiff ℝ ∞ G → (∀ j, ContDiff ℝ ∞ (φ j)) → (∀ j, ContDiff ℝ ∞ (H j)) →
      Set.MapsTo (lowJet G) U K → WeightedBound U s (m + order P) B (lowJet G) →
      (∀ j, WeightedBound U s (m + order P) (C j) (H j)) →
      (∀ j v, WeightedBound U s (m + order P) Q
        (fun p => fderiv ℝ (φ j) p (coordinateVector v))) →
…

Mentions: OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.JetPolynomial.LowJet, OAI.ClosedSurfaceR4.JetPolynomial.Expression, OAI.ClosedSurfaceR4.JetPolynomial.Space, OAI.ClosedSurfaceR4.JetPolynomial.lowJet, OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.order, OAI.ClosedSurfaceR4.JetPolynomial.coordinateVector