ExplicitPeriodicFormula.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The polynomial expression evaluates to the explicit vector-valued periodic correction, including its covariance inverse and normalized integral.

lemma OAI.ClosedSurfaceR4.JetPolynomial.realCorrector_continuous line 17
lemma OAI.ClosedSurfaceR4.JetPolynomial.primitive_map line 26

theorem OAI.ClosedSurfaceR4.JetPolynomial.Expression.eval_angularCorrection line 42

Source documentation

The symbolic construction is exactly the span-plus-integrated-covariance formula, not just a formal expression with a similar order bound.

theorem eval_angularCorrection {O : Set LowJet} (hO : IsOpen O)
    {Y C X₀ : LowJet → E} {V : LowJet → C(Period, E)} {q : LowJet → ℝ}
    (hY : ContDiffOn ℝ ∞ Y O) (hC : ContDiffOn ℝ ∞ C O) (hX : ContDiffOn ℝ ∞ X₀ O)
    (hV : ContDiffOn ℝ ∞ (fun z : LowJet × ℝ => V z.1 (z.2 : Period)) (O ×ˢ Set.univ))
    (hd : ∀ Q ∈ O, gramDet (Y Q) (C Q) ≠ 0)
    (hq : ContDiffOn ℝ ∞ q O) (hqp : ∀ Q ∈ O, 0 < q Q)
    (hcircle : ∀ Q ∈ O, ∀ t, inner ℝ (V Q t) (V Q t) = q Q)
    (L : E →L[ℝ] ℝ) {h K e : Expression}
    (hh : h.SmoothCoeffs O) (hK : K.SmoothCoeffs O) (he : e.SmoothCoeffs O)
    (G : Base → Space) {p : Base} (hp : lowJet G p ∈ O) (t : ℝ) :
    (Expression.add (spanTerm Y C L h.primitive K)
      ((angularSource Y C X₀ V h K e).covariance V q L).primitive).eval G (p, t) =
…

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.spanTerm, OAI.ClosedSurfaceR4.JetPolynomial.Expression.angularSource, OAI.ClosedSurfaceR4.JetPolynomial.Expression.covariance, OAI.ClosedSurfaceR4.JetPolynomial.Expression.primitive, OAI.ClosedSurfaceR4.JetPolynomial.Expression.eval