OAI/Probability/IsingPerceptron/GaussianMomentTest.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

Gaussian Moment Test.

  1. def OAI.IsingPerceptron.gaussianMoment line 16
  2. lemma OAI.IsingPerceptron.gaussianMoment_bound line 19
  3. lemma OAI.IsingPerceptron.gaussianMoment_extension line 31
  4. theorem OAI.IsingPerceptron.jointArray_tendsto_gaussianMoment line 45
  5. def OAI.IsingPerceptron.freshPatternFactor line 74
  6. lemma OAI.IsingPerceptron.freshPatternFactor_bound line 78
  7. lemma OAI.IsingPerceptron.gaussianMoment_cylinder_integral line 96
  8. lemma OAI.IsingPerceptron.freshGaussianReplica_integrable line 110
  9. lemma OAI.IsingPerceptron.freshPatternFactor_pow line 132
  10. lemma OAI.IsingPerceptron.freshPatternFactor_moment line 140
  11. lemma OAI.IsingPerceptron.measurable_random_freshPatternFactor line 168
  12. theorem OAI.IsingPerceptron.freshPatternFactor_array_moment line 180
  13. def OAI.IsingPerceptron.labeledScalarFactor line 249
  14. lemma OAI.IsingPerceptron.measurable_labeledScalarFactor line 253
  15. lemma OAI.IsingPerceptron.labeledScalar_log_bound line 269
  16. lemma OAI.IsingPerceptron.labeledScalarFactor_eq_noise line 276
  17. theorem OAI.IsingPerceptron.labeledScalar_log_recursion line 306
  18. def OAI.IsingPerceptron.rowFactor line 345
  19. lemma OAI.IsingPerceptron.measurable_rowFactor line 348
  20. lemma OAI.IsingPerceptron.rowFactor_bound line 351
  21. lemma OAI.IsingPerceptron.gaussianTransform_one line 368
  22. lemma OAI.IsingPerceptron.exp_gaussianTransform_one line 372
  23. lemma OAI.IsingPerceptron.gaussianTransform_one_bound line 377
  24. lemma OAI.IsingPerceptron.rowFactor_product line 388
  25. lemma OAI.IsingPerceptron.gaussianCoordinates_prefix line 395
  26. lemma OAI.IsingPerceptron.rowFactor_product_coordinates line 401
  27. lemma OAI.IsingPerceptron.residualGaussian_integrable line 418
  28. lemma OAI.IsingPerceptron.gaussianMoment_residual line 439
  29. lemma OAI.IsingPerceptron.labeledCommonDepth_ultrametric line 493
  30. lemma OAI.IsingPerceptron.monotone_labeledCommonDepth_ultrametric line 501
  31. def OAI.IsingPerceptron.diagonalPatch line 519
  32. lemma OAI.IsingPerceptron.measurable_diagonalPatch line 522
  33. lemma OAI.IsingPerceptron.diagonalPatch_arrayBlock line 528
  34. lemma OAI.IsingPerceptron.HasGhirlandaGuerra.patchDiagonal line 533
  35. lemma OAI.IsingPerceptron.diagonalPatch_ultrametric line 553
  36. theorem OAI.IsingPerceptron.cascade_blockLaw_unique line 582