OAI/Probability/DirectionalWalk/Entropy.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalZeroOne.atomInfo line 12
  2. def OAI.DirectionalZeroOne.discreteEntropy line 15
  3. lemma OAI.DirectionalZeroOne.atomInfo_nonneg line 18
  4. lemma OAI.DirectionalZeroOne.discreteEntropy_nonneg line 22
  5. lemma OAI.DirectionalZeroOne.ae_atom_real_pos line 26
  6. lemma OAI.DirectionalZeroOne.summable_integral_ratio line 31
  7. lemma OAI.DirectionalZeroOne.integrable_atom_ratio line 42
  8. lemma OAI.DirectionalZeroOne.integral_atom_ratio_le line 49
  9. lemma OAI.DirectionalZeroOne.atomInfo_le_comparison line 59
  10. lemma OAI.DirectionalZeroOne.integrable_atomInfo_of_comparison line 70
  11. lemma OAI.DirectionalZeroOne.discreteEntropy_le_comparison line 81
  12. lemma OAI.DirectionalZeroOne.rnDeriv_atom line 99
  13. lemma OAI.DirectionalZeroOne.llr_atom line 106
  14. lemma OAI.DirectionalZeroOne.absolutelyContinuous_of_atoms line 115
  15. lemma OAI.DirectionalZeroOne.atom_logRatio_nonneg line 123
  16. lemma OAI.DirectionalZeroOne.atom_klDiv_formula line 133
  17. def OAI.DirectionalZeroOne.conditionalInfo line 143
  18. def OAI.DirectionalZeroOne.conditionalEntropy line 147
  19. lemma OAI.DirectionalZeroOne.atom_le_fst line 150
  20. lemma OAI.DirectionalZeroOne.conditionalInfo_nonneg line 156
  21. lemma OAI.DirectionalZeroOne.conditionalInfo_log line 166
  22. lemma OAI.DirectionalZeroOne.compProd_atom line 176
  23. lemma OAI.DirectionalZeroOne.integrable_conditionalInfo line 184
  24. lemma OAI.DirectionalZeroOne.conditionalEntropy_le_crossEntropy line 207
  25. lemma OAI.DirectionalZeroOne.joint_ac_marginal_product line 228
  26. lemma OAI.DirectionalZeroOne.conditionalEntropy_le_entropy_snd line 243