JetPolynomialCovariance.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The actual covariance inversion preserves finite polynomial dependence on higher jets. Its inverse matrix depends only on the low-jet geometric data.

def OAI.ClosedSurfaceR4.JetPolynomial.Expression.covariance line 17
lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.smoothCoeffs_covariance line 21
lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.order_covariance line 33
lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.loss_covariance line 38
lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.eval_covariance line 43
theorem OAI.ClosedSurfaceR4.JetPolynomial.Expression.eval_covariance_periodic line 58
Source documentation
Each component of the covariance corrector used in the finite periodic recursion has an actual polynomial representation with the same order and loss.
```
theorem eval_covariance_periodic {O : Set LowJet} (hO : IsOpen O)
    (V : LowJet → C(Period, E)) (q : LowJet → ℝ) (L : E →L[ℝ] ℝ)
    {e : Expression} (he : e.SmoothCoeffs O) (G : Base → Space)
    (r : Base → C(Period, ℝ)) {p : Base} (hp : lowJet G p ∈ O)
    (hr : ∀ s : ℝ, e.eval G (p, s) = r p (s : Period)) (t : ℝ) :
    (e.covariance V q L).eval G (p, t) =
      L (parameterCorrector (fun x => V (lowJet G x)) r (fun x => q (lowJet G x))
        p (t : Period)) := by
…
```
Mentions: OAI.ClosedSurfaceR4.JetPolynomial.LowJet, OAI.ClosedSurfaceR4.JetPolynomial.Expression, OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.JetPolynomial.Space, OAI.ClosedSurfaceR4.JetPolynomial.lowJet, OAI.ClosedSurfaceR4.JetPolynomial.Expression.eval