OAI/Analysis/HardSphere/Density/DensityLinearity.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HardSphere.Density.Operator.compression_summable line 13
  2. lemma OAI.HardSphere.Density.Operator.compressionTrace_linear line 22
  3. lemma OAI.HardSphere.Density.rankOne_diagonal line 32
  4. def OAI.HardSphere.Density.pure line 38
  5. lemma OAI.HardSphere.Density.pure_compression line 44
  6. lemma OAI.HardSphere.Density.projection_diagonal line 62
  7. lemma OAI.HardSphere.Density.projection_trace line 68
  8. def OAI.HardSphere.Density.normalizedProjection line 78
  9. lemma OAI.HardSphere.Density.normalizedProjection_support line 86