OAI/Probability/CriticalPercolation/Entropy/MarkedEntropy.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CriticalPercolation.FiniteEntropy.pushMass_comp line 14
  2. lemma OAI.CriticalPercolation.FiniteEntropy.sum_pushMass_pair line 23
  3. def OAI.CriticalPercolation.FiniteEntropy.conditionalMass line 33
  4. lemma OAI.CriticalPercolation.FiniteEntropy.conditionalMass_nonneg line 38
  5. lemma OAI.CriticalPercolation.FiniteEntropy.sum_conditionalMass_le_one line 43
  6. lemma OAI.CriticalPercolation.FiniteEntropy.conditionalMass_pos line 52
  7. lemma OAI.CriticalPercolation.FiniteEntropy.divergence_as_log line 57
  8. theorem OAI.CriticalPercolation.FiniteEntropy.conditional_marks_log line 73
  9. lemma OAI.CriticalPercolation.FiniteEntropy.divergence_pushMass_eq line 132
  10. lemma OAI.CriticalPercolation.FiniteEntropy.divergence_mark_chain line 137
  11. lemma OAI.CriticalPercolation.FiniteEntropy.conditional_cost_ge line 161
  12. theorem OAI.CriticalPercolation.FiniteEntropy.conditional_mark_cost_le line 248
  13. theorem OAI.CriticalPercolation.FiniteEntropy.active_contact_entropy_le line 311
  14. lemma OAI.CriticalPercolation.FiniteEntropy.pushMass_fst line 347
  15. theorem OAI.CriticalPercolation.FiniteEntropy.marginal_density_le line 353
  16. theorem OAI.CriticalPercolation.FiniteEntropy.entropy_exponential_domination line 360
  17. def OAI.CriticalPercolation.FiniteEntropy.logContactMass line 392
  18. lemma OAI.CriticalPercolation.FiniteEntropy.exp_logContactMass line 396
  19. lemma OAI.CriticalPercolation.FiniteEntropy.logContactMass_nonneg line 404
  20. theorem OAI.CriticalPercolation.FiniteEntropy.contact_configuration_entropy line 408
  21. lemma OAI.CriticalPercolation.FiniteEntropy.inactive_contact_log_le line 436
  22. theorem OAI.CriticalPercolation.FiniteEntropy.active_inverse_cost_le line 459