OAI/Probability/GaussianInformation/Inverse/InverseMoments.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.AllScaleInverseVolume.GreedyEvent line 15
  2. lemma OAI.AllScaleInverseVolume.measurableSet_greedyEvent line 17
  3. lemma OAI.AllScaleInverseVolume.lintegral_greedy_clipped_le line 20
  4. def OAI.AllScaleInverseVolume.rawInverse line 49
  5. lemma OAI.AllScaleInverseVolume.clippedInverse_eq line 52
  6. lemma OAI.AllScaleInverseVolume.measurable_rawInverse line 61
  7. lemma OAI.AllScaleInverseVolume.tendsto_clippedInverse line 69
  8. lemma OAI.AllScaleInverseVolume.lintegral_greedy_raw_le line 84
  9. lemma OAI.AllScaleInverseVolume.rawInverse_perm line 108
  10. lemma OAI.AllScaleInverseVolume.measurePreserving_permutation line 115
  11. lemma OAI.AllScaleInverseVolume.lintegral_raw_le line 127
  12. lemma OAI.AllScaleInverseVolume.inverse_constants line 156