OAI/Probability/Perceptron/Cascade/IndexedMarkedPoisson.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptronFreeEnergy.law_count_iid_zip line 13
  2. lemma OAI.SphericalPerceptronFreeEnergy.indexedMarkedPoisson_law line 32
  3. lemma OAI.SphericalPerceptronFreeEnergy.countablePoissonLaw_product_intensity line 67
  4. lemma OAI.SphericalPerceptronFreeEnergy.indexedMarkedPoisson_canonical_law line 85
  5. def OAI.SphericalPerceptronFreeEnergy.IndexedCascadeBase line 97
  6. def OAI.SphericalPerceptronFreeEnergy.IndexedCascadeMarks line 101
  7. instance OAI.SphericalPerceptronFreeEnergy.indexedCascadeBase_nonempty line 105
  8. instance OAI.SphericalPerceptronFreeEnergy.indexedCascadeMarks_nonempty line 110
  9. def OAI.SphericalPerceptronFreeEnergy.indexedCascadeBaseLaw line 116
  10. def OAI.SphericalPerceptronFreeEnergy.indexedCascadeMarksLaw line 124
  11. def OAI.SphericalPerceptronFreeEnergy.indexedCascadeRealize line 130
  12. lemma OAI.SphericalPerceptronFreeEnergy.indexedCascadeRealize_measurable line 137
  13. instance OAI.SphericalPerceptronFreeEnergy.countablePoissonIntensity_sfinite line 146
  14. lemma OAI.SphericalPerceptronFreeEnergy.countablePoissonLaw_eq_canonical line 152
  15. lemma OAI.SphericalPerceptronFreeEnergy.prod_rotate_front line 160
  16. lemma OAI.SphericalPerceptronFreeEnergy.indexedPoissonMeasure_map line 169
  17. lemma OAI.SphericalPerceptronFreeEnergy.prod_interlace_law line 177
  18. lemma OAI.SphericalPerceptronFreeEnergy.indexedCascadeRealize_law line 191