OAI/Probability/InvariantIsing/Pressure/EntropyBudget.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Nonnegative entropy budgets for successive finite sampling steps.

  1. lemma OAI.InvariantIsing.entropy_budget_of_real line 14
  2. lemma OAI.InvariantIsing.entropy_budget_drop line 23
  3. lemma OAI.InvariantIsing.entropy_budget_map line 32
  4. lemma OAI.InvariantIsing.tilted_pair_entropy_budget_ennreal line 40