OAI/Analysis/HardSphere/Operators/CompactFormCutoff.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HardSphere.CompactForm.cutoff line 11
2. lemma OAI.HardSphere.CompactForm.cutoff_smooth line 12
3. lemma OAI.HardSphere.CompactForm.cutoff_nonneg line 14
4. lemma OAI.HardSphere.CompactForm.cutoff_le_one line 15
5. lemma OAI.HardSphere.CompactForm.cutoff_zero line 16
6. lemma OAI.HardSphere.CompactForm.cutoff_one line 20
7. lemma OAI.HardSphere.CompactForm.cutoff_error line 24
8. lemma OAI.HardSphere.CompactForm.finite_range_compact line 38
9. lemma OAI.HardSphere.CompactForm.cutoff_compact line 43
10. lemma OAI.HardSphere.CompactForm.cutoff_embedding_error line 80
11. lemma OAI.HardSphere.CompactForm.compact_embedding line 135