OAI/Probability/GaussianInformation/Inverse/DyadicBins.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.AllScaleInverseVolume.dyadicRadius line 15
  2. lemma OAI.AllScaleInverseVolume.dyadicRadius_pos line 16
  3. lemma OAI.AllScaleInverseVolume.dyadicRadius_antitone line 17
  4. lemma OAI.AllScaleInverseVolume.exists_dyadic_bin line 20
  5. def OAI.AllScaleInverseVolume.clippedLength line 26
  6. def OAI.AllScaleInverseVolume.InBins line 29
  7. lemma OAI.AllScaleInverseVolume.exists_bins line 32
  8. lemma OAI.AllScaleInverseVolume.bins_monotone line 38
  9. def OAI.AllScaleInverseVolume.binGap line 47
  10. lemma OAI.AllScaleInverseVolume.dyadicRadius_sq_gap line 50
  11. lemma OAI.AllScaleInverseVolume.greedy_mem_groupedTube line 61
  12. lemma OAI.AllScaleInverseVolume.measurable_snoc_const line 109
  13. lemma OAI.AllScaleInverseVolume.snoc_update_last line 117