OAI/Analysis/HardSphere/Conditioning/Phase.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HardSphere.IsGroundVector.ae_killed_zero_propagation line 14
  2. def OAI.HardSphere.complexPhase line 56
  3. lemma OAI.HardSphere.complexPhase_eq_of_inner line 58
  4. lemma OAI.HardSphere.complexPhase_mul_norm line 71
  5. lemma OAI.HardSphere.norm_complexPhase line 76
  6. lemma OAI.HardSphere.inner_eq_of_complexPhase_eq line 80
  7. lemma OAI.HardSphere.measurable_complexPhase line 95
  8. lemma OAI.HardSphere.IsGroundVector.ae_killed_complexPhase line 97
  9. lemma OAI.HardSphere.IsGroundVector.phase_region line 112
  10. def OAI.HardSphere.groundPhaseRepresentative line 124
  11. lemma OAI.HardSphere.IsGroundVector.ae_phaseRepresentative line 127
  12. lemma OAI.HardSphere.IsGroundVector.phaseRepresentative_eq_on_connected line 132