OAI/Probability/Perceptron/Cascade/WeightedCDF.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SphericalPerceptronFreeEnergy.weightedCDF line 14
  2. lemma OAI.SphericalPerceptronFreeEnergy.weightedCDF_fubini line 17
  3. lemma OAI.SphericalPerceptronFreeEnergy.realTail_inv_formula line 61
  4. lemma OAI.SphericalPerceptronFreeEnergy.cappedA_zero line 88
  5. lemma OAI.SphericalPerceptronFreeEnergy.realTail_mul_A line 91
  6. lemma OAI.SphericalPerceptronFreeEnergy.realTail_at_top line 121
  7. lemma OAI.SphericalPerceptronFreeEnergy.realCDF_at_top line 129
  8. lemma OAI.SphericalPerceptronFreeEnergy.weightedCDF_at_top line 139
  9. lemma OAI.SphericalPerceptronFreeEnergy.realTail_inv_zero_formula line 149
  10. theorem OAI.SphericalPerceptronFreeEnergy.cappedA_sphere_equation line 185
  11. lemma OAI.SphericalPerceptronFreeEnergy.cappedA_eq_integral line 206
  12. theorem OAI.SphericalPerceptronFreeEnergy.sphere_self_consistency line 214
  13. def OAI.SphericalPerceptronFreeEnergy.boundedCDF line 238
  14. lemma OAI.SphericalPerceptronFreeEnergy.boundedCDF_eq line 240
  15. lemma OAI.SphericalPerceptronFreeEnergy.boundedCDF_monotone line 245
  16. lemma OAI.SphericalPerceptronFreeEnergy.boundedCDF_top line 250
  17. lemma OAI.SphericalPerceptronFreeEnergy.boundedCDF_nonneg line 258
  18. lemma OAI.SphericalPerceptronFreeEnergy.boundedCDF_le_one line 261
  19. lemma OAI.SphericalPerceptronFreeEnergy.boundedCDF_right_continuous line 266
  20. def OAI.SphericalPerceptronFreeEnergy.boundedQuantile line 273
  21. lemma OAI.SphericalPerceptronFreeEnergy.boundedQuantile_le_iff line 276
  22. lemma OAI.SphericalPerceptronFreeEnergy.boundedQuantile_monotone line 292
  23. lemma OAI.SphericalPerceptronFreeEnergy.boundedQuantile_measurable line 298
  24. theorem OAI.SphericalPerceptronFreeEnergy.boundedQuantile_law line 301
  25. lemma OAI.SphericalPerceptronFreeEnergy.map_snd_restrict_prod line 313
  26. lemma OAI.SphericalPerceptronFreeEnergy.map_fst_restrict_prod line 323
  27. lemma OAI.SphericalPerceptronFreeEnergy.measure_prod_ext_Iic line 332
  28. theorem OAI.SphericalPerceptronFreeEnergy.no_crossing_lower_orthant line 355
  29. theorem OAI.SphericalPerceptronFreeEnergy.no_crossing_quantile_coupling line 376
  30. theorem OAI.SphericalPerceptronFreeEnergy.no_crossing_quantile_bin_integral line 402
  31. instance OAI.SphericalPerceptronFreeEnergy.(instance at line 432) line 432