PolynomialTaylorBounds.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A fixed-power cubic remainder bound for the actual polynomial map.

theorem OAI.ClosedSurfaceR4.JetPolynomial.Expression.compact_taylorRemainder_bound line 15

Source documentation

The third variation controls the nonlinear remainder, with an exponent independent of the requested output derivative order.

theorem compact_taylorRemainder_bound {U : Set Base} {Q : Set LowJet}
    (hU : IsOpen U) (hQ : IsCompact Q) (e : Expression) (he : e.SmoothCoeffs Set.univ)
    (m : ℕ) (B : ℝ) (hB : 1 ≤ B) :
    ∃ D : ℝ, 0 ≤ D ∧ ∀ (G H : Base → Space) (s C : ℝ),
      0 < s → s ≤ 1 → 0 < C → ContDiff ℝ ∞ G → ContDiff ℝ ∞ H →
      (∀ t ∈ Set.Icc (0 : ℝ) 1, Set.MapsTo (lowJet (fun p => G p + t • H p)) U Q) →
      (∀ t ∈ Set.Icc (0 : ℝ) 1, WeightedBound U s (m + e.order) B
        (lowJet (fun p => G p + t • H p))) →
      WeightedBound U s (m + e.order) C H →
      ∀ θ ∈ Set.Icc (0 : ℝ) 1,
        WeightedBound U s m (D * C ^ 3 / s ^ (e.loss + 6) / 2) (e.taylorRemainder G H θ) := by
…

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