OAI/Probability/Perceptron/Variational/FocusedShapeProbability.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptronFreeEnergy.cascadeBiasedLaw_zero line 15
  2. lemma OAI.SphericalPerceptronFreeEnergy.stableBlockProbability_eppf_value line 19
  3. lemma OAI.SphericalPerceptronFreeEnergy.cascadeShapeProbability_law line 26
  4. def OAI.SphericalPerceptronFreeEnergy.focusedShapeProbability line 34
  5. def OAI.SphericalPerceptronFreeEnergy.focusedShapeNumerator line 44
  6. lemma OAI.SphericalPerceptronFreeEnergy.focusedShapeProbability_cons line 50
  7. lemma OAI.SphericalPerceptronFreeEnergy.markedBlockProbability_map_measurable line 61
  8. lemma OAI.SphericalPerceptronFreeEnergy.focusedShapeProbability_measurable line 69
  9. lemma OAI.SphericalPerceptronFreeEnergy.focusedShapeNumerator_pos line 95
  10. theorem OAI.SphericalPerceptronFreeEnergy.focusedShapeProbability_integral line 120
  11. lemma OAI.SphericalPerceptronFreeEnergy.descendant_transform_independent line 204
  12. lemma OAI.SphericalPerceptronFreeEnergy.stableIntensity_normalized_mark_projection line 212
  13. lemma OAI.SphericalPerceptronFreeEnergy.stableIntensity_descendant_transform line 224
  14. lemma OAI.SphericalPerceptronFreeEnergy.stablePoisson_descendant_transform line 247
  15. lemma OAI.SphericalPerceptronFreeEnergy.countKernel_parameter_map_measurable line 264
  16. lemma OAI.SphericalPerceptronFreeEnergy.markedStableCountKernel_ae_eq line 284
  17. def OAI.SphericalPerceptronFreeEnergy.DecoratedCascade line 289
  18. instance OAI.SphericalPerceptronFreeEnergy.decoratedCascadeNonempty line 293
  19. def OAI.SphericalPerceptronFreeEnergy.decoratedCascadeLaw line 299
  20. def OAI.SphericalPerceptronFreeEnergy.decoratedCascadeTransform line 306
  21. lemma OAI.SphericalPerceptronFreeEnergy.decoratedCascadeTransform_measurable line 313
  22. theorem OAI.SphericalPerceptronFreeEnergy.decoratedCascadeTransform_law line 328
  23. lemma OAI.SphericalPerceptronFreeEnergy.decoratedCascadeTransform_root_independent line 364
  24. lemma OAI.SphericalPerceptronFreeEnergy.cascadeTotal_log_memLp_two line 376
  25. def OAI.SphericalPerceptronFreeEnergy.decoratedWeightedTotalE line 396
  26. lemma OAI.SphericalPerceptronFreeEnergy.decoratedWeightedTotalE_transform line 404