OAI/Probability/GaussianInformation/Inverse/ClippedMoments.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.AllScaleInverseVolume.integerWeight line 15
  2. lemma OAI.AllScaleInverseVolume.tsum_integerWeight line 16
  3. lemma OAI.AllScaleInverseVolume.tsum_prod_integerWeight line 25
  4. def OAI.AllScaleInverseVolume.clippedInverse line 50
  5. def OAI.AllScaleInverseVolume.binInverseExponent line 52
  6. def OAI.AllScaleInverseVolume.baseExponent line 54
  7. lemma OAI.AllScaleInverseVolume.measurable_clippedInverse line 57
  8. lemma OAI.AllScaleInverseVolume.clipped_length_inv_le line 63
  9. lemma OAI.AllScaleInverseVolume.clippedInverse_le_bin line 76
  10. lemma OAI.AllScaleInverseVolume.abs_bins_sum line 97
  11. lemma OAI.AllScaleInverseVolume.integerWeight_eq_exp line 104
  12. lemma OAI.AllScaleInverseVolume.prod_integerWeight_eq_exp line 117
  13. lemma OAI.AllScaleInverseVolume.exponent_small_negative line 124
  14. lemma OAI.AllScaleInverseVolume.exponent_large_negative line 133
  15. lemma OAI.AllScaleInverseVolume.lintegral_bin_clipped_le line 140