OAI/Probability/SphericalField/Cascade/MarkedMass.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptron.markedDistinctMoment_laplace_factor line 28
2. lemma OAI.SphericalPerceptron.mellin_weighted_identity line 44
3. lemma OAI.SphericalPerceptron.markedDistinctMoment_mellin_factor line 69
4. def OAI.SphericalPerceptron.markedTotalBiasedLaw line 114
5. lemma OAI.SphericalPerceptron.markedStableTotal_momentE line 118
6. lemma OAI.SphericalPerceptron.markedTotalBiasedLaw_probability line 125
7. def OAI.SphericalPerceptron.markedOrderedDistinctMass line 143
8. lemma OAI.SphericalPerceptron.markedOrderedDistinctMass_measurable line 147
9. lemma OAI.SphericalPerceptron.markedOrderedDistinctMass_biased line 152
10. lemma OAI.SphericalPerceptron.markedOrderedDistinctMass_eppf line 174
11. lemma OAI.SphericalPerceptron.normalizedMeasure_map line 190
12. lemma OAI.SphericalPerceptron.markedStableMassKernel_projection line 197