OAI/Probability/GaussianInformation/Inverse/ExponentBounds.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.AllScaleInverseVolume.positiveSum line 15
  2. def OAI.AllScaleInverseVolume.negativeSum line 16
  3. lemma OAI.AllScaleInverseVolume.positiveSum_nonneg line 17
  4. lemma OAI.AllScaleInverseVolume.negativeSum_nonneg line 19
  5. lemma OAI.AllScaleInverseVolume.sum_bins line 21
  6. lemma OAI.AllScaleInverseVolume.binGap_sum_le line 29
  7. lemma OAI.AllScaleInverseVolume.dyadicRadius_eq_exp line 45
  8. lemma OAI.AllScaleInverseVolume.grouped_bound_eq_exp line 51
  9. def OAI.AllScaleInverseVolume.stageExponent line 68
  10. def OAI.AllScaleInverseVolume.totalExponent line 71
  11. lemma OAI.AllScaleInverseVolume.stageExponent_sum line 75
  12. lemma OAI.AllScaleInverseVolume.measure_stage_le line 81
  13. def OAI.AllScaleInverseVolume.BinEvent line 117
  14. lemma OAI.AllScaleInverseVolume.measurableSet_inBins line 120
  15. lemma OAI.AllScaleInverseVolume.measurableSet_binEvent line 129
  16. lemma OAI.AllScaleInverseVolume.measure_binEvent_le line 133