OAI/Probability/Perceptron/Variational/CovarianceMatrix.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SphericalPerceptronFreeEnergy.CovarianceMatrix line 17
  2. instance OAI.SphericalPerceptronFreeEnergy.covarianceMatrixMeasurableSpace line 19
  3. instance OAI.SphericalPerceptronFreeEnergy.covarianceMatrixBorelSpace line 23
  4. def OAI.SphericalPerceptronFreeEnergy.gaussianCovarianceLaw line 27
  5. lemma OAI.SphericalPerceptronFreeEnergy.gaussianCovarianceLaw_continuous line 30
  6. lemma OAI.SphericalPerceptronFreeEnergy.gaussianCovariance_integral_continuous line 55
  7. lemma OAI.SphericalPerceptronFreeEnergy.gaussianCovariance_integral_tendsto line 61
  8. def OAI.SphericalPerceptronFreeEnergy.gaussianRows line 74
  9. lemma OAI.SphericalPerceptronFreeEnergy.gaussianRows_apply line 79
  10. lemma OAI.SphericalPerceptronFreeEnergy.gaussianRows_adjoint_basis line 83
  11. lemma OAI.SphericalPerceptronFreeEnergy.gaussianRows_map_stdGaussian line 90
  12. def OAI.SphericalPerceptronFreeEnergy.gaussianReplicaTest line 108
  13. lemma OAI.SphericalPerceptronFreeEnergy.gaussianReplicaTest_apply line 111
  14. lemma OAI.SphericalPerceptronFreeEnergy.freshPattern_moment_covariance_integral line 114
  15. def OAI.SphericalPerceptronFreeEnergy.gramCovariance line 144
  16. lemma OAI.SphericalPerceptronFreeEnergy.gramCovariance_continuous line 148
  17. def OAI.SphericalPerceptronFreeEnergy.gaussianCovarianceKernel line 155
  18. def OAI.SphericalPerceptronFreeEnergy.gramReplicaLaw line 168
  19. lemma OAI.SphericalPerceptronFreeEnergy.freshPattern_moment_tendsto_of_gram_laws line 174
  20. abbrev OAI.SphericalPerceptronFreeEnergy.CompactOverlap line 196
  21. abbrev OAI.SphericalPerceptronFreeEnergy.CompactJointOverlap line 197
  22. abbrev OAI.SphericalPerceptronFreeEnergy.CompactArray line 198
  23. abbrev OAI.SphericalPerceptronFreeEnergy.CompactBlock line 199
  24. def OAI.SphericalPerceptronFreeEnergy.compactBlock line 201
  25. lemma OAI.SphericalPerceptronFreeEnergy.compactBlock_continuous line 204
  26. lemma OAI.SphericalPerceptronFreeEnergy.compact_array_law_subsequence line 207
  27. lemma OAI.SphericalPerceptronFreeEnergy.weak_limit_closed_full line 215
  28. def OAI.SphericalPerceptronFreeEnergy.compactGGDefect line 228
  29. lemma OAI.SphericalPerceptronFreeEnergy.compactGGDefect_continuous line 235
  30. lemma OAI.SphericalPerceptronFreeEnergy.compactGGDefect_limit line 247
  31. lemma OAI.SphericalPerceptronFreeEnergy.compactGG_joint_law line 255
  32. lemma OAI.SphericalPerceptronFreeEnergy.integral_continuous_tendsto_of_moments line 294
  33. lemma OAI.SphericalPerceptronFreeEnergy.trial_integrable line 342
  34. lemma OAI.SphericalPerceptronFreeEnergy.tailIntegral_mono line 349
  35. lemma OAI.SphericalPerceptronFreeEnergy.entropy_antitone line 353
  36. def OAI.SphericalPerceptronFreeEnergy.upperRoundedTrial line 359
  37. lemma OAI.SphericalPerceptronFreeEnergy.le_upperRoundedTrial line 375
  38. lemma OAI.SphericalPerceptronFreeEnergy.upperRoundedTrial_sub_le line 379
  39. lemma OAI.SphericalPerceptronFreeEnergy.upperRoundedTrial_finite_range line 388
  40. def OAI.SphericalPerceptronFreeEnergy.terminalTrial line 395