OAI/Geometry/SurfaceImmersion/Atlas/GridSupportedCutoffs.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The actual normalized grid cutoffs multiplied by a supported chart weight. The derivative constant is independent of the number of cells.

  1. lemma OAI.ClosedSurfaceR4.WeightedEstimates.WeightedBound.to_unit_scale line 14
  2. def OAI.ClosedSurfaceR4.PhaseGrid.supportedNormalizedCutoff line 28
  3. lemma OAI.ClosedSurfaceR4.PhaseGrid.supportedNormalizedCutoff_apply line 40
  4. theorem OAI.ClosedSurfaceR4.PhaseGrid.supported_normalized_cutoff_bounds line 45