OAI/Probability/ThreeStateClauses/BranchMoments.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

Branch Moments.

  1. def OAI.ThreeState.TreeClauses.Experiment.branchProduct line 18
  2. def OAI.ThreeState.TreeClauses.Experiment.normalizer line 20
  3. def OAI.ThreeState.TreeClauses.Experiment.normalizedProduct line 22
  4. lemma OAI.ThreeState.TreeClauses.Experiment.avg_sum line 24
  5. lemma OAI.ThreeState.TreeClauses.Experiment.avg_div line 30
  6. lemma OAI.ThreeState.TreeClauses.Experiment.normalizer_positive line 33
  7. lemma OAI.ThreeState.TreeClauses.Experiment.normalizedProduct_positive line 38
  8. lemma OAI.ThreeState.TreeClauses.Experiment.log_normalizedProduct line 45
  9. lemma OAI.ThreeState.TreeClauses.Experiment.logCentered_normalizedProduct line 52
  10. lemma OAI.ThreeState.TreeClauses.Experiment.symEntropy_centeredLog line 58
  11. lemma OAI.ThreeState.TreeClauses.Experiment.weighted_symEntropy line 69
  12. lemma OAI.ThreeState.TreeClauses.Experiment.weighted_correction line 78
  13. lemma OAI.ThreeState.TreeClauses.Experiment.weighted_info line 84
  14. def OAI.ThreeState.TreeClauses.Experiment.weightProduct line 107
  15. lemma OAI.ThreeState.TreeClauses.Experiment.select_product line 110
  16. lemma OAI.ThreeState.TreeClauses.Experiment.integrable_weighted_single line 115
  17. lemma OAI.ThreeState.TreeClauses.Experiment.integral_weighted_single line 124
  18. lemma OAI.ThreeState.TreeClauses.Experiment.select_pair_product line 135
  19. lemma OAI.ThreeState.TreeClauses.Experiment.integrable_weighted_pair line 142
  20. lemma OAI.ThreeState.TreeClauses.Experiment.integral_weighted_pair line 154
  21. lemma OAI.ThreeState.TreeClauses.Experiment.integrable_weighted_sum line 174
  22. lemma OAI.ThreeState.TreeClauses.Experiment.integral_weighted_sum line 179
  23. lemma OAI.ThreeState.TreeClauses.Experiment.integrable_weighted_sq_sum line 187
  24. theorem OAI.ThreeState.TreeClauses.Experiment.integral_weighted_sq_sum line 197
  25. abbrev OAI.ThreeState.TreeClauses.Experiment.branchEdges line 226
  26. def OAI.ThreeState.TreeClauses.Experiment.finiteBranchExpectation line 228
  27. def OAI.ThreeState.TreeClauses.Experiment.correlationEntropy line 232
  28. lemma OAI.ThreeState.TreeClauses.Experiment.branchEdges_positive line 236
  29. lemma OAI.ThreeState.TreeClauses.Experiment.continuous_branchProduct line 239
  30. lemma OAI.ThreeState.TreeClauses.Experiment.continuous_normalizer line 244
  31. lemma OAI.ThreeState.TreeClauses.Experiment.continuous_correlationIntegrand line 248
  32. lemma OAI.ThreeState.TreeClauses.Experiment.integral_normalizer line 253
  33. lemma OAI.ThreeState.TreeClauses.Experiment.correlationEntropy_nonneg line 265
  34. theorem OAI.ThreeState.TreeClauses.Experiment.finite_symEntropy line 282
  35. theorem OAI.ThreeState.TreeClauses.Experiment.finite_correction line 305
  36. theorem OAI.ThreeState.TreeClauses.Experiment.finite_info line 333