OAI/Probability/Perceptron/Variational/IndexedAncestry.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SphericalPerceptronFreeEnergy.indexedVertexDepth line 11
  2. lemma OAI.SphericalPerceptronFreeEnergy.indexedLeafVertex_depth line 17
  3. def OAI.SphericalPerceptronFreeEnergy.indexedSharedVertexDepth line 26
  4. lemma OAI.SphericalPerceptronFreeEnergy.indexedLeafSharedVertex_depth line 30
  5. def OAI.SphericalPerceptronFreeEnergy.indexedCommonDepth line 37
  6. lemma OAI.SphericalPerceptronFreeEnergy.indexedCommonDepth_comm line 41
  7. lemma OAI.SphericalPerceptronFreeEnergy.indexedCommonDepth_self line 47
  8. lemma OAI.SphericalPerceptronFreeEnergy.indexedLeafVertex_eq_iff line 53
  9. lemma OAI.SphericalPerceptronFreeEnergy.indexedLeafSharedVertex_eq_iff line 68
  10. lemma OAI.SphericalPerceptronFreeEnergy.indexedLeafSharedVertex_eq_iff_pair line 76
  11. lemma OAI.SphericalPerceptronFreeEnergy.maskedGaussianCoefficient_sq_prefix line 91
  12. lemma OAI.SphericalPerceptronFreeEnergy.maskedGaussianCoefficient_sq_bound line 103
  13. def OAI.SphericalPerceptronFreeEnergy.gaussianPrefixCovariance line 109
  14. def OAI.SphericalPerceptronFreeEnergy.countableGaussianCovariance line 112
  15. lemma OAI.SphericalPerceptronFreeEnergy.gaussianPrefixCovariance_measurable line 115
  16. lemma OAI.SphericalPerceptronFreeEnergy.countableGaussianCovariance_measurable line 123
  17. lemma OAI.SphericalPerceptronFreeEnergy.gaussianPrefixCovariance_bound line 132
  18. lemma OAI.SphericalPerceptronFreeEnergy.gaussianPrefixCovariance_eventually_eq line 152