OAI/Probability/CriticalPercolation/Entropy/Divergence.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CriticalPercolation.FiniteEntropy.divergence line 16
  2. lemma OAI.CriticalPercolation.FiniteEntropy.mul_log_div_ge_sub line 19
  3. lemma OAI.CriticalPercolation.FiniteEntropy.mass_sub_le_divergence line 33
  4. lemma OAI.CriticalPercolation.FiniteEntropy.divergence_nonneg line 39
  5. lemma OAI.CriticalPercolation.FiniteEntropy.normalizer_pos line 44
  6. theorem OAI.CriticalPercolation.FiniteEntropy.entropy_inequality line 55
  7. def OAI.CriticalPercolation.FiniteEntropy.binaryDivergence line 92
  8. lemma OAI.CriticalPercolation.FiniteEntropy.mul_log_div_le line 95
  9. theorem OAI.CriticalPercolation.FiniteEntropy.binaryDivergence_upper line 101
  10. lemma OAI.CriticalPercolation.FiniteEntropy.mul_log_div_eq line 111
  11. def OAI.CriticalPercolation.FiniteEntropy.binaryRemainder line 118
  12. lemma OAI.CriticalPercolation.FiniteEntropy.continuous_binaryRemainder line 122
  13. lemma OAI.CriticalPercolation.FiniteEntropy.binaryRemainder_eq line 126
  14. lemma OAI.CriticalPercolation.FiniteEntropy.hasDerivAt_binaryRemainder line 132
  15. lemma OAI.CriticalPercolation.FiniteEntropy.hasDerivAt_binaryRemainder_deriv line 144
  16. lemma OAI.CriticalPercolation.FiniteEntropy.binary_second_deriv_nonneg line 155
  17. lemma OAI.CriticalPercolation.FiniteEntropy.convexOn_binaryRemainder line 164
  18. theorem OAI.CriticalPercolation.FiniteEntropy.binaryDivergence_lower line 179