OAI/Probability/Perceptron/Variational/AtomicPairVisitLaw.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SphericalPerceptronFreeEnergy.indexedPairStateWeight line 13
  2. lemma OAI.SphericalPerceptronFreeEnergy.indexedPairStateWeight_measurable line 20
  3. lemma OAI.SphericalPerceptronFreeEnergy.indexedPairStateWeight_mass_le line 31
  4. def OAI.SphericalPerceptronFreeEnergy.indexedPairStateKernel line 46
  5. instance OAI.SphericalPerceptronFreeEnergy.indexedPairStateKernel_finite line 56
  6. lemma OAI.SphericalPerceptronFreeEnergy.indexedPairStateKernel_lintegral line 62
  7. lemma OAI.SphericalPerceptronFreeEnergy.oneDecoratedVisit_bare_eq line 81
  8. lemma OAI.SphericalPerceptronFreeEnergy.twoDecoratedVisit_bare_eq line 88
  9. def OAI.SphericalPerceptronFreeEnergy.twoVisitMass line 99
  10. lemma OAI.SphericalPerceptronFreeEnergy.twoVisitMass_eq line 103
  11. lemma OAI.SphericalPerceptronFreeEnergy.lintegral_indicator_prod line 112
  12. lemma OAI.SphericalPerceptronFreeEnergy.indexedPairStateLaw_eq line 124