OAI/Probability/SphericalField/Entropy/Quantile.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SphericalPerceptron.cappedA_sphere_equation line 17
  2. lemma OAI.SphericalPerceptron.cappedA_eq_integral line 38
  3. theorem OAI.SphericalPerceptron.sphere_self_consistency line 46
  4. def OAI.SphericalPerceptron.boundedCDF line 70
  5. lemma OAI.SphericalPerceptron.boundedCDF_eq line 72
  6. lemma OAI.SphericalPerceptron.boundedCDF_monotone line 77
  7. lemma OAI.SphericalPerceptron.boundedCDF_top line 82
  8. lemma OAI.SphericalPerceptron.boundedCDF_nonneg line 90
  9. lemma OAI.SphericalPerceptron.boundedCDF_le_one line 93
  10. lemma OAI.SphericalPerceptron.boundedCDF_right_continuous line 98
  11. def OAI.SphericalPerceptron.boundedQuantile line 105
  12. lemma OAI.SphericalPerceptron.boundedQuantile_le_iff line 108
  13. lemma OAI.SphericalPerceptron.boundedQuantile_monotone line 124
  14. lemma OAI.SphericalPerceptron.boundedQuantile_measurable line 130
  15. theorem OAI.SphericalPerceptron.boundedQuantile_law line 133
  16. lemma OAI.SphericalPerceptron.map_snd_restrict_prod line 145
  17. lemma OAI.SphericalPerceptron.map_fst_restrict_prod line 155
  18. lemma OAI.SphericalPerceptron.measure_prod_ext_Iic line 164
  19. theorem OAI.SphericalPerceptron.no_crossing_lower_orthant line 187
  20. theorem OAI.SphericalPerceptron.no_crossing_quantile_coupling line 208
  21. theorem OAI.SphericalPerceptron.no_crossing_quantile_bin_integral line 234