OAI/Probability/ContinuumTransition/MomentEnergy.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ContinuumTemperature.latticeCell line 11
  2. theorem OAI.ContinuumTemperature.measurable_cellIndex line 13
  3. theorem OAI.ContinuumTemperature.measurableSet_latticeCell line 18
  4. theorem OAI.ContinuumTemperature.gibbsEnergy_eq_pairSum line 21
  5. theorem OAI.ContinuumTemperature.gibbsEnergy_sub line 35
  6. theorem OAI.ContinuumTemperature.gibbsEnergy_nonneg line 44
  7. theorem OAI.ContinuumTemperature.gibbsEnergy_le_card_sq line 57
  8. theorem OAI.ContinuumTemperature.core_gibbsEnergy_one_cell line 73
  9. theorem OAI.ContinuumTemperature.physical_gibbs_moment_energy line 83