OAI/Geometry/Immersion/ClosedSurface/GridPartition.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ClosedSurfaceR4.PhaseGrid.cutoff_weighted_bounds line 15
2. lemma OAI.ClosedSurfaceR4.PhaseGrid.weighted_sum_bounded_overlap line 36
3. def OAI.ClosedSurfaceR4.PhaseGrid.squareSum line 69
4. def OAI.ClosedSurfaceR4.PhaseGrid.normalizedCutoff line 72
5. lemma OAI.ClosedSurfaceR4.PhaseGrid.squareSum_smooth line 75
6. lemma OAI.ClosedSurfaceR4.PhaseGrid.squareSum_nonneg line 78
7. lemma OAI.ClosedSurfaceR4.PhaseGrid.squareSum_ge_one line 81
8. lemma OAI.ClosedSurfaceR4.PhaseGrid.normalizedCutoff_tsupport line 87
9. lemma OAI.ClosedSurfaceR4.PhaseGrid.normalizedCutoff_squares line 93
10. lemma OAI.ClosedSurfaceR4.PhaseGrid.squareSum_weighted_bounds line 100
11. lemma OAI.ClosedSurfaceR4.PhaseGrid.inverse_sqrt_smooth line 125
12. lemma OAI.ClosedSurfaceR4.PhaseGrid.normalizedCutoff_smooth line 130
13. theorem OAI.ClosedSurfaceR4.PhaseGrid.normalizedCutoff_weighted_bounds line 142
14. theorem OAI.ClosedSurfaceR4.PhaseGrid.normalizedCutoff_polynomial_derivatives line 187