OAI/Probability/ContinuumTransition/GibbsQuadratic.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ContinuumTemperature.gibbsEnergy_const line 11
  2. theorem OAI.ContinuumTemperature.gibbsEnergy_congr line 17
  3. theorem OAI.ContinuumTemperature.gibbsFamily_shift line 28
  4. theorem OAI.ContinuumTemperature.familyTerm_shift line 38
  5. theorem OAI.ContinuumTemperature.integrableOn_gibbs_of_lower line 46
  6. def OAI.ContinuumTemperature.quadraticBlock line 67
  7. theorem OAI.ContinuumTemperature.measurable_quadraticBlock line 70
  8. theorem OAI.ContinuumTemperature.quadraticBlock_symm line 74
  9. theorem OAI.ContinuumTemperature.quadraticBlock_on line 81
  10. theorem OAI.ContinuumTemperature.quadraticBlock_cross line 88
  11. theorem OAI.ContinuumTemperature.familyTerm_quadraticBlock line 95