OAI/Probability/ThreeState/ScalarBounds.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Scalar inequalities for criticality, Poisson survival and nonlinear decay.

  1. def OAI.ThreeState.PositiveScalar.lowerC line 9
  2. lemma OAI.ThreeState.PositiveScalar.small_polynomial line 11
  3. lemma OAI.ThreeState.PositiveScalar.middle_polynomial line 23
  4. lemma OAI.ThreeState.PositiveScalar.rational_lower line 40
  5. lemma OAI.ThreeState.PositiveScalar.regular_scalar line 44
  6. lemma OAI.ThreeState.PositiveScalar.high_scalar line 79
  7. theorem OAI.ThreeState.PositiveScalar.scalar_contradiction line 96
  8. lemma OAI.ThreeState.PositiveScalar.q_lower line 119
  9. lemma OAI.ThreeState.PositiveScalar.root_loss line 124
  10. lemma OAI.ThreeState.PositiveScalar.J_square_bound line 130
  11. lemma OAI.ThreeState.PositiveScalar.scalar_from_moments line 153
  12. lemma OAI.ThreeState.PositiveScalar.moment_scalar_contradiction line 174
  13. lemma OAI.ThreeState.poisson_sqrt_tangent line 202
  14. lemma OAI.ThreeState.poisson_reciprocal_tangent line 215
  15. lemma OAI.ThreeState.poisson_correlation_scalar line 223
  16. lemma OAI.ThreeState.log_survival_bound line 288
  17. lemma OAI.ThreeState.poisson_support_bound line 317
  18. lemma OAI.ThreeState.bernoulli_lower line 338
  19. lemma OAI.ThreeState.bernoulli_quadratic_lower line 346
  20. def OAI.ThreeState.decaySeq line 358
  21. lemma OAI.ThreeState.decaySeq_bounds line 361
  22. lemma OAI.ThreeState.decaySeq_antitone line 371
  23. lemma OAI.ThreeState.decaySeq_tendsto line 373