OAI/Combinatorics/RamseyFive/Entropy/FiniteKernels.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpRamseyFive.FiniteEntropy.sigmaLaw line 14
  2. lemma OAI.SharpRamseyFive.FiniteEntropy.mean_sigma line 20
  3. lemma OAI.SharpRamseyFive.FiniteEntropy.map_adaptive_first line 25
  4. lemma OAI.SharpRamseyFive.FiniteEntropy.second_adaptive line 33
  5. lemma OAI.SharpRamseyFive.FiniteEntropy.fiber_adaptive line 36
  6. lemma OAI.SharpRamseyFive.FiniteEntropy.adaptive_stream line 49
  7. lemma OAI.SharpRamseyFive.FiniteEntropy.Law.ext_mean line 54
  8. lemma OAI.SharpRamseyFive.FiniteEntropy.adaptive_reconstruct line 60
  9. lemma OAI.SharpRamseyFive.FiniteEntropy.map_adaptive_source line 66
  10. def OAI.SharpRamseyFive.FiniteEntropy.liftObserved line 73
  11. lemma OAI.SharpRamseyFive.FiniteEntropy.liftObserved_original line 76
  12. lemma OAI.SharpRamseyFive.FiniteEntropy.liftObserved_joint line 79
  13. lemma OAI.SharpRamseyFive.FiniteEntropy.liftObserved_stream line 84
  14. def OAI.SharpRamseyFive.FiniteEntropy.BlockHistory line 95
  15. instance OAI.SharpRamseyFive.FiniteEntropy.blockHistoryFintype line 99
  16. def OAI.SharpRamseyFive.FiniteEntropy.historyPosterior line 106
  17. def OAI.SharpRamseyFive.FiniteEntropy.historyUnused line 111
  18. def OAI.SharpRamseyFive.FiniteEntropy.historyLaw line 115
  19. theorem OAI.SharpRamseyFive.FiniteEntropy.history_posterior_mean line 122
  20. def OAI.SharpRamseyFive.FiniteEntropy.historyTupleLaw line 147
  21. lemma OAI.SharpRamseyFive.FiniteEntropy.historyTuple_second line 151
  22. lemma OAI.SharpRamseyFive.FiniteEntropy.historyTuple_fiber line 157
  23. theorem OAI.SharpRamseyFive.FiniteEntropy.history_round_mean line 162
  24. lemma OAI.SharpRamseyFive.FiniteEntropy.blockRoundMean_total_irrel line 188
  25. theorem OAI.SharpRamseyFive.FiniteEntropy.history_pre_round line 215