OAI/Probability/MemoryPrecision/DensityPassage.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MemoryPrecision.fiberSmoothing line 23
  2. lemma OAI.MemoryPrecision.measurable_fiberSmoothing line 26
  3. lemma OAI.MemoryPrecision.lintegral_fiberSmoothing_test line 32
  4. lemma OAI.MemoryPrecision.lintegral_projectionSmoothing_test line 69
  5. lemma OAI.MemoryPrecision.projectionSmoothing_ae_eq_fiberSmoothing line 91
  6. def OAI.MemoryPrecision.boxScalar line 117
  7. lemma OAI.MemoryPrecision.measurable_boxScalar line 120
  8. lemma OAI.MemoryPrecision.lintegral_boxScalar line 123
  9. lemma OAI.MemoryPrecision.box_product_eq line 132
  10. lemma OAI.MemoryPrecision.fiberSmoothing_box_eq_average line 165
  11. lemma OAI.MemoryPrecision.ae_tendsto_fiberSmoothing_box line 187
  12. lemma OAI.MemoryPrecision.projectionLaw_set_bound_of_moment line 226
  13. lemma OAI.MemoryPrecision.projectionLaw_ac_of_moment line 259
  14. lemma OAI.MemoryPrecision.projectionLaw_rnDeriv_moment line 272