OAI/Probability/Perceptron/Variational/TiltedVisitKernelLaw.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptronFreeEnergy.pathOneKernel_lintegral line 14
  2. lemma OAI.SphericalPerceptronFreeEnergy.pathPairKernel_lintegral line 36
  3. def OAI.SphericalPerceptronFreeEnergy.atomicVisitKernel line 73
  4. lemma OAI.SphericalPerceptronFreeEnergy.atomicVisitKernel_lintegral line 82
  5. lemma OAI.SphericalPerceptronFreeEnergy.atomicVisitKernel_finite line 89
  6. lemma OAI.SphericalPerceptronFreeEnergy.atomicVisitLaw_lintegral line 96
  7. lemma OAI.SphericalPerceptronFreeEnergy.indexedTiltedProbability_mass_le line 106
  8. lemma OAI.SphericalPerceptronFreeEnergy.indexedTiltedProbability_fixed_measurable line 113
  9. lemma OAI.SphericalPerceptronFreeEnergy.indexedLeafState_fixed_measurable line 125
  10. def OAI.SphericalPerceptronFreeEnergy.indexedOneStateKernel line 133
  11. instance OAI.SphericalPerceptronFreeEnergy.indexedOneStateKernel_finite line 144
  12. lemma OAI.SphericalPerceptronFreeEnergy.indexedOneStateKernel_lintegral line 150
  13. lemma OAI.SphericalPerceptronFreeEnergy.indexedOneStateLaw_eq line 156