OAI/Probability/GaussianReplacement/Entropy.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CurrentProjection.joint_le_fst_prod_count line 14
  2. lemma OAI.CurrentProjection.joint_ac_fst_prod_count line 33
  3. lemma OAI.CurrentProjection.ae_positive_atom line 37
  4. lemma OAI.CurrentProjection.joint_ac_prod_marginals line 45
  5. lemma OAI.CurrentProjection.joint_le_prod_inverse_mass line 68
  6. lemma OAI.CurrentProjection.rnDeriv_le_of_le_withDensity line 102
  7. lemma OAI.CurrentProjection.klDiv_bound_of_llr_le line 113
  8. def OAI.CurrentProjection.shannonEntropy line 133

    Also declared: ComparatorChallenges/GaussianReplacement.lean:93 (same declaration text).

  9. lemma OAI.CurrentProjection.atom_surprisal_nonneg line 136
  10. lemma OAI.CurrentProjection.countable_information_le_entropy line 142
  11. lemma OAI.CurrentProjection.klDiv_map_equiv line 176
  12. def OAI.CurrentProjection.swapLast line 183

    Also declared: ComparatorChallenges/GaussianReplacement.lean:80 (same declaration text).

  13. lemma OAI.CurrentProjection.map_swapLast_prod line 192
  14. def OAI.CurrentProjection.rowInformation line 211

    Also declared: ComparatorChallenges/GaussianReplacement.lean:89 (same declaration text).

  15. lemma OAI.CurrentProjection.rowInformation_le_entropy line 215
  16. lemma OAI.CurrentProjection.rowInformation_refinement line 239
  17. def OAI.CurrentProjection.messagePosterior line 270
  18. instance OAI.CurrentProjection.messagePosterior_markov line 274
  19. lemma OAI.CurrentProjection.messagePosterior_apply line 280
  20. lemma OAI.CurrentProjection.messagePosterior_le line 294
  21. lemma OAI.CurrentProjection.messagePosterior_disintegrate line 305
  22. def OAI.CurrentProjection.refineSignal line 315
  23. instance OAI.CurrentProjection.refineSignal_finite line 319
  24. lemma OAI.CurrentProjection.refineSignal_apply line 324
  25. lemma OAI.CurrentProjection.refineSignal_mass line 340
  26. lemma OAI.CurrentProjection.refineSignal_positive_original line 353
  27. lemma OAI.CurrentProjection.messagePosterior_refinement line 365
  28. lemma OAI.CurrentProjection.countable_ac_of_atom line 389
  29. lemma OAI.CurrentProjection.rnDeriv_atom line 399
  30. lemma OAI.CurrentProjection.countable_entropy_le_crossEntropy line 410
  31. lemma OAI.CurrentProjection.shannonEntropy_map_le line 445
  32. lemma OAI.CurrentProjection.shannonEntropy_equiv line 462
  33. lemma OAI.CurrentProjection.geometric_pair_entropy line 470
  34. lemma OAI.CurrentProjection.entropy_finite_integrable line 535
  35. lemma OAI.CurrentProjection.integral_surprisal line 541
  36. lemma OAI.CurrentProjection.shannonEntropy_subadd line 547
  37. lemma OAI.CurrentProjection.intCode_le line 587
  38. def OAI.CurrentProjection.natIntEquivNatNat line 592
  39. lemma OAI.CurrentProjection.natInt_entropy line 597
  40. lemma OAI.CurrentProjection.map_fiber_ac_prod line 620
  41. lemma OAI.CurrentProjection.ae_condKernel_ac_of_joint_ac line 644
  42. lemma OAI.CurrentProjection.adjoin_countable_ac line 656
  43. lemma OAI.CurrentProjection.countable_null_transfer line 667
  44. lemma OAI.CurrentProjection.log_one_add_nonneg line 689
  45. lemma OAI.CurrentProjection.log_one_add_le line 692
  46. lemma OAI.CurrentProjection.measurable_log_one_add line 695
  47. lemma OAI.CurrentProjection.log_one_add_jensen line 699
  48. lemma OAI.CurrentProjection.exp_log_normalization line 737
  49. lemma OAI.CurrentProjection.mixed_entropy_log_bound line 747