OAI/Geometry/Immersion/ClosedSurface/GridBumps.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ClosedSurfaceR4.PhaseGrid.gridBump line 14
2. def OAI.ClosedSurfaceR4.PhaseGrid.center line 15
3. def OAI.ClosedSurfaceR4.PhaseGrid.cutoff line 16
4. lemma OAI.ClosedSurfaceR4.PhaseGrid.cutoff_smooth line 19
5. lemma OAI.ClosedSurfaceR4.PhaseGrid.cutoff_nonneg line 23
6. lemma OAI.ClosedSurfaceR4.PhaseGrid.cutoff_le_one line 25
7. lemma OAI.ClosedSurfaceR4.PhaseGrid.scaled_coordinate_lt line 28
8. lemma OAI.ClosedSurfaceR4.PhaseGrid.cutoff_support line 33
9. lemma OAI.ClosedSurfaceR4.PhaseGrid.cutoff_one_on_cell line 43
10. lemma OAI.ClosedSurfaceR4.PhaseGrid.cutoff_tsupport_subset line 53
11. theorem OAI.ClosedSurfaceR4.PhaseGrid.cutoff_derivative_bounds line 69
12. theorem OAI.ClosedSurfaceR4.PhaseGrid.cutoff_same_color_disjoint line 95