PolynomialCoefficientExtension.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Coefficients can be extended smoothly off the permitted compact low-jet set without changing the operator there or changing its jet order/loss.

def OAI.ClosedSurfaceR4.JetPolynomial.Expression.cutoffCoeffs line 14
lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.cutoffCoeffs_smooth line 17
lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.cutoffCoeffs_eval line 28
theorem OAI.ClosedSurfaceR4.JetPolynomial.Expression.exists_global_extension line 33
Source documentation
Only the compact set of low jets used by the application is retained.
```
theorem exists_global_extension {e : Expression} {O Q : Set LowJet}
    (hO : IsOpen O) (he : e.SmoothCoeffs O) (hQ : IsCompact Q) (hQO : Q ⊆ O) :
    ∃ e' : Expression, e'.SmoothCoeffs Set.univ ∧ e'.order = e.order ∧ e'.loss = e.loss ∧
      ∀ (G : Base → Space) (z : Base × ℝ), lowJet G z.1 ∈ Q → e'.eval G z = e.eval G z := by
…
```
Mentions: OAI.ClosedSurfaceR4.JetPolynomial.Expression, OAI.ClosedSurfaceR4.JetPolynomial.LowJet, OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.JetPolynomial.Space, OAI.ClosedSurfaceR4.JetPolynomial.lowJet