OAI/Probability/GaussianReplacement/FreshRows.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CurrentProjection.cauchyObservation line 13
  2. lemma OAI.CurrentProjection.measurable_cauchyObservation line 17
  3. def OAI.CurrentProjection.cauchyObservationLaw line 22
  4. instance OAI.CurrentProjection.cauchyObservationLaw_probability line 26
  5. lemma OAI.CurrentProjection.gaussian_inner_map_sphere line 31
  6. lemma OAI.CurrentProjection.cauchyObservationLaw_snd line 36
  7. lemma OAI.CurrentProjection.log_standardGaussianPDF line 54
  8. def OAI.CurrentProjection.standardGaussianEntropy line 62
  9. lemma OAI.CurrentProjection.standardGaussian_cross_entropy line 64
  10. lemma OAI.CurrentProjection.cauchyMixture_experiment_bound line 83
  11. def OAI.CurrentProjection.reciprocalScale line 126
  12. def OAI.CurrentProjection.reciprocalCutoff line 129
  13. lemma OAI.CurrentProjection.reciprocalCutoff_pos line 131
  14. lemma OAI.CurrentProjection.reciprocalCutoff_le_one line 132
  15. lemma OAI.CurrentProjection.reciprocalCutoff_antitone line 136
  16. lemma OAI.CurrentProjection.reciprocalCutoff_limit line 141
  17. lemma OAI.CurrentProjection.regularizedReciprocal_monotone line 144
  18. lemma OAI.CurrentProjection.regularizedReciprocal_limit line 151
  19. lemma OAI.CurrentProjection.regularizedScale_ofReal line 165
  20. lemma OAI.CurrentProjection.regularizedScale_limit line 171
  21. lemma OAI.CurrentProjection.regularizedScale_monotone line 180
  22. lemma OAI.CurrentProjection.reciprocalScale_kernel_measurable line 187
  23. lemma OAI.CurrentProjection.regularizedScale_le_reciprocalScale line 193
  24. lemma OAI.CurrentProjection.reciprocalScale_lower line 199
  25. def OAI.CurrentProjection.logScaleExtended line 204
  26. lemma OAI.CurrentProjection.continuous_logScaleExtended line 206
  27. lemma OAI.CurrentProjection.logScaleExtended_monotone line 209
  28. lemma OAI.CurrentProjection.logScaleExtended_ofReal line 214
  29. lemma OAI.CurrentProjection.logScaleExtended_top_iff line 223
  30. lemma OAI.CurrentProjection.log_add_log_two_nonneg line 226
  31. lemma OAI.CurrentProjection.reciprocalScale_log_bound line 232
  32. lemma OAI.CurrentProjection.reciprocalScale_experiment_bound line 300
  33. def OAI.CurrentProjection.residualObservation line 316
  34. lemma OAI.CurrentProjection.measurable_residualObservation line 320
  35. def OAI.CurrentProjection.residualLaw line 325
  36. instance OAI.CurrentProjection.residualLaw_probability line 329
  37. lemma OAI.CurrentProjection.residualLaw_support line 335
  38. lemma OAI.CurrentProjection.residualPosterior_support line 342
  39. lemma OAI.CurrentProjection.reciprocalScale_finite_nonatomicAt line 350
  40. lemma OAI.CurrentProjection.reciprocalScale_finite_eq_real line 357
  41. lemma OAI.CurrentProjection.label_eq_difference_orthogonal line 369
  42. def OAI.CurrentProjection.fixedTargetPosterior line 384
  43. instance OAI.CurrentProjection.fixedTargetPosterior_markov line 390
  44. lemma OAI.CurrentProjection.fixedTargetPosterior_support line 396
  45. lemma OAI.CurrentProjection.mixed_entropy_log_bound_ae line 443
  46. def OAI.CurrentProjection.residualScale line 522
  47. lemma OAI.CurrentProjection.measurable_residualScale line 527
  48. lemma OAI.CurrentProjection.residualScale_lower line 533
  49. lemma OAI.CurrentProjection.fixedTargetPosterior_scale line 537
  50. def OAI.CurrentProjection.residualCube line 546
  51. lemma OAI.CurrentProjection.measurable_residualCube line 553
  52. lemma OAI.CurrentProjection.residualCube_bound line 570
  53. lemma OAI.CurrentProjection.residualCube_finite line 592
  54. lemma OAI.CurrentProjection.residualCube_integral_finite line 597
  55. lemma OAI.CurrentProjection.residualCube_moment line 604
  56. def OAI.CurrentProjection.scalarCube line 644
  57. lemma OAI.CurrentProjection.scalarCube_ball line 647
  58. lemma OAI.CurrentProjection.measurable_scalarCube line 660
  59. def OAI.CurrentProjection.scalarExtended line 666
  60. def OAI.CurrentProjection.scalarDensity line 669
  61. lemma OAI.CurrentProjection.measurable_scalarExtended line 672
  62. lemma OAI.CurrentProjection.measurable_scalarDensity line 677
  63. lemma OAI.CurrentProjection.scalarDensity_finite line 683
  64. lemma OAI.CurrentProjection.scalarDensity_ae_rnDeriv line 687
  65. lemma OAI.CurrentProjection.scalarDensity_ae_limit line 698
  66. lemma OAI.CurrentProjection.scalarDensity_withDensity line 709
  67. lemma OAI.CurrentProjection.kernel_scalarDensity_withDensity line 714
  68. lemma OAI.CurrentProjection.kernel_scalarDensity_ae_limit line 729