OAI/Probability/GaussianInformation/Dyadic/LabelBounds.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RepeatedLocalization.projection_constant_bound line 18
  2. lemma OAI.RepeatedLocalization.lintegral_weighted_average line 68
  3. lemma OAI.RepeatedLocalization.actual_good_score_l2bound line 86
  4. def OAI.RepeatedLocalization.goodLabels line 122
  5. lemma OAI.RepeatedLocalization.measurableSet_goodLabels line 123
  6. lemma OAI.RepeatedLocalization.goodLabels_eq_preimage line 128
  7. lemma OAI.RepeatedLocalization.volume_goodLabels_ne_top line 140
  8. lemma OAI.RepeatedLocalization.volume_goodLabels_pos line 144
  9. def OAI.RepeatedLocalization.labelVolumeConstant line 149
  10. lemma OAI.RepeatedLocalization.labelVolumeConstant_ge_one line 150
  11. lemma OAI.RepeatedLocalization.volume_goodLabels_le line 156
  12. lemma OAI.RepeatedLocalization.normalized_label_tail line 169
  13. def OAI.RepeatedLocalization.averagedScores line 176
  14. lemma OAI.RepeatedLocalization.measurable_averagedScores line 179
  15. lemma OAI.RepeatedLocalization.integrable_score_section line 183
  16. lemma OAI.RepeatedLocalization.averagedScores_bounds line 189
  17. lemma OAI.RepeatedLocalization.averagedScores_sum line 200
  18. def OAI.RepeatedLocalization.goodRegion line 208
  19. lemma OAI.RepeatedLocalization.measurableSet_goodRegion line 210
  20. lemma OAI.RepeatedLocalization.reference_goodRegion_volume line 213
  21. lemma OAI.RepeatedLocalization.gaussianRows_probability line 218
  22. lemma OAI.RepeatedLocalization.finite_reference_scores line 222
  23. lemma OAI.RepeatedLocalization.weightedProjectionMoment_toReal line 246
  24. def OAI.RepeatedLocalization.blockInformationConstant line 256
  25. lemma OAI.RepeatedLocalization.blockInformationConstant_pos line 257