OAI/Analysis/HardSphere/Geometry/ScalarPartitionIms.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HardSphere.scalar_partition_ims line 35
2. lemma OAI.HardSphere.real_norm_sq line 52
3. lemma OAI.HardSphere.SmoothMultiplier.partition_derivative line 56
4. lemma OAI.HardSphere.SmoothMultiplier.partition_norm line 77
5. lemma OAI.HardSphere.SmoothMultiplier.partition_scalar_norm line 84
6. lemma OAI.HardSphere.SmoothMultiplier.partition_direction_ims line 98
7. theorem OAI.HardSphere.SmoothMultiplier.partition_ims line 124
8. def OAI.HardSphere.productPartition line 142
9. lemma OAI.HardSphere.productPartition_apply line 146
10. lemma OAI.HardSphere.productPartition_real line 150
11. lemma OAI.HardSphere.productPartition_unity line 159
12. lemma OAI.HardSphere.productPartition_partial line 168
13. lemma OAI.HardSphere.binary_product_sum line 183
14. lemma OAI.HardSphere.productPartition_gradient_partition line 203