OAI/Probability/GaussianReplacement/Information.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CurrentProjection.klDiv_prod_chain line 13
  2. lemma OAI.CurrentProjection.mutualInformation_reference line 21
  3. lemma OAI.CurrentProjection.klDiv_map_leftInverse line 28
  4. lemma OAI.CurrentProjection.mutualInformation_map_left line 38
  5. lemma OAI.CurrentProjection.mutualInformation_swap line 57
  6. lemma OAI.CurrentProjection.mutualInformation_rows_chain line 68
  7. lemma OAI.CurrentProjection.mutualInformation_independent_rows line 89
  8. lemma OAI.CurrentProjection.mutualInformation_reference_comparison line 108
  9. lemma OAI.CurrentProjection.density_mutualInformation_comparison line 143
  10. def OAI.CurrentProjection.observedMessageMap line 207
  11. lemma OAI.CurrentProjection.measurable_observedMessageMap line 210
  12. def OAI.CurrentProjection.observedMessage line 214
  13. instance OAI.CurrentProjection.observedMessage_probability line 218
  14. lemma OAI.CurrentProjection.observedMessage_snd line 224
  15. lemma OAI.CurrentProjection.exposedInformation_chain line 231
  16. lemma OAI.CurrentProjection.observedMessage_fst_of_independence line 260
  17. lemma OAI.CurrentProjection.prod_posterior_map line 279
  18. lemma OAI.CurrentProjection.swapped_compProd_withDensity line 309
  19. def OAI.CurrentProjection.posteriorProjectionKernel line 327
  20. lemma OAI.CurrentProjection.measurable_posteriorProjectionMap line 333
  21. instance OAI.CurrentProjection.posteriorProjectionKernel_markov line 337
  22. lemma OAI.CurrentProjection.posteriorProjectionKernel_apply line 342
  23. lemma OAI.CurrentProjection.observedMessage_independent_disintegrate line 351
  24. lemma OAI.CurrentProjection.observedMessage_independent_density line 357
  25. lemma OAI.CurrentProjection.criticalPosterior_probability line 374
  26. lemma OAI.CurrentProjection.criticalPosterior_ae_class line 382
  27. lemma OAI.CurrentProjection.criticalPosterior_cover_entropy line 387
  28. lemma OAI.CurrentProjection.projection_positive_reference line 418
  29. lemma OAI.CurrentProjection.independent_rows_signal line 439
  30. lemma OAI.CurrentProjection.swapLast_snd line 448
  31. lemma OAI.CurrentProjection.exposedInformation_density_comparison line 456