OAI/Probability/ThreeStateClauses/CompactLimits.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

Compact Limits.

  1. def OAI.ThreeState.TreeClauses.Experiment.quadraticGap line 18
  2. lemma OAI.ThreeState.TreeClauses.Experiment.continuous_quadraticGap line 20
  3. lemma OAI.ThreeState.TreeClauses.Experiment.quadraticGap_nonneg line 25
  4. lemma OAI.ThreeState.TreeClauses.Experiment.quadraticGap_zero_iff line 28
  5. lemma OAI.ThreeState.TreeClauses.Experiment.quadraticGap_expand line 40
  6. lemma OAI.ThreeState.TreeClauses.Experiment.continuous_centeredProduct line 45
  7. def OAI.ThreeState.TreeClauses.Experiment.degradationCoupling line 54
  8. lemma OAI.ThreeState.TreeClauses.Experiment.integral_degradationCoupling line 58
  9. lemma OAI.ThreeState.TreeClauses.Experiment.degradationCoupling_fst line 68
  10. lemma OAI.ThreeState.TreeClauses.Experiment.degradationCoupling_snd line 77
  11. lemma OAI.ThreeState.TreeClauses.Experiment.degradationCoupling_centered line 87
  12. lemma OAI.ThreeState.TreeClauses.Experiment.degradationCoupling_loss line 96
  13. lemma OAI.ThreeState.TreeClauses.Experiment.discrete_degradation_mu line 123
  14. def OAI.ThreeState.TreeClauses.Tree.vertex line 142
  15. lemma OAI.ThreeState.TreeClauses.Tree.discreteMessage_pure line 146
  16. lemma OAI.ThreeState.TreeClauses.Tree.vertex_permute line 151
  17. lemma OAI.ThreeState.TreeClauses.Tree.pureMarginal line 157
  18. lemma OAI.ThreeState.TreeClauses.Tree.integral_rootProbability line 159
  19. lemma OAI.ThreeState.TreeClauses.Tree.rootProbability_symmetric line 168
  20. def OAI.ThreeState.TreeClauses.Tree.rootLaw line 184
  21. def OAI.ThreeState.TreeClauses.Tree.regularPosteriorLaw line 189
  22. lemma OAI.ThreeState.TreeClauses.Tree.regularPosteriorLaw_probability line 193
  23. lemma OAI.ThreeState.TreeClauses.Tree.regularPosteriorLaw_antitone line 202
  24. lemma OAI.ThreeState.TreeClauses.Experiment.probability_continuous_integral line 222
  25. lemma OAI.ThreeState.TreeClauses.Experiment.limit_balanced line 230
  26. lemma OAI.ThreeState.TreeClauses.Experiment.limit_symmetric line 236
  27. def OAI.ThreeState.TreeClauses.Experiment.limitLaw line 245
  28. lemma OAI.ThreeState.TreeClauses.Experiment.finiteProbability_tendsto line 252
  29. lemma OAI.ThreeState.TreeClauses.Experiment.coupling_diagonal_of_loss_zero line 267
  30. lemma OAI.ThreeState.TreeClauses.Experiment.degrading_finite_fixed_point line 285
  31. def OAI.ThreeState.TreeClauses.Experiment.tvMessage line 339
  32. lemma OAI.ThreeState.TreeClauses.Experiment.continuous_tvMessage line 341
  33. lemma OAI.ThreeState.TreeClauses.Experiment.tvMessage_nonneg line 344
  34. lemma OAI.ThreeState.TreeClauses.Experiment.tvMessage_formula line 347
  35. lemma OAI.ThreeState.TreeClauses.Experiment.tvMessage_sq_bound line 352
  36. lemma OAI.ThreeState.TreeClauses.Experiment.integral_tvMessage_sq_bound line 359
  37. lemma OAI.ThreeState.TreeClauses.Experiment.main_marginal_eq line 380
  38. lemma OAI.ThreeState.TreeClauses.Experiment.main_posterior_eq line 385
  39. lemma OAI.ThreeState.TreeClauses.Experiment.tvMessage_le_one line 393
  40. lemma OAI.ThreeState.TreeClauses.Experiment.integrable_tv_discrete line 399
  41. lemma OAI.ThreeState.TreeClauses.Experiment.advantage_eq_integral line 407
  42. lemma OAI.ThreeState.TreeClauses.Experiment.advantage_nonneg line 423
  43. lemma OAI.ThreeState.TreeClauses.Experiment.advantage_sq_bound line 428