OAI/Probability/ThreeStateClauses/PoissonFixed.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Poisson Fixed.

  1. def OAI.ThreeState.TreeClauses.Experiment.uniformMessage line 17
  2. lemma OAI.ThreeState.TreeClauses.Experiment.uniformMessage_x line 19
  3. lemma OAI.ThreeState.TreeClauses.Experiment.branch_uniform line 21
  4. lemma OAI.ThreeState.TreeClauses.Experiment.branchOutput_uniform line 25
  5. lemma OAI.ThreeState.TreeClauses.Experiment.finite_uniform_atom line 32
  6. lemma OAI.ThreeState.TreeClauses.Experiment.poisson_generating line 48
  7. lemma OAI.ThreeState.TreeClauses.Experiment.poisson_uniform_atom line 66
  8. def OAI.ThreeState.TreeClauses.Experiment.Law.nonuniformMass line 88
  9. lemma OAI.ThreeState.TreeClauses.Experiment.Law.nonuniformMass_nonneg line 90
  10. lemma OAI.ThreeState.TreeClauses.Experiment.Law.nonuniformMass_le_one line 94
  11. lemma OAI.ThreeState.TreeClauses.Experiment.Law.nonuniform_second_moment line 98
  12. lemma OAI.ThreeState.TreeClauses.Probability.neg_log_one_sub_lower line 130
  13. lemma OAI.ThreeState.TreeClauses.Probability.poisson_subfixed_mass_bound line 153
  14. lemma OAI.ThreeState.TreeClauses.Positive.poisson_fixed_mass_bound line 184
  15. theorem OAI.ThreeState.TreeClauses.Positive.poisson_fixed_mu_zero line 200
  16. lemma OAI.ThreeState.TreeClauses.Tree.ordered_advantage_sq_moment line 270
  17. lemma OAI.ThreeState.TreeClauses.Tree.poisson_positive_critical_mu line 280
  18. theorem OAI.ThreeState.TreeClauses.Tree.poisson_positive_nonreconstruction line 304