OAI/Probability/ThreeStateClauses/RadialBounds.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

Radial Bounds.

  1. def OAI.ThreeState.TreeClauses.Radial.f₀ line 13
  2. def OAI.ThreeState.TreeClauses.Radial.f₁ line 15
  3. def OAI.ThreeState.TreeClauses.Radial.f₂ line 18
  4. lemma OAI.ThreeState.TreeClauses.Radial.f₀_certificate line 20
  5. lemma OAI.ThreeState.TreeClauses.Radial.f₁_certificate line 26
  6. lemma OAI.ThreeState.TreeClauses.Radial.f₂_certificate line 33
  7. lemma OAI.ThreeState.TreeClauses.Radial.f_positive line 39
  8. def OAI.ThreeState.TreeClauses.Radial.a₀ line 69
  9. def OAI.ThreeState.TreeClauses.Radial.a₁ line 71
  10. def OAI.ThreeState.TreeClauses.Radial.a₂ line 73
  11. def OAI.ThreeState.TreeClauses.Radial.b₀ line 75
  12. def OAI.ThreeState.TreeClauses.Radial.b₁ line 77
  13. def OAI.ThreeState.TreeClauses.Radial.b₂ line 79
  14. def OAI.ThreeState.TreeClauses.Radial.b₃ line 81
  15. lemma OAI.ThreeState.TreeClauses.Radial.a_nonneg line 83
  16. lemma OAI.ThreeState.TreeClauses.Radial.b_nonneg line 94
  17. def OAI.ThreeState.TreeClauses.Radial.normalizedA line 105
  18. def OAI.ThreeState.TreeClauses.Radial.normalizedL line 108
  19. lemma OAI.ThreeState.TreeClauses.Radial.normalizeA line 113
  20. lemma OAI.ThreeState.TreeClauses.Radial.normalizeL line 116
  21. def OAI.ThreeState.TreeClauses.Radial.paramX line 119
  22. lemma OAI.ThreeState.TreeClauses.Radial.a_certificate line 121
  23. lemma OAI.ThreeState.TreeClauses.Radial.b_certificate line 130
  24. lemma OAI.ThreeState.TreeClauses.Radial.param_polynomial_nonneg line 139
  25. lemma OAI.ThreeState.TreeClauses.Radial.domain_parametrization line 159
  26. lemma OAI.ThreeState.TreeClauses.Radial.polyN_one_nonneg line 192
  27. lemma OAI.ThreeState.TreeClauses.Radial.polynomial_goal line 209
  28. lemma OAI.ThreeState.TreeClauses.Radial.polyN_nonneg line 222
  29. def OAI.ThreeState.TreeClauses.Radial.denom line 238
  30. def OAI.ThreeState.TreeClauses.Radial.kpoly line 240
  31. def OAI.ThreeState.TreeClauses.Radial.invMoment line 242
  32. def OAI.ThreeState.TreeClauses.Radial.logInvMoment line 244
  33. def OAI.ThreeState.TreeClauses.Radial.logMoment line 247
  34. def OAI.ThreeState.TreeClauses.Radial.radialG line 249
  35. lemma OAI.ThreeState.TreeClauses.Radial.edge_pos line 255
  36. lemma OAI.ThreeState.TreeClauses.Radial.denom_pos line 263
  37. lemma OAI.ThreeState.TreeClauses.Radial.rational_identity line 266
  38. lemma OAI.ThreeState.TreeClauses.Radial.rational_centered line 273
  39. lemma OAI.ThreeState.TreeClauses.Radial.hasDerivAt_log_edge line 283
  40. lemma OAI.ThreeState.TreeClauses.Radial.integral_log_edge line 287
  41. lemma OAI.ThreeState.TreeClauses.Radial.integral_avg line 300
  42. lemma OAI.ThreeState.TreeClauses.Radial.integral_k line 307
  43. lemma OAI.ThreeState.TreeClauses.Radial.avg_div line 331
  44. lemma OAI.ThreeState.TreeClauses.Radial.avg_logCentered line 334
  45. lemma OAI.ThreeState.TreeClauses.Radial.h_inverse line 337
  46. def OAI.ThreeState.TreeClauses.Radial.polynomialR line 348
  47. def OAI.ThreeState.TreeClauses.Radial.logWeight line 353
  48. lemma OAI.ThreeState.TreeClauses.Radial.polynomialN_representation line 357
  49. lemma OAI.ThreeState.TreeClauses.Radial.G_algebra line 365
  50. lemma OAI.ThreeState.TreeClauses.Radial.integrable_k line 375
  51. lemma OAI.ThreeState.TreeClauses.Radial.integral_N line 382
  52. lemma OAI.ThreeState.TreeClauses.Radial.RN_representation line 396
  53. lemma OAI.ThreeState.TreeClauses.Radial.polynomial_integral line 402
  54. lemma OAI.ThreeState.TreeClauses.Radial.L_representation line 414
  55. theorem OAI.ThreeState.TreeClauses.Radial.radialG_bound line 423