OAI/Analysis/HardSphere/Geometry/TorusLiftBox.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HardSphere.torusLiftBox line 27
  2. lemma OAI.HardSphere.isCompact_torusLiftBox line 29
  3. lemma OAI.HardSphere.torusLiftBox_preserving line 33
  4. lemma OAI.HardSphere.integral_torusLiftBox line 44
  5. lemma OAI.HardSphere.SmoothMultiplier.smooth_fiberIntegral line 49
  6. def OAI.HardSphere.SmoothMultiplier.fiberMass line 68
  7. lemma OAI.HardSphere.SmoothMultiplier.smooth_fiberMass line 71
  8. def OAI.HardSphere.SmoothMultiplier.ofSmooth line 93
  9. def OAI.HardSphere.SmoothMultiplier.massRoot line 103
  10. def OAI.HardSphere.SmoothMultiplier.normalization line 108
  11. lemma OAI.HardSphere.SmoothMultiplier.normalization_real line 116
  12. lemma OAI.HardSphere.SmoothMultiplier.normalization_norm line 123
  13. lemma OAI.HardSphere.SmoothMultiplier.normalization_clearance line 132
  14. lemma OAI.HardSphere.integral_norm_add_sq_orthogonal line 141
  15. lemma OAI.HardSphere.SmoothMultiplier.fiber_derivative_mul_tail_le line 162