OAI/Probability/ContinuumTransition/Tetrahedron.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ContinuumTemperature.tetraRaw line 11
  2. lemma OAI.ContinuumTemperature.tetraRaw_zero line 14
  3. lemma OAI.ContinuumTemperature.tetraRaw_dist line 16
  4. def OAI.ContinuumTemperature.tetraVertex line 25
  5. lemma OAI.ContinuumTemperature.tetraVertex_zero line 28
  6. lemma OAI.ContinuumTemperature.tetraVertex_dist line 30
  7. lemma OAI.ContinuumTemperature.tetraVertex_norm line 36
  8. def OAI.ContinuumTemperature.clusterRadius line 43
  9. lemma OAI.ContinuumTemperature.clusterRadius_pos line 45
  10. def OAI.ContinuumTemperature.TetraCluster line 47
  11. lemma OAI.ContinuumTemperature.tetraCluster_free line 50
  12. lemma OAI.ContinuumTemperature.tetraCluster_norm_le line 71