OAI/Geometry/Relativity/CKS/CollarCutoffs.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CKSBending.roundingWeight line 11
2. lemma OAI.CKSBending.roundingWeight_smooth line 12
3. lemma OAI.CKSBending.roundingWeight_nonneg line 15
4. lemma OAI.CKSBending.roundingWeight_le_one line 16
5. lemma OAI.CKSBending.roundingWeight_zero line 17
6. lemma OAI.CKSBending.roundingWeight_one line 21
7. lemma OAI.CKSBending.roundingWeight_le_paddingWeight line 25
8. lemma OAI.CKSBending.roundingWeight_deriv_initial line 28
9. lemma OAI.CKSBending.roundingWeight_deriv line 36
10. theorem OAI.CKSBending.roundingWeight_weighted_deriv line 46