PolynomialMetricBounds.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Quantitative bounds for the actual finite pullback-metric tail.

theorem OAI.ClosedSurfaceR4.JetPolynomial.MetricPolynomial.compact_finite_metric_tail line 16

Source documentation

A single finite algebraic loss bounds the true metric remainder, at every weighted derivative order. This applies to each of xx, xy, and yy by choosing the two tangent coefficient sequences.

theorem compact_finite_metric_tail {S : TopologicalSpace.Opens Base} {O K : Set LowJet}
    (hO : IsOpen O) (hK : IsCompact K) (hKO : K ⊆ O)
    (X Y : ℕ → VectorExpression) (hXs : ∀ i, (X i).SmoothCoeffs O)
    (hYs : ∀ i, (Y i).SmoothCoeffs O) (L N : ℕ) (hN : 2 ≤ N)
    (hX : ∀ i ≤ L, ∀ a, (X i a).order ≤ N)
    (hY : ∀ i ≤ L, ∀ a, (Y i a).order ≤ N) (ℓ : Base →L[ℝ] ℝ) :
    ∃ d : ℕ, ∀ (m : ℕ) (B : ℝ), 1 ≤ B → ∃ D : ℝ, 0 ≤ D ∧
      ∀ (G : Base → Space) (s z : ℝ), 0 < z → z ≤ s → s ≤ 1 →
      ContDiff ℝ ∞ G → Set.MapsTo (lowJet G) S K →
      WeightedBound S s (m + N) B (lowJet G) →
      ∀ (A B : ℕ → Family S R4),
        (∀ i, VectorExpression.Represents G (X i) (A i)) →
…

Mentions: OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.JetPolynomial.LowJet, OAI.ClosedSurfaceR4.JetPolynomial.VectorExpression, OAI.ClosedSurfaceR4.JetPolynomial.Space, OAI.ClosedSurfaceR4.JetPolynomial.lowJet, OAI.ClosedSurfaceR4.JetPolynomial.R4, OAI.ClosedSurfaceR4.JetPolynomial.VectorExpression.Represents