OAI/MathematicalPhysics/Boltzmann/Branching/ProductionDualLimit.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Bounded linear tests for the extended entropy production

  1. def OAI.BoltzmannNonuniqueness.productionDual line 17
  2. theorem OAI.BoltzmannNonuniqueness.productionDual_linear line 20
  3. theorem OAI.BoltzmannNonuniqueness.productionDual_ofReal_le line 25
  4. theorem OAI.BoltzmannNonuniqueness.productionDual_log_ratio line 43
  5. def OAI.BoltzmannNonuniqueness.rawProductionTest line 53
  6. def OAI.BoltzmannNonuniqueness.boundedProductionTest line 57
  7. theorem OAI.BoltzmannNonuniqueness.rawProductionTest_bound line 60
  8. theorem OAI.BoltzmannNonuniqueness.boundedProductionTest_bound line 65
  9. theorem OAI.BoltzmannNonuniqueness.productionDual_boundedTest_nonneg line 72
  10. theorem OAI.BoltzmannNonuniqueness.ofReal_productionDual_boundedTest line 79
  11. theorem OAI.BoltzmannNonuniqueness.productionDual_coefficient_bound line 89
  12. theorem OAI.BoltzmannNonuniqueness.measurable_productionDual line 104
  13. theorem OAI.BoltzmannNonuniqueness.measurable_rawProductionTest line 109
  14. theorem OAI.BoltzmannNonuniqueness.measurable_boundedProductionTest line 117
  15. theorem OAI.BoltzmannNonuniqueness.integrable_productionDual line 124
  16. theorem OAI.BoltzmannNonuniqueness.ofReal_productionDual_rawTest_tendsto line 149
  17. theorem OAI.BoltzmannNonuniqueness.ofReal_productionDual_boundedTest_tendsto line 188