OAI/Probability/ThreeStateClauses/PositiveFixed.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Positive Fixed.

  1. def OAI.ThreeState.TreeClauses.Positive.qExact line 16
  2. def OAI.ThreeState.TreeClauses.Positive.cExact line 17
  3. def OAI.ThreeState.TreeClauses.Positive.jMean line 19
  4. def OAI.ThreeState.TreeClauses.Positive.edgeJMean line 21
  5. lemma OAI.ThreeState.TreeClauses.Positive.edgeJ_integrable line 23
  6. lemma OAI.ThreeState.TreeClauses.Positive.residual_integrable line 28
  7. lemma OAI.ThreeState.TreeClauses.Positive.momentA_integrable line 40
  8. lemma OAI.ThreeState.TreeClauses.Positive.momentQ_integrable line 49
  9. lemma OAI.ThreeState.TreeClauses.Positive.expected_moment_bounds line 62
  10. theorem OAI.ThreeState.TreeClauses.Positive.regular_fixed_moment_bounds line 117
  11. lemma OAI.ThreeState.TreeClauses.Positive.branch_sum_first line 141
  12. lemma OAI.ThreeState.TreeClauses.Positive.branch_sum_second line 150
  13. lemma OAI.ThreeState.TreeClauses.Positive.reciprocal_tangent line 159
  14. lemma OAI.ThreeState.TreeClauses.Positive.weighted_branch_jensen line 164
  15. lemma OAI.ThreeState.TreeClauses.Positive.sqrt_branch_sum line 203
  16. lemma OAI.ThreeState.TreeClauses.Positive.truncated_quadratic line 241
  17. lemma OAI.ThreeState.TreeClauses.Positive.product_cubic_bound line 256
  18. lemma OAI.ThreeState.TreeClauses.Positive.correlation_truncated line 271
  19. lemma OAI.ThreeState.TreeClauses.Positive.finite_increment_bound line 284
  20. lemma OAI.ThreeState.TreeClauses.Positive.finite_correlation_sum line 325
  21. theorem OAI.ThreeState.TreeClauses.Positive.regular_fixed_correlation_bounds line 341
  22. lemma OAI.ThreeState.TreeClauses.Positive.fixed_edgeJ line 387
  23. lemma OAI.ThreeState.TreeClauses.Positive.regular_fixed_entropy_radial line 399
  24. lemma OAI.ThreeState.TreeClauses.Positive.qExact_lower line 476
  25. lemma OAI.ThreeState.TreeClauses.Positive.cExact_lower line 482
  26. lemma OAI.ThreeState.TreeClauses.Positive.qExact_coefficient line 488
  27. lemma OAI.ThreeState.TreeClauses.Positive.jMean_square_bound line 493
  28. lemma OAI.ThreeState.TreeClauses.Positive.strict_correlation_coefficient line 514
  29. theorem OAI.ThreeState.TreeClauses.Positive.regular_fixed_mu_zero line 530
  30. lemma OAI.ThreeState.TreeClauses.Positive.message_uniform_of_x_zero line 587
  31. theorem OAI.ThreeState.TreeClauses.Positive.regular_fixed_uniform line 592