OAI/Analysis/HardSphere/Geometry/PartitionErrorIntegral.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HardSphere.SmoothMultiplier.partition_error_integral line 25
  2. theorem OAI.HardSphere.productPartition_ims line 43
  3. lemma OAI.HardSphere.productPartition_norm_partition line 58
  4. lemma OAI.HardSphere.binary_product_membership line 65
  5. lemma OAI.HardSphere.productPartition_selected_probability line 75
  6. theorem OAI.HardSphere.productPartition_removal_cost line 88
  7. def OAI.HardSphere.selectedEnergy line 114
  8. lemma OAI.HardSphere.continuous_selectedEnergy line 117
  9. def OAI.HardSphere.selectedAllEquiv line 122
  10. lemma OAI.HardSphere.selectedEnergy_all line 125
  11. def OAI.HardSphere.selectedDeleteEquiv line 130
  12. lemma OAI.HardSphere.SmoothTest.selected_slice_integrable line 143
  13. lemma OAI.HardSphere.SmoothTest.integral_selected_slice line 148
  14. theorem OAI.HardSphere.selected_rayleigh line 159
  15. theorem OAI.HardSphere.selected_ground_removal line 192