OAI/Probability/SphericalField/Entropy/CappedDensity.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SphericalPerceptron.cappedDensity line 16
  2. def OAI.SphericalPerceptron.cappedA line 19
  3. lemma OAI.SphericalPerceptron.cappedDensity_continuous line 22
  4. lemma OAI.SphericalPerceptron.cappedA_hasDerivAt line 29
  5. lemma OAI.SphericalPerceptron.cappedA_continuous line 36
  6. lemma OAI.SphericalPerceptron.cappedDensity_eq line 40
  7. lemma OAI.SphericalPerceptron.realTail_inv_integral line 45
  8. def OAI.SphericalPerceptron.weightedCDF line 61
  9. lemma OAI.SphericalPerceptron.weightedCDF_fubini line 64
  10. lemma OAI.SphericalPerceptron.realTail_inv_formula line 108
  11. lemma OAI.SphericalPerceptron.cappedA_zero line 135
  12. lemma OAI.SphericalPerceptron.realTail_mul_A line 138
  13. lemma OAI.SphericalPerceptron.realTail_at_top line 168
  14. lemma OAI.SphericalPerceptron.realCDF_at_top line 176
  15. lemma OAI.SphericalPerceptron.weightedCDF_at_top line 186
  16. lemma OAI.SphericalPerceptron.realTail_inv_zero_formula line 196