PolynomialVariationBounds.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The first three actual polynomial variations have one fixed scale exponent, the excess-jet loss plus six.

def OAI.ClosedSurfaceR4.JetPolynomial.Expression.variations line 17
lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.variations_smoothCoeffs line 22
lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.variations_order line 34
lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.variations_loss line 44
lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.first_variation_eval line 56

theorem OAI.ClosedSurfaceR4.JetPolynomial.Expression.compact_three_variation_bound line 70

Source documentation

The constant can depend on the requested output order; the exponent and finite input loss do not. All three direction maps have unit weighted norm.

theorem compact_three_variation_bound {U : Set Base} {O K : Set LowJet}
    (hU : IsOpen U) (hO : IsOpen O) (hK : IsCompact K) (hKO : K ⊆ O)
    (e : Expression) (he : e.SmoothCoeffs O) (m : ℕ) (B : ℝ) (hB : 1 ≤ B) :
    ∃ D : ℝ, 0 ≤ D ∧ ∀ (G : Fin 4 → Base → Space) (s : ℝ), 0 < s → s ≤ 1 →
      (∀ i, ContDiff ℝ ∞ (G i)) → Set.MapsTo (lowJet (G 0)) U K →
      WeightedBound U s (m + e.order) B (lowJet (G 0)) →
      (∀ i : Fin 3, WeightedBound U s (m + e.order) 1 (G i.succ)) →
      ∀ t ∈ Set.Icc (0 : ℝ) 1, ∀ i : Fin 3,
        WeightedBound U s m (D / s ^ (e.loss + 6))
          (fun p => (e.variations i).eval G (p, t)) := by
…

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