OAI/Probability/ContinuumTransition/LatticeBounds.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ContinuumTemperature.cellIndex line 15
  2. theorem OAI.ContinuumTemperature.dist_lt_one_of_cellIndex_eq line 17
  3. abbrev OAI.ContinuumTemperature.Lattice line 39
  4. def OAI.ContinuumTemperature.cellRadius line 41
  5. def OAI.ContinuumTemperature.nearCells line 43
  6. theorem OAI.ContinuumTemperature.mem_nearCells_iff line 46
  7. theorem OAI.ContinuumTemperature.nearCells_symm line 52
  8. theorem OAI.ContinuumTemperature.cellRadius_nonneg line 56
  9. theorem OAI.ContinuumTemperature.cellRadius_le line 59
  10. theorem OAI.ContinuumTemperature.card_nearCells line 64
  11. theorem OAI.ContinuumTemperature.card_nearCells_le line 74
  12. theorem OAI.ContinuumTemperature.cellIndex_mem_nearCells line 85
  13. def OAI.ContinuumTemperature.latticeEnvelope line 106
  14. theorem OAI.ContinuumTemperature.latticeEnvelope_nonneg line 109
  15. theorem OAI.ContinuumTemperature.latticeEnvelope_symm line 114
  16. theorem OAI.ContinuumTemperature.latticeEnvelope_le line 118
  17. theorem OAI.ContinuumTemperature.sum_latticeEnvelope_le line 125
  18. theorem OAI.ContinuumTemperature.kernel_le_latticeEnvelope line 145
  19. def OAI.ContinuumTemperature.mixedEnvelope line 154
  20. theorem OAI.ContinuumTemperature.summable_mixedEnvelope_terms line 157
  21. theorem OAI.ContinuumTemperature.mixedEnvelope_nonneg line 169
  22. theorem OAI.ContinuumTemperature.mixedEnvelope_symm line 174
  23. theorem OAI.ContinuumTemperature.sum_mixedEnvelope_le line 181
  24. theorem OAI.ContinuumTemperature.attraction_le_mixedEnvelope line 202