OAI/Geometry/SurfaceImmersion/Atlas/ChartedPartitionLeading.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A supported phase family has leading tensor equal to the cutoff square times its input tensor. This is the local identity used by the global atlas.

  1. lemma OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.covectorSquare_directions line 15
  2. theorem OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.charted_cutoff_leading line 20
  3. theorem OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.charted_partition_leading line 46