CoordinatePolynomialRealization.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The coordinate operator used in the finite parametrix really is the linearization of the polynomial perturbation on real oscillatory fields.

def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.coordinateRealLinearized line 15
Source documentation
Polynomial first variation in the product coordinates of the metric solver.
```
def coordinateRealLinearized {n : ℕ} (P : Fin 3 → Fin n → Expression) (ε : ℝ)
    (G : Base → Space) (X : RealModes.RField 4) (t : ℝ) : SmallModes.Base → Fin 3 → ℝ :=
…
```
Mentions: OAI.ClosedSurfaceR4.JetPolynomial.Expression, OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.JetPolynomial.Space, OAI.ClosedSurfaceR4.RealModes.RField, OAI.ClosedSurfaceR4.SmallModes.Base
lemma OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.coordinatePolynomialOperator_realization line 19