OAI/Probability/SphericalField/Cascade/TotalLaw.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptron.poissonWeightedTotal_law line 23
  2. def OAI.SphericalPerceptron.StableCascade line 63
  3. instance OAI.SphericalPerceptron.stableCascadeNonempty line 67
  4. def OAI.SphericalPerceptron.cascadeTotalE line 72
  5. lemma OAI.SphericalPerceptron.cascadeTotalE_measurable line 77
  6. def OAI.SphericalPerceptron.cascadeTotal line 84
  7. lemma OAI.SphericalPerceptron.cascadeTotal_measurable line 86
  8. def OAI.SphericalPerceptron.cascadeLaw line 89
  9. lemma OAI.SphericalPerceptron.poissonWeightedTotal_identDistrib line 94
  10. lemma OAI.SphericalPerceptron.poissonWeightedTotal_pos line 106
  11. lemma OAI.SphericalPerceptron.poissonWeightedTotal_rpow_integrable line 115
  12. lemma OAI.SphericalPerceptron.poissonRandomMeasureLaw_ae_ae line 130
  13. lemma OAI.SphericalPerceptron.cascadeTotal_succ_eq line 136
  14. theorem OAI.SphericalPerceptron.cascadeTotal_regular line 159