OAI/Geometry/SurfaceImmersion/Correction/GridMeanReconstruction.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The leading tensor of all cell phases is exactly the original chart weight squared times the input tensor. No cardinality-dependent loss occurs.

  1. lemma OAI.ClosedSurfaceR4.PhaseGrid.supportedCellCutoff_square_sum line 14
  2. theorem OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.charted_grid_partition_leading line 37