OAI/Probability/ThreeStateClauses/PoissonCalculus.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

Poisson Calculus.

  1. def OAI.ThreeState.TreeClauses.Probability.exponentialAverage line 16
  2. def OAI.ThreeState.TreeClauses.Probability.poissonAverage line 18
  3. lemma OAI.ThreeState.TreeClauses.Probability.exponentialAverage_summable line 20
  4. def OAI.ThreeState.TreeClauses.Probability.exponentialDerivative line 27
  5. lemma OAI.ThreeState.TreeClauses.Probability.exponentialDerivative_summable line 31
  6. lemma OAI.ThreeState.TreeClauses.Probability.exponentialDerivative_sum line 36
  7. lemma OAI.ThreeState.TreeClauses.Probability.hasDerivAt_exponentialAverage line 41
  8. theorem OAI.ThreeState.TreeClauses.Probability.hasDerivAt_poissonAverage line 75
  9. lemma OAI.ThreeState.TreeClauses.Probability.poissonAverage_eq_tsum line 81
  10. lemma OAI.ThreeState.TreeClauses.Probability.poissonAverage_eq_integral line 86
  11. lemma OAI.ThreeState.TreeClauses.Probability.continuous_poissonAverage line 94
  12. lemma OAI.ThreeState.TreeClauses.Probability.poissonAverage_zero line 98
  13. lemma OAI.ThreeState.TreeClauses.Experiment.offspring_positive line 114
  14. lemma OAI.ThreeState.TreeClauses.Experiment.correction_nonneg line 121
  15. lemma OAI.ThreeState.TreeClauses.Experiment.poisson_mixture_integrable_nonneg line 127
  16. lemma OAI.ThreeState.TreeClauses.Experiment.poisson_integrable_symEntropy line 139
  17. lemma OAI.ThreeState.TreeClauses.Experiment.poisson_integrable_correction line 149
  18. lemma OAI.ThreeState.TreeClauses.Experiment.poissonLaw_symEntropy line 165
  19. lemma OAI.ThreeState.TreeClauses.Experiment.poissonLaw_correction line 175
  20. def OAI.ThreeState.TreeClauses.Experiment.iMean line 191
  21. def OAI.ThreeState.TreeClauses.Experiment.edgeIMean line 193
  22. lemma OAI.ThreeState.TreeClauses.Experiment.bounded_iMean line 195
  23. def OAI.ThreeState.TreeClauses.Experiment.poissonCorrelation line 203
  24. lemma OAI.ThreeState.TreeClauses.Experiment.poissonLaw_info line 206
  25. lemma OAI.ThreeState.TreeClauses.Experiment.poissonCorrelation_continuous line 220
  26. lemma OAI.ThreeState.TreeClauses.Positive.poisson_fixed_edgeJ line 236
  27. lemma OAI.ThreeState.TreeClauses.Positive.functional_integral line 248
  28. lemma OAI.ThreeState.TreeClauses.Positive.integrated_radial line 260
  29. lemma OAI.ThreeState.TreeClauses.Positive.poisson_fixed_entropy_radial line 286
  30. lemma OAI.ThreeState.TreeClauses.Positive.poisson_fixed_moment_bounds line 331
  31. lemma OAI.ThreeState.TreeClauses.Experiment.finite_iMean_succ line 350
  32. lemma OAI.ThreeState.TreeClauses.Experiment.finite_iMean_zero line 357
  33. lemma OAI.ThreeState.TreeClauses.Experiment.poissonCorrelation_zero line 362
  34. def OAI.ThreeState.TreeClauses.Experiment.poissonSlope line 366
  35. lemma OAI.ThreeState.TreeClauses.Experiment.hasDerivAt_poissonCorrelation line 370
  36. lemma OAI.ThreeState.TreeClauses.Experiment.continuous_poissonSlope line 377
  37. lemma OAI.ThreeState.TreeClauses.Experiment.bounded_pairCorrelation line 384
  38. lemma OAI.ThreeState.TreeClauses.Experiment.poissonSlope_eq_pairCorrelation line 393
  39. lemma OAI.ThreeState.TreeClauses.Positive.poisson_increment_bound line 428
  40. lemma OAI.ThreeState.TreeClauses.Positive.sqrt_intensity_tangent line 467
  41. theorem OAI.ThreeState.TreeClauses.Positive.poisson_fixed_correlation_bound line 479