OAI/Probability/ContinuumTransition/TrialConfigurations.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ContinuumTemperature.gridPoint line 14
  2. def OAI.ContinuumTemperature.trialBall line 17
  3. theorem OAI.ContinuumTemperature.trialBall_coord line 19
  4. theorem OAI.ContinuumTemperature.trialBall_separation line 28
  5. theorem OAI.ContinuumTemperature.trialBall_disjoint line 46
  6. def OAI.ContinuumTemperature.gridRadius line 55
  7. def OAI.ContinuumTemperature.gridNeighbors line 57
  8. theorem OAI.ContinuumTemperature.mem_gridNeighbors_iff line 60
  9. theorem OAI.ContinuumTemperature.trialBall_close_mem line 65
  10. theorem OAI.ContinuumTemperature.gridRadius_nonneg line 85
  11. theorem OAI.ContinuumTemperature.card_gridNeighbors line 88
  12. theorem OAI.ContinuumTemperature.grid_close_card_le line 96
  13. def OAI.ContinuumTemperature.trialEnergyConstant line 108
  14. theorem OAI.ContinuumTemperature.trialEnergyConstant_nonneg line 112
  15. theorem OAI.ContinuumTemperature.trial_core_row_le line 116
  16. def OAI.ContinuumTemperature.interiorGrid line 147
  17. theorem OAI.ContinuumTemperature.interiorGrid_ball_subset line 151
  18. theorem OAI.ContinuumTemperature.card_interiorGrid line 171
  19. theorem OAI.ContinuumTemperature.card_interiorGrid_lower line 178
  20. theorem OAI.ContinuumTemperature.exists_trial_sites line 190
  21. def OAI.ContinuumTemperature.trialVolume line 207
  22. theorem OAI.ContinuumTemperature.trialVolume_pos line 209
  23. theorem OAI.ContinuumTemperature.real_volume_trialBall line 213
  24. theorem OAI.ContinuumTemperature.symmetricWeight_grid_lower line 220
  25. theorem OAI.ContinuumTemperature.partition_grid_lower line 255
  26. theorem OAI.ContinuumTemperature.partition_trial_lower line 288