OAI/Probability/ThreeStateClauses/RadialAlgebra.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

Radial Algebra.

  1. abbrev OAI.ThreeState.TreeClauses.Radial.Vec line 12
  2. def OAI.ThreeState.TreeClauses.Radial.avg line 14
  3. def OAI.ThreeState.TreeClauses.Radial.PositiveMessage line 16
  4. def OAI.ThreeState.TreeClauses.Radial.centered line 18
  5. def OAI.ThreeState.TreeClauses.Radial.momentX line 20
  6. def OAI.ThreeState.TreeClauses.Radial.momentY line 22
  7. def OAI.ThreeState.TreeClauses.Radial.logAverage line 24
  8. def OAI.ThreeState.TreeClauses.Radial.logCentered line 26
  9. def OAI.ThreeState.TreeClauses.Radial.info line 28
  10. def OAI.ThreeState.TreeClauses.Radial.symEntropy line 30
  11. def OAI.ThreeState.TreeClauses.Radial.correction line 32
  12. def OAI.ThreeState.TreeClauses.Radial.functional line 34
  13. def OAI.ThreeState.TreeClauses.Radial.edge line 36
  14. def OAI.ThreeState.TreeClauses.Radial.RadialInequality line 38
  15. lemma OAI.ThreeState.TreeClauses.Radial.avg_add line 43
  16. lemma OAI.ThreeState.TreeClauses.Radial.avg_sub line 46
  17. lemma OAI.ThreeState.TreeClauses.Radial.avg_mul line 49
  18. lemma OAI.ThreeState.TreeClauses.Radial.avg_const line 52
  19. lemma OAI.ThreeState.TreeClauses.Radial.avg_centered line 54
  20. lemma OAI.ThreeState.TreeClauses.Radial.info_eq line 59
  21. lemma OAI.ThreeState.TreeClauses.Radial.functional_eq line 62
  22. lemma OAI.ThreeState.TreeClauses.Radial.third_eq line 66
  23. lemma OAI.ThreeState.TreeClauses.Radial.momentX_nonneg line 69
  24. lemma OAI.ThreeState.TreeClauses.Radial.cubic line 72
  25. lemma OAI.ThreeState.TreeClauses.Radial.product_eq line 83
  26. lemma OAI.ThreeState.TreeClauses.Radial.discriminant line 88
  27. lemma OAI.ThreeState.TreeClauses.Radial.moment_discriminant line 93
  28. lemma OAI.ThreeState.TreeClauses.Radial.momentX_lt_one line 98
  29. lemma OAI.ThreeState.TreeClauses.Radial.denominator_pos line 106
  30. def OAI.ThreeState.TreeClauses.Radial.hpoly line 119
  31. def OAI.ThreeState.TreeClauses.Radial.Hpoly line 121
  32. lemma OAI.ThreeState.TreeClauses.Radial.Hpoly_one line 123
  33. lemma OAI.ThreeState.TreeClauses.Radial.Hpoly_two line 126
  34. lemma OAI.ThreeState.TreeClauses.Radial.Hpoly_three line 130
  35. def OAI.ThreeState.TreeClauses.Radial.polyA line 135
  36. def OAI.ThreeState.TreeClauses.Radial.polyC line 138
  37. def OAI.ThreeState.TreeClauses.Radial.polyN line 141
  38. def OAI.ThreeState.TreeClauses.Radial.polyL line 143
  39. lemma OAI.ThreeState.TreeClauses.Radial.polyN_one line 149
  40. lemma OAI.ThreeState.TreeClauses.Radial.polyN_affine line 153