OAI/Probability/Perceptron/Sphere/SphereKernel.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SphericalPerceptronFreeEnergy.joint_gg_crossed_regions_null line 14
  2. theorem OAI.SphericalPerceptronFreeEnergy.weighted_kernel_homogeneous_eq_zero line 47
  3. def OAI.SphericalPerceptronFreeEnergy.sphereKernel line 91
  4. def OAI.SphericalPerceptronFreeEnergy.sphereTail line 93
  5. lemma OAI.SphericalPerceptronFreeEnergy.sphereKernel_nonneg line 96
  6. lemma OAI.SphericalPerceptronFreeEnergy.sphereKernel_le_weight line 104
  7. lemma OAI.SphericalPerceptronFreeEnergy.sphereTail_integrable line 114
  8. lemma OAI.SphericalPerceptronFreeEnergy.sphereKernel_integrable line 127
  9. lemma OAI.SphericalPerceptronFreeEnergy.sphereTail_lower line 136
  10. lemma OAI.SphericalPerceptronFreeEnergy.sphereKernel_row_bound line 145
  11. theorem OAI.SphericalPerceptronFreeEnergy.sphere_equation_unique line 157
  12. lemma OAI.SphericalPerceptronFreeEnergy.sphereTail_nonneg line 199
  13. lemma OAI.SphericalPerceptronFreeEnergy.sphereTail_upper line 203
  14. theorem OAI.SphericalPerceptronFreeEnergy.sphere_equation_support_bound line 211
  15. def OAI.SphericalPerceptronFreeEnergy.realTail line 229
  16. def OAI.SphericalPerceptronFreeEnergy.realCDF line 232
  17. lemma OAI.SphericalPerceptronFreeEnergy.continuous_time_integrable line 234
  18. lemma OAI.SphericalPerceptronFreeEnergy.realTail_integrable line 238
  19. lemma OAI.SphericalPerceptronFreeEnergy.hasDerivWithinAt_max_right line 242
  20. lemma OAI.SphericalPerceptronFreeEnergy.realTail_right_derivative line 253
  21. lemma OAI.SphericalPerceptronFreeEnergy.abs_realTail_sub_le line 296
  22. lemma OAI.SphericalPerceptronFreeEnergy.realTail_continuous line 307
  23. lemma OAI.SphericalPerceptronFreeEnergy.realCDF_monotone line 315
  24. lemma OAI.SphericalPerceptronFreeEnergy.realCDF_integrable line 320
  25. lemma OAI.SphericalPerceptronFreeEnergy.integral_cdf_mul line 324
  26. lemma OAI.SphericalPerceptronFreeEnergy.realTail_lower line 365
  27. def OAI.SphericalPerceptronFreeEnergy.cappedDensity line 374
  28. def OAI.SphericalPerceptronFreeEnergy.cappedA line 377
  29. lemma OAI.SphericalPerceptronFreeEnergy.cappedDensity_continuous line 380
  30. lemma OAI.SphericalPerceptronFreeEnergy.cappedA_hasDerivAt line 387
  31. lemma OAI.SphericalPerceptronFreeEnergy.cappedA_continuous line 394
  32. lemma OAI.SphericalPerceptronFreeEnergy.cappedDensity_eq line 398
  33. lemma OAI.SphericalPerceptronFreeEnergy.realTail_inv_integral line 403