OAI/Probability/RadialTransition/LatticeStability.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.RadialTransition.Cell line 14
  2. def OAI.RadialTransition.cellOf line 16
  3. def OAI.RadialTransition.cellMargin line 18
  4. def OAI.RadialTransition.CellReach line 20
  5. instance OAI.RadialTransition.(instance at line 22) line 22
  6. def OAI.RadialTransition.rangeCells line 24
  7. theorem OAI.RadialTransition.mem_rangeCells line 27
  8. theorem OAI.RadialTransition.cellReach_symm line 31
  9. theorem OAI.RadialTransition.cellMargin_nonneg line 35
  10. theorem OAI.RadialTransition.card_rangeCells line 40
  11. theorem OAI.RadialTransition.cellReach_of_dist line 64
  12. def OAI.RadialTransition.cellMajorant line 81
  13. theorem OAI.RadialTransition.cellMajorant_nonneg line 84
  14. theorem OAI.RadialTransition.cellMajorant_symm line 88
  15. theorem OAI.RadialTransition.cellMajorant_row line 96
  16. theorem OAI.RadialTransition.same_cell_diameter line 117
  17. theorem OAI.RadialTransition.scaledBumpProfile_le_cellMajorant line 138
  18. def OAI.RadialTransition.familyCellMajorant line 148
  19. theorem OAI.RadialTransition.summable_cellMajorant line 151
  20. theorem OAI.RadialTransition.familyCellMajorant_nonneg line 166
  21. theorem OAI.RadialTransition.familyCellMajorant_symm line 174
  22. theorem OAI.RadialTransition.familyCellMajorant_row line 182
  23. theorem OAI.RadialTransition.attraction_le_familyCellMajorant line 205
  24. theorem OAI.RadialTransition.family_energy_cell_bound line 213
  25. theorem OAI.RadialTransition.stable_familyPotential line 232
  26. theorem OAI.RadialTransition.decay_familyPotential line 248
  27. def OAI.RadialTransition.cubeCells line 282
  28. theorem OAI.RadialTransition.cellOf_mem_cubeCells line 285
  29. theorem OAI.RadialTransition.card_cubeCells line 291
  30. theorem OAI.RadialTransition.square_count_le_card_occupation line 308
  31. theorem OAI.RadialTransition.family_density_stability line 313