OAI/Probability/GaussianInformation/Dyadic/MixtureBounds.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RepeatedLocalization.smoothingWidth line 19
  2. lemma OAI.RepeatedLocalization.smoothingWidth_pos line 21
  3. lemma OAI.RepeatedLocalization.smoothingWidth_tendsto line 25
  4. def OAI.RepeatedLocalization.boxAverage line 28
  5. lemma OAI.RepeatedLocalization.measurable_boxAverage line 32
  6. lemma OAI.RepeatedLocalization.open_box_eventually line 42
  7. lemma OAI.RepeatedLocalization.indicator_le_liminf_boxAverage line 57
  8. def OAI.RepeatedLocalization.mixtureDensity line 79
  9. lemma OAI.RepeatedLocalization.measurable_mixture_kernel line 83
  10. lemma OAI.RepeatedLocalization.measurable_mixtureDensity line 90
  11. lemma OAI.RepeatedLocalization.lintegral_mixtureDensity_mul line 94
  12. lemma OAI.RepeatedLocalization.measure_rpow_bound_of_open line 120
  13. lemma OAI.RepeatedLocalization.lintegral_holder_set_bound line 140
  14. lemma OAI.RepeatedLocalization.bounded_layer_cake line 171
  15. lemma OAI.RepeatedLocalization.bounded_borel_test_of_measure_rpow_bound line 189
  16. def OAI.RepeatedLocalization.exactMixtureLaw line 215
  17. lemma OAI.RepeatedLocalization.exactMixtureLaw_open_bound line 219
  18. lemma OAI.RepeatedLocalization.exactMixtureLaw_borel_test line 260