OAI/MeasureTheory/SelfSimilar/Conditioning.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.EntropyRateDimension.FairPairs.Law.ofObservable line 11
  2. theorem OAI.EntropyRateDimension.FairPairs.Law.ofObservable_support line 21
  3. theorem OAI.EntropyRateDimension.FairPairs.Law.ofObservable_prob line 25
  4. theorem OAI.EntropyRateDimension.FairPairs.Law.ofObservable_entropy line 29
  5. theorem OAI.EntropyRateDimension.FairPairs.Law.ofObservable_gridEntropy line 33
  6. theorem OAI.EntropyRateDimension.FairPairs.Law.smul_sum_ofObservable line 43
  7. def OAI.EntropyRateDimension.FiniteCondition.fiber line 71
  8. def OAI.EntropyRateDimension.FiniteCondition.mass line 74
  9. theorem OAI.EntropyRateDimension.FiniteCondition.mass_pos line 77
  10. theorem OAI.EntropyRateDimension.FiniteCondition.mass_eq_of_tag line 82
  11. def OAI.EntropyRateDimension.FiniteCondition.posterior line 85
  12. theorem OAI.EntropyRateDimension.FiniteCondition.posterior_nonneg line 88
  13. theorem OAI.EntropyRateDimension.FiniteCondition.posterior_sum line 95
  14. theorem OAI.EntropyRateDimension.FiniteCondition.posterior_uncondition line 102
  15. theorem OAI.EntropyRateDimension.FiniteCondition.posterior_expectation line 117
  16. theorem OAI.EntropyRateDimension.FiniteCondition.fiber_normalized_sum line 123
  17. def OAI.EntropyRateDimension.FiniteCondition.law line 128
  18. theorem OAI.EntropyRateDimension.FiniteCondition.law_entropy_mean line 132
  19. theorem OAI.EntropyRateDimension.FiniteCondition.law_smul_sum line 146
  20. theorem OAI.EntropyRateDimension.FiniteCondition.posterior_smul_uncondition line 156