OAI/Probability/SphericalField/Gibbs/GaussianRows.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SphericalPerceptron.gaussianRows line 24
  2. lemma OAI.SphericalPerceptron.gaussianRows_apply line 29
  3. lemma OAI.SphericalPerceptron.gaussianRows_adjoint_basis line 33
  4. lemma OAI.SphericalPerceptron.gaussianRows_map_stdGaussian line 40
  5. def OAI.SphericalPerceptron.gaussianReplicaTest line 58
  6. lemma OAI.SphericalPerceptron.gaussianReplicaTest_apply line 61
  7. lemma OAI.SphericalPerceptron.freshPattern_moment_covariance_integral line 64
  8. def OAI.SphericalPerceptron.gramCovariance line 94
  9. lemma OAI.SphericalPerceptron.gramCovariance_continuous line 98
  10. def OAI.SphericalPerceptron.gaussianCovarianceKernel line 105
  11. def OAI.SphericalPerceptron.gramReplicaLaw line 118
  12. lemma OAI.SphericalPerceptron.freshPattern_moment_tendsto_of_gram_laws line 123
  13. abbrev OAI.SphericalPerceptron.CompactOverlap line 145
  14. abbrev OAI.SphericalPerceptron.CompactJointOverlap line 146
  15. abbrev OAI.SphericalPerceptron.CompactArray line 147
  16. abbrev OAI.SphericalPerceptron.CompactBlock line 148
  17. def OAI.SphericalPerceptron.compactBlock line 150
  18. lemma OAI.SphericalPerceptron.compactBlock_continuous line 153
  19. lemma OAI.SphericalPerceptron.compact_array_law_subsequence line 156
  20. lemma OAI.SphericalPerceptron.weak_limit_closed_full line 164
  21. def OAI.SphericalPerceptron.compactGGDefect line 177
  22. lemma OAI.SphericalPerceptron.compactGGDefect_continuous line 184