OAI/Probability/ThreeState/RadialDerivatives.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

Radial logarithmic derivatives and the entropy inequality.

  1. def OAI.ThreeState.Radial.ray line 10
  2. def OAI.ThreeState.Radial.logAvg line 11
  3. def OAI.ThreeState.Radial.logVariance line 12
  4. def OAI.ThreeState.Radial.weightedLogVariance line 13
  5. def OAI.ThreeState.Radial.energy line 16
  6. def OAI.ThreeState.Radial.gapY line 19
  7. def OAI.ThreeState.Radial.gapZ line 23
  8. lemma OAI.ThreeState.Radial.avg_hasDerivAt line 28
  9. lemma OAI.ThreeState.Radial.avg_ray line 34
  10. lemma OAI.ThreeState.Radial.X_ray line 36
  11. lemma OAI.ThreeState.Radial.centeredLog_avg_zero line 38
  12. lemma OAI.ThreeState.Radial.ray_log_hasDerivAt line 41
  13. lemma OAI.ThreeState.Radial.ray_inv_hasDerivAt line 44
  14. lemma OAI.ThreeState.Radial.logAvg_hasDerivAt line 49
  15. lemma OAI.ThreeState.Radial.centeredLog_hasDerivAt line 60
  16. lemma OAI.ThreeState.Radial.invMoment_one_hasDerivAt line 67
  17. lemma OAI.ThreeState.Radial.invMoment_two_hasDerivAt line 79
  18. lemma OAI.ThreeState.Radial.logMoment_hasDerivAt line 93
  19. lemma OAI.ThreeState.Radial.logVariance_hasDerivAt line 111
  20. lemma OAI.ThreeState.Radial.weightedLogVariance_hasDerivAt line 127
  21. lemma OAI.ThreeState.Radial.logInvMoment_one_hasDerivAt line 147
  22. lemma OAI.ThreeState.Radial.X_hasDerivAt line 163
  23. lemma OAI.ThreeState.Radial.energy_hasDerivAt line 168
  24. lemma OAI.ThreeState.Radial.gapY_hasDerivAt line 177
  25. lemma OAI.ThreeState.Radial.gapZ_hasDerivAt line 192
  26. lemma OAI.ThreeState.Radial.ray_zero line 213
  27. lemma OAI.ThreeState.Radial.ray_one line 214
  28. lemma OAI.ThreeState.Radial.logAvg_zero line 215
  29. lemma OAI.ThreeState.Radial.centeredLog_zero line 216
  30. lemma OAI.ThreeState.Radial.logMoment_zero line 218
  31. lemma OAI.ThreeState.Radial.logVariance_zero line 219
  32. lemma OAI.ThreeState.Radial.weightedLogVariance_zero line 220
  33. lemma OAI.ThreeState.Radial.invMoment_zero line 222
  34. lemma OAI.ThreeState.Radial.logInvMoment_zero line 224
  35. lemma OAI.ThreeState.Radial.momentX_zero line 226
  36. lemma OAI.ThreeState.Radial.energy_zero line 227
  37. lemma OAI.ThreeState.Radial.gapY_zero line 228
  38. lemma OAI.ThreeState.Radial.gapZ_zero line 229
  39. lemma OAI.ThreeState.Radial.logAvg_hasDerivAt_zero line 231
  40. lemma OAI.ThreeState.Radial.centeredLog_hasDerivAt_zero line 237
  41. lemma OAI.ThreeState.Radial.invMoment_one_hasDerivAt_zero line 242
  42. lemma OAI.ThreeState.Radial.logMoment_hasDerivAt_zero line 249
  43. lemma OAI.ThreeState.Radial.logVariance_hasDerivAt_zero line 257
  44. lemma OAI.ThreeState.Radial.weightedLogVariance_hasDerivAt_zero line 264
  45. lemma OAI.ThreeState.Radial.gapY_hasDerivAt_zero line 272
  46. lemma OAI.ThreeState.Radial.logAvg_continuousAt line 283
  47. lemma OAI.ThreeState.Radial.centeredLog_continuousAt line 289
  48. lemma OAI.ThreeState.Radial.gapZ_continuousAt line 294
  49. lemma OAI.ThreeState.Radial.normalized_gapY_continuousAt_zero line 303
  50. lemma OAI.ThreeState.Radial.gapZ_nonneg line 315
  51. lemma OAI.ThreeState.Radial.normalized_gapY_hasDerivAt line 336
  52. lemma OAI.ThreeState.Radial.gapY_nonneg line 342
  53. lemma OAI.ThreeState.Radial.normalized_energy_hasDerivAt line 366
  54. theorem OAI.ThreeState.Radial.radial_inequality line 376
  55. def OAI.ThreeState.Radial.sourceF line 408
  56. lemma OAI.ThreeState.Radial.avg_message_deviation line 414
  57. lemma OAI.ThreeState.Radial.logMoment_uncentered line 419
  58. lemma OAI.ThreeState.Radial.energy_sourceF line 425
  59. theorem OAI.ThreeState.Radial.radial_source line 434