OAI/Analysis/HardSphere/Conditioning/PhaseTransfer.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HardSphere.Phase.HasCommonPhase line 18
  2. lemma OAI.HardSphere.Phase.norm_setIntegral_of_commonPhase line 21
  3. lemma OAI.HardSphere.Phase.slice_phase_loss line 29
  4. lemma OAI.HardSphere.Phase.integral_mul_le_sqrt line 50
  5. lemma OAI.HardSphere.Phase.integral_norm_sq_le line 58
  6. lemma OAI.HardSphere.Phase.memLp_slices line 76
  7. lemma OAI.HardSphere.Phase.memLp_integral_norm line 82
  8. lemma OAI.HardSphere.Phase.setIntegral_norm_sq_le line 93
  9. def OAI.HardSphere.Phase.occupation line 102
  10. def OAI.HardSphere.Phase.modulusOccupation line 105
  11. def OAI.HardSphere.Phase.geometricLoss line 108
  12. theorem OAI.HardSphere.Phase.phase_transfer line 112