OAI/Probability/ThreeStateClauses/PoissonMoments.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Poisson Moments.

  1. def OAI.ThreeState.TreeClauses.Probability.poissonWeight line 14

    Distinct definitions of this name: ComparatorChallenges/ThreeStateTreeClauses.lean:68 (different declaration text). Qualify references as OAI.ThreeState.TreeClauses.Probability.poissonWeight@path.

  2. lemma OAI.ThreeState.TreeClauses.Probability.poissonWeight_nonneg line 16

    Distinct definitions of this name: ComparatorChallenges/ThreeStateTreeClauses.lean:71 (different declaration text). Qualify references as OAI.ThreeState.TreeClauses.Probability.poissonWeight_nonneg@path.

  3. lemma OAI.ThreeState.TreeClauses.Probability.poissonWeight_mass line 19

    Distinct definitions of this name: ComparatorChallenges/ThreeStateTreeClauses.lean:76 (different declaration text). Qualify references as OAI.ThreeState.TreeClauses.Probability.poissonWeight_mass@path.

  4. def OAI.ThreeState.TreeClauses.Probability._root_.OAI.ThreeState.TreeClauses.poissonPMF line 22

    Also declared: ComparatorChallenges/ThreeStateTreeClauses.lean:79 (same declaration text).

  5. lemma OAI.ThreeState.TreeClauses.Probability.poissonWeight_succ line 28
  6. lemma OAI.ThreeState.TreeClauses.Probability.poissonWeight_mean line 35
  7. lemma OAI.ThreeState.TreeClauses.Probability.poissonWeight_factorial_second line 41
  8. lemma OAI.ThreeState.TreeClauses.Probability.poissonWeight_second line 55
  9. lemma OAI.ThreeState.TreeClauses.Probability.poissonPMF_real line 61
  10. lemma OAI.ThreeState.TreeClauses.Probability.poissonPMF_toMeasure line 65
  11. lemma OAI.ThreeState.TreeClauses.Probability.poisson_integrable_first line 72
  12. lemma OAI.ThreeState.TreeClauses.Probability.poisson_integrable_second line 76
  13. lemma OAI.ThreeState.TreeClauses.Probability.poisson_integral_first line 80
  14. lemma OAI.ThreeState.TreeClauses.Probability.poisson_integral_second line 84
  15. lemma OAI.ThreeState.TreeClauses.Probability.poisson_integral_factorial_second line 88