CoordinateLinearizedResidual.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Exact realization of the full perturbed linear residual in real fields.

def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.coordinateFullLinearized line 14
Source documentation
The actual metric derivative plus the actual polynomial derivative, written in the coordinates used by the finite solver.
```
def coordinateFullLinearized {n : ℕ} (P : Fin 3 → Fin n → Expression) (ε : ℝ)
    (G : Base → Space) (X : RealModes.RField 4) : 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.coordinateFullLinearized_residual line 19