OAI/Geometry/SurfaceImmersion/Correction/CoordinateLinearizedSupport.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The full linearized metric perturbation preserves the support of its varying field, including every higher-jet polynomial term.

  1. lemma OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.coordinateFullLinearized_zero_of_notMem line 12
  2. lemma OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.coordinateFullLinearized_tsupport line 32
  3. lemma OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.fullLinearized_residual_tsupport line 40