OAI/Probability/Perceptron/Cascade/PoissonDensityDerivative.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptronFreeEnergy.summable_nat_mul_pow_div_factorial line 11
2. lemma OAI.SphericalPerceptronFreeEnergy.summable_linear_pow_div_factorial line 20
3. lemma OAI.SphericalPerceptronFreeEnergy.bounded_increment_linear_bound line 28
4. lemma OAI.SphericalPerceptronFreeEnergy.bounded_increment_factorial_summable line 35
5. lemma OAI.SphericalPerceptronFreeEnergy.hasDerivAt_factorial_series line 44
6. def OAI.SphericalPerceptronFreeEnergy.poissonRealMean line 86
7. lemma OAI.SphericalPerceptronFreeEnergy.poissonRealMean_eq_integral line 89
8. lemma OAI.SphericalPerceptronFreeEnergy.hasDerivAt_poissonRealMean line 99