OAI/Probability/ThreeStateClauses/FiniteUpdate.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

Finite Update.

  1. def OAI.ThreeState.TreeClauses.Experiment.branchOutput line 19
  2. lemma OAI.ThreeState.TreeClauses.Experiment.continuous_branchOutput line 25
  3. def OAI.ThreeState.TreeClauses.Experiment.tiltedProduct line 31
  4. lemma OAI.ThreeState.TreeClauses.Experiment.tiltedProduct_isProbability line 35
  5. lemma OAI.ThreeState.TreeClauses.Experiment.integral_tiltedProduct line 44
  6. lemma OAI.ThreeState.TreeClauses.Experiment.measurePreserving_density line 56
  7. lemma OAI.ThreeState.TreeClauses.Experiment.branchProduct_permute line 65
  8. lemma OAI.ThreeState.TreeClauses.Experiment.normalizer_permute line 70
  9. lemma OAI.ThreeState.TreeClauses.Experiment.branchOutput_permute line 76
  10. lemma OAI.ThreeState.TreeClauses.Experiment.tiltedProduct_symmetric line 85
  11. def OAI.ThreeState.TreeClauses.Experiment.finiteProbability line 98
  12. lemma OAI.ThreeState.TreeClauses.Experiment.integral_finiteProbability line 103
  13. lemma OAI.ThreeState.TreeClauses.Experiment.finiteProbability_balanced line 112
  14. lemma OAI.ThreeState.TreeClauses.Experiment.finiteProbability_symmetric line 124
  15. def OAI.ThreeState.TreeClauses.Experiment.finiteLaw line 139
  16. lemma OAI.ThreeState.TreeClauses.Experiment.channel_real line 156
  17. lemma OAI.ThreeState.TreeClauses.Experiment.edge_pmf_real line 160
  18. def OAI.ThreeState.TreeClauses.Experiment.discreteBranchLaw line 176
  19. lemma OAI.ThreeState.TreeClauses.Experiment.discreteBranchLaw_real line 179
  20. lemma OAI.ThreeState.TreeClauses.Experiment.discreteBranchWeight line 186
  21. lemma OAI.ThreeState.TreeClauses.Experiment.discreteBranchMessage line 194
  22. lemma OAI.ThreeState.TreeClauses.Experiment.discreteBranch_integrand line 208
  23. lemma OAI.ThreeState.TreeClauses.Experiment.discreteMessage_preserving line 222
  24. lemma OAI.ThreeState.TreeClauses.Experiment.integral_discreteBranchLaw line 226
  25. lemma OAI.ThreeState.TreeClauses.Experiment.probability_ext_continuous line 246
  26. lemma OAI.ThreeState.TreeClauses.Experiment.discreteBranchLaw_probability line 253
  27. lemma OAI.ThreeState.TreeClauses.Experiment.measurable_symEntropy line 273
  28. lemma OAI.ThreeState.TreeClauses.Experiment.measurable_info line 279
  29. lemma OAI.ThreeState.TreeClauses.Experiment.measurable_correction line 284
  30. lemma OAI.ThreeState.TreeClauses.Experiment.continuous_symEntropy_comp line 293
  31. lemma OAI.ThreeState.TreeClauses.Experiment.continuous_correction_comp line 300
  32. lemma OAI.ThreeState.TreeClauses.Experiment.continuous_info_comp line 309
  33. lemma OAI.ThreeState.TreeClauses.Experiment.finite_integrable_of_comp line 313
  34. lemma OAI.ThreeState.TreeClauses.Experiment.finite_integrable_symEntropy line 321
  35. lemma OAI.ThreeState.TreeClauses.Experiment.finite_integrable_correction line 327
  36. lemma OAI.ThreeState.TreeClauses.Experiment.measurableSet_positive line 333
  37. lemma OAI.ThreeState.TreeClauses.Experiment.finite_positive line 340
  38. lemma OAI.ThreeState.TreeClauses.Experiment.finiteLaw_symEntropy line 346
  39. lemma OAI.ThreeState.TreeClauses.Experiment.finiteLaw_correction line 353
  40. lemma OAI.ThreeState.TreeClauses.Experiment.finiteLaw_info line 361