OAI/Probability/SKValue/Evolution/GridProfile.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKValue.gridProfile line 12
  2. lemma OAI.SKValue.gridProfile_time line 16
  3. lemma OAI.SKValue.gridProfile_mem line 22
  4. lemma OAI.SKValue.gridProfile_pairwise line 33
  5. lemma OAI.SKValue.gridProfile_sample line 46
  6. def OAI.SKValue.gridDelta line 82
  7. lemma OAI.SKValue.gridDelta_coe line 84
  8. def OAI.SKValue.OrderParameter.grid line 86
  9. lemma OAI.SKValue.OrderParameter.grid_time line 90
  10. lemma OAI.SKValue.OrderParameter.grid_mono line 95
  11. lemma OAI.SKValue.OrderParameter.grid_sample line 105
  12. lemma OAI.SKValue.OrderParameter.grid_le line 122