PolynomialJetRecursion.lean`

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Finite jet-order induction for the explicit periodic correction recursion.

def OAI.ClosedSurfaceR4.JetPolynomial.MetricPolynomial.longitudinal line 13
Source documentation
Low-jet longitudinal vector, including the velocity loop.
```
def longitudinal (X₀ : LowJet → R4) (V : LowJet → C(CovarianceCorrector.Period, R4)) :
    VectorExpression := fun a => .coeff (fun z => (X₀ z.1 + V z.1 (z.2 : CovarianceCorrector.Period)) a)
```
Mentions: OAI.ClosedSurfaceR4.JetPolynomial.LowJet, OAI.ClosedSurfaceR4.JetPolynomial.R4, OAI.ClosedSurfaceR4.CovarianceCorrector.Period, OAI.ClosedSurfaceR4.JetPolynomial.VectorExpression
def OAI.ClosedSurfaceR4.JetPolynomial.MetricPolynomial.transverse line 16
def OAI.ClosedSurfaceR4.JetPolynomial.MetricPolynomial.initial line 18
def OAI.ClosedSurfaceR4.JetPolynomial.MetricPolynomial.step line 22
Source documentation
All forcing expressions are formed before the full correction is applied.
```
def step (Y C X₀ : LowJet → R4) (V : LowJet → C(CovarianceCorrector.Period, R4))
    (q : LowJet → ℝ) (dx dy : Fin 2) (U : ℕ → VectorExpression) (r : ℕ) : VectorExpression :=
…
```
Mentions: OAI.ClosedSurfaceR4.JetPolynomial.LowJet, OAI.ClosedSurfaceR4.JetPolynomial.R4, OAI.ClosedSurfaceR4.CovarianceCorrector.Period, OAI.ClosedSurfaceR4.JetPolynomial.VectorExpression
def OAI.ClosedSurfaceR4.JetPolynomial.MetricPolynomial.coefficients line 29
lemma OAI.ClosedSurfaceR4.JetPolynomial.MetricPolynomial.order_step line 35
theorem OAI.ClosedSurfaceR4.JetPolynomial.MetricPolynomial.coefficients_order line 55
Source documentation
The expression for U_(i+1) uses jets of the base map through order 2i+2, independently of how much further the finite recursion is continued.
```
theorem coefficients_order (Y C X₀ : LowJet → R4)
    (V : LowJet → C(CovarianceCorrector.Period, R4)) (q : LowJet → ℝ)
    (dx dy : Fin 2) (n i : ℕ) (a : Fin 4) :
    (coefficients Y C X₀ V q dx dy n i a).order ≤ 2 * i + 2 := by
…
```
Mentions: OAI.ClosedSurfaceR4.JetPolynomial.LowJet, OAI.ClosedSurfaceR4.JetPolynomial.R4, OAI.ClosedSurfaceR4.CovarianceCorrector.Period, OAI.ClosedSurfaceR4.JetPolynomial.MetricPolynomial.coefficients