OAI/Probability/RadialTransition/FinitePartition.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RadialTransition.isClosed_cube line 14
  2. theorem OAI.RadialTransition.measurableSet_cube line 22
  3. theorem OAI.RadialTransition.volume_cube line 25
  4. theorem OAI.RadialTransition.measurableSet_configurationCube line 34
  5. theorem OAI.RadialTransition.volume_configurationCube line 42
  6. theorem OAI.RadialTransition.continuous_energy line 51
  7. theorem OAI.RadialTransition.energy_abs_bound line 57
  8. theorem OAI.RadialTransition.integrableOn_boltzmann line 71
  9. theorem OAI.RadialTransition.partition_pos line 90
  10. theorem OAI.RadialTransition.log_integral_exp_convex_mix line 104
  11. theorem OAI.RadialTransition.integral_const_configurationCube line 134
  12. theorem OAI.RadialTransition.partition_zero line 140
  13. theorem OAI.RadialTransition.partition_nonneg line 148
  14. theorem OAI.RadialTransition.partition_upper_of_energy_lower line 152
  15. theorem OAI.RadialTransition.partition_stability_upper line 166
  16. theorem OAI.RadialTransition.log_partition_upper_of_energy_lower line 179
  17. theorem OAI.RadialTransition.boltzmannIntegral_pos line 196
  18. theorem OAI.RadialTransition.log_partition_convex_mix line 202
  19. def OAI.RadialTransition.finiteCanonical line 221
  20. theorem OAI.RadialTransition.finiteCanonical_concave line 224
  21. def OAI.RadialTransition.grandPartition line 236
  22. theorem OAI.RadialTransition.grandTerm_stability_upper line 239
  23. theorem OAI.RadialTransition.grandPartition_summable line 253
  24. theorem OAI.RadialTransition.grandPartition_bounds line 262
  25. theorem OAI.RadialTransition.log_tsum_convex_mix line 278
  26. def OAI.RadialTransition.cubeProbability line 311
  27. theorem OAI.RadialTransition.cubeProbability_isProbability line 314
  28. theorem OAI.RadialTransition.measure_pi_smul line 322
  29. theorem OAI.RadialTransition.cubeProbability_pi line 335
  30. theorem OAI.RadialTransition.measurePreserving_pair_eval line 349
  31. theorem OAI.RadialTransition.probability_pair_kernel_bound line 361
  32. theorem OAI.RadialTransition.probability_energy_upper line 381
  33. theorem OAI.RadialTransition.integral_cubeProbability_pi line 428
  34. theorem OAI.RadialTransition.log_partition_lower_of_energy_mean line 435