OAI/Probability/IsingPerceptron/GaussianFamilyGenerator.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

Gaussian Family Generator.

  1. lemma OAI.IsingPerceptron.gaussianFamily_hasFDerivAt line 16
  2. structure OAI.IsingPerceptron.GaussianFamily line 86
  3. def OAI.IsingPerceptron.familyAverage line 107
  4. def OAI.IsingPerceptron.familyTransform line 110
  5. lemma OAI.IsingPerceptron.familyAverage_measurable line 113
  6. lemma OAI.IsingPerceptron.familyTransform_measurable line 118
  7. lemma OAI.IsingPerceptron.familyAverage_bound line 122
  8. lemma OAI.IsingPerceptron.familyAverage_local_bound line 128
  9. lemma OAI.IsingPerceptron.square_bound line 135
  10. def OAI.IsingPerceptron.GaussianFamily.newX line 142
  11. def OAI.IsingPerceptron.GaussianFamily.newXX line 144
  12. def OAI.IsingPerceptron.GaussianFamily.newT line 148
  13. lemma OAI.IsingPerceptron.GaussianFamily.bound_newX line 152
  14. lemma OAI.IsingPerceptron.GaussianFamily.bound_newXX line 155
  15. lemma OAI.IsingPerceptron.GaussianFamily.bound_newT line 170
  16. lemma OAI.IsingPerceptron.GaussianFamily.spatial_newX line 184
  17. lemma OAI.IsingPerceptron.GaussianFamily.spatial_newXX line 189
  18. lemma OAI.IsingPerceptron.GaussianFamily.measurable_newXX line 199
  19. lemma OAI.IsingPerceptron.GaussianFamily.measurable_newT line 204
  20. def OAI.IsingPerceptron.GaussianFamily.transform line 209
  21. lemma OAI.IsingPerceptron.gaussianTilt_integrable line 243
  22. lemma OAI.IsingPerceptron.gaussianTiltAverage_add line 251
  23. lemma OAI.IsingPerceptron.gaussianTiltAverage_mul_const line 258
  24. lemma OAI.IsingPerceptron.gaussianTiltAverage_const_mul line 262
  25. lemma OAI.IsingPerceptron.gaussianTiltAverage_const line 266
  26. lemma OAI.IsingPerceptron.gaussianTiltAverage_nonneg line 275
  27. lemma OAI.IsingPerceptron.gaussianTiltAverage_mono line 278
  28. lemma OAI.IsingPerceptron.gaussianTiltAverage_sq_le line 285
  29. lemma OAI.IsingPerceptron.familyAverage_add_at line 320
  30. lemma OAI.IsingPerceptron.familyAverage_const_mul line 329
  31. lemma OAI.IsingPerceptron.familyAverage_sum line 333
  32. lemma OAI.IsingPerceptron.GaussianFamily.average_generator line 345
  33. lemma OAI.IsingPerceptron.GaussianFamily.generator_identity line 355
  34. lemma OAI.IsingPerceptron.GaussianFamily.cancellation line 362
  35. lemma OAI.IsingPerceptron.GaussianFamily.squared_newX_le line 379
  36. def OAI.IsingPerceptron.GaussianFamily.terminal line 385
  37. lemma OAI.IsingPerceptron.monotone_fin_cons line 422
  38. lemma OAI.IsingPerceptron.familyAverage_congr_fiber line 437
  39. lemma OAI.IsingPerceptron.familyAverage_weightedSum line 443
  40. structure OAI.IsingPerceptron.VariationCertificate line 460
  41. def OAI.IsingPerceptron.VariationCertificate.prependC line 475
  42. lemma OAI.IsingPerceptron.VariationCertificate.measurable_prependC line 479
  43. lemma OAI.IsingPerceptron.VariationCertificate.nonneg_prependC line 484
  44. lemma OAI.IsingPerceptron.VariationCertificate.bound_prependC line 494
  45. lemma OAI.IsingPerceptron.VariationCertificate.head_le_prependTail line 500
  46. lemma OAI.IsingPerceptron.VariationCertificate.leading_prependC line 506
  47. lemma OAI.IsingPerceptron.VariationCertificate.monotone_prependC line 511
  48. lemma OAI.IsingPerceptron.VariationCertificate.formula_prependC line 523
  49. def OAI.IsingPerceptron.VariationCertificate.prepend line 537
  50. def OAI.IsingPerceptron.VariationCertificate.empty line 550
  51. def OAI.IsingPerceptron.FinTailNonneg line 571
  52. lemma OAI.IsingPerceptron.FinTailNonneg.succ line 574
  53. lemma OAI.IsingPerceptron.FinTailNonneg.total line 580
  54. lemma OAI.IsingPerceptron.finite_tail_pairing_nonneg line 587