OAI/Probability/Perceptron/Cascade/WeightedTotalBiasedLaw.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SphericalPerceptronFreeEnergy.weightedTotalBiasedLaw line 24
  2. lemma OAI.SphericalPerceptronFreeEnergy.weightedTotalBiasedLaw_shift line 29
  3. lemma OAI.SphericalPerceptronFreeEnergy.weightedTotalBiasedLaw_add_const line 46
  4. lemma OAI.SphericalPerceptronFreeEnergy.weightedBranchMass_map line 63
  5. def OAI.SphericalPerceptronFreeEnergy.exponentialMarkTilt line 72
  6. def OAI.SphericalPerceptronFreeEnergy.centeredLogMark line 75
  7. lemma OAI.SphericalPerceptronFreeEnergy.centeredLogMark_measurable line 79
  8. lemma OAI.SphericalPerceptronFreeEnergy.exponentialMarkTilt_probability line 83
  9. lemma OAI.SphericalPerceptronFreeEnergy.centeredLogMark_density line 94
  10. lemma OAI.SphericalPerceptronFreeEnergy.weightedTotalBiasedLaw_centered line 115
  11. lemma OAI.SphericalPerceptronFreeEnergy.weightedRootBlock_factor line 122
  12. def OAI.SphericalPerceptronFreeEnergy.cascadeBiasedLaw line 147
  13. lemma OAI.SphericalPerceptronFreeEnergy.cascadeLogTotalMoment_integrable line 151
  14. lemma OAI.SphericalPerceptronFreeEnergy.cascadeBiasedLaw_eq_exponentialTilt line 160
  15. lemma OAI.SphericalPerceptronFreeEnergy.cascadeBiasedLaw_probability line 170
  16. lemma OAI.SphericalPerceptronFreeEnergy.cascadeBiasedLaw_succ_eq_weighted line 176
  17. lemma OAI.SphericalPerceptronFreeEnergy.cascadeRootBlock_factor line 189
  18. def OAI.SphericalPerceptronFreeEnergy.CascadeVisitShape line 209
  19. def OAI.SphericalPerceptronFreeEnergy.cascadeVisitCount line 213
  20. def OAI.SphericalPerceptronFreeEnergy.CascadeVisitShape.Valid line 217
  21. lemma OAI.SphericalPerceptronFreeEnergy.cascadeVisitCount_pos line 221
  22. def OAI.SphericalPerceptronFreeEnergy.cascadeShapeProbability line 235
  23. lemma OAI.SphericalPerceptronFreeEnergy.cascadeShapeProbability_measurable line 242
  24. def OAI.SphericalPerceptronFreeEnergy.cascadeShapeLikelihood line 257
  25. theorem OAI.SphericalPerceptronFreeEnergy.cascadeShapeProbability_integral line 263