OAI/Probability/ThreeState/RadialMoments.lean

GitHub source file

76 declarations, 0 contain sorry, 0 declared as axioms

Three-coordinate moment identities and positive radial polynomials.

  1. def OAI.ThreeState.Radial.f0 line 9
  2. def OAI.ThreeState.Radial.f1 line 10
  3. def OAI.ThreeState.Radial.f2 line 12
  4. lemma OAI.ThreeState.Radial.tail0_pos line 14
  5. lemma OAI.ThreeState.Radial.tail1_pos line 16
  6. lemma OAI.ThreeState.Radial.tail2_pos line 18
  7. lemma OAI.ThreeState.Radial.transform_f0 line 21
  8. lemma OAI.ThreeState.Radial.transform_f1 line 28
  9. lemma OAI.ThreeState.Radial.transform_f2 line 35
  10. lemma OAI.ThreeState.Radial.f0_pos line 42
  11. lemma OAI.ThreeState.Radial.f1_pos line 58
  12. lemma OAI.ThreeState.Radial.f2_pos line 74
  13. def OAI.ThreeState.Radial.A line 90
  14. def OAI.ThreeState.Radial.C line 92
  15. def OAI.ThreeState.Radial.Lscaled line 94
  16. lemma OAI.ThreeState.Radial.N1_factor line 98
  17. def OAI.ThreeState.Radial.xa line 103
  18. def OAI.ThreeState.Radial.a0 line 104
  19. def OAI.ThreeState.Radial.a1 line 105
  20. def OAI.ThreeState.Radial.a2 line 106
  21. def OAI.ThreeState.Radial.b0 line 107
  22. def OAI.ThreeState.Radial.b1 line 108
  23. def OAI.ThreeState.Radial.b2 line 109
  24. def OAI.ThreeState.Radial.b3 line 110
  25. lemma OAI.ThreeState.Radial.a_nonneg line 112
  26. lemma OAI.ThreeState.Radial.b_nonneg line 122
  27. lemma OAI.ThreeState.Radial.A_certificate line 134
  28. lemma OAI.ThreeState.Radial.L_certificate line 141
  29. lemma OAI.ThreeState.Radial.A_nonneg_param line 148
  30. lemma OAI.ThreeState.Radial.L_nonneg_param line 157
  31. lemma OAI.ThreeState.Radial.physical_parameterization line 166
  32. lemma OAI.ThreeState.Radial.physical_signs line 201
  33. def OAI.ThreeState.Radial.avg line 234
  34. def OAI.ThreeState.Radial.momentX line 235
  35. def OAI.ThreeState.Radial.momentY line 236
  36. def OAI.ThreeState.Radial.denom line 237
  37. def OAI.ThreeState.Radial.cofactor line 239
  38. def OAI.ThreeState.Radial.kernel line 241
  39. def OAI.ThreeState.Radial.centeredLog line 243
  40. lemma OAI.ThreeState.Radial.avg_expand line 246
  41. lemma OAI.ThreeState.Radial.zero_sum_elim line 249
  42. lemma OAI.ThreeState.Radial.cubic_identity line 252
  43. lemma OAI.ThreeState.Radial.denom_product line 263
  44. lemma OAI.ThreeState.Radial.cofactor_identity line 269
  45. lemma OAI.ThreeState.Radial.message_segment_pos line 274
  46. lemma OAI.ThreeState.Radial.denom_pos line 282
  47. lemma OAI.ThreeState.Radial.momentX_nonneg line 288
  48. lemma OAI.ThreeState.Radial.discriminant line 291
  49. lemma OAI.ThreeState.Radial.discriminant_nonneg line 298
  50. lemma OAI.ThreeState.Radial.momentX_lt_one line 304
  51. lemma OAI.ThreeState.Radial.momentY_le_X line 314
  52. lemma OAI.ThreeState.Radial.denom_le_one line 323
  53. def OAI.ThreeState.Radial.cofMoment line 332
  54. lemma OAI.ThreeState.Radial.cofMoment_one line 335
  55. lemma OAI.ThreeState.Radial.cofMoment_two line 341
  56. lemma OAI.ThreeState.Radial.cofMoment_three line 347
  57. def OAI.ThreeState.Radial.numerator line 354
  58. lemma OAI.ThreeState.Radial.numerator_expansion line 359
  59. lemma OAI.ThreeState.Radial.integral_avg line 367
  60. lemma OAI.ThreeState.Radial.log_integral line 373
  61. lemma OAI.ThreeState.Radial.kernel_div_identity line 391
  62. lemma OAI.ThreeState.Radial.centeredLog_integral line 422
  63. def OAI.ThreeState.Radial.invMoment line 444
  64. def OAI.ThreeState.Radial.logInvMoment line 446
  65. def OAI.ThreeState.Radial.logMoment line 448
  66. def OAI.ThreeState.Radial.gExpr line 451
  67. def OAI.ThreeState.Radial.rCore line 456
  68. def OAI.ThreeState.Radial.logCoeff line 460
  69. lemma OAI.ThreeState.Radial.inv_cofactor line 464
  70. lemma OAI.ThreeState.Radial.RN_algebra line 470
  71. lemma OAI.ThreeState.Radial.kernel_div_integrable line 480
  72. lemma OAI.ThreeState.Radial.RN_representation line 489
  73. lemma OAI.ThreeState.Radial.integrate_N_lower line 507
  74. lemma OAI.ThreeState.Radial.L_expansion line 526
  75. lemma OAI.ThreeState.Radial.numerator_nonneg line 541
  76. lemma OAI.ThreeState.Radial.gExpr_lower line 553