JetPolynomialFullEvaluation.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Identification of the complete polynomial expression with the same explicit solution supplied by the full periodic system theorem.

theorem OAI.ClosedSurfaceR4.JetPolynomial.Expression.eval_fullComponent line 19

Source documentation

Polynomial forcing produces the explicit full corrector. The derivative in the transverse datum is the actual derivative of the forcing primitive.

theorem eval_fullComponent {O : Set LowJet} {S : Set Base} (hO : IsOpen O) (hS : IsOpen S)
    {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[ℝ] ℝ) (v : Fin 2) {h j e : Expression}
    (hh : h.SmoothCoeffs O) (hj : j.SmoothCoeffs O) (he : e.SmoothCoeffs O)
    {G : Base → Space} (hG : ContDiff ℝ ∞ G) (hQ : Set.MapsTo (lowJet G) S O)
    (hf jf ef : Base → C(Period, ℝ))
    (hhr : ∀ p ∈ S, ∀ t : ℝ, h.eval G (p, t) = hf p (t : Period))
…

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