OAI/Probability/SphericalField/Poisson/BiasedLaw.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SphericalPerceptron.stableTotalBiasedLaw line 25
  2. lemma OAI.SphericalPerceptron.stableTotalBias_mass line 29
  3. lemma OAI.SphericalPerceptron.stableTotalBiasedLaw_probability line 38
  4. def OAI.SphericalPerceptron.stableOrderedDistinctMass line 49
  5. lemma OAI.SphericalPerceptron.stableOrderedDistinctMass_measurable line 52
  6. lemma OAI.SphericalPerceptron.stableOrderedDistinctMass_biased line 56
  7. lemma OAI.SphericalPerceptron.stableOrderedDistinctMass_eppf line 77
  8. lemma OAI.SphericalPerceptron.stableCountAtom_measurable line 86
  9. lemma OAI.SphericalPerceptron.stablePoissonCount_simple line 99
  10. lemma OAI.SphericalPerceptron.stableMassKernel_atom_eq line 132
  11. lemma OAI.SphericalPerceptron.stableMassAtom_measurable line 143
  12. lemma OAI.SphericalPerceptron.stableMassAtom_measurable_comp line 156
  13. def OAI.SphericalPerceptron.stableBlockProbability line 162
  14. lemma OAI.SphericalPerceptron.stableBlockProbability_measurable line 167
  15. lemma OAI.SphericalPerceptron.stableBlockProbability_moment line 185
  16. lemma OAI.SphericalPerceptron.stableTotalBiasedLaw_absolutelyContinuous line 234
  17. lemma OAI.SphericalPerceptron.stableBlockProbability_ordered line 238
  18. lemma OAI.SphericalPerceptron.stableBlockProbability_eppf line 250