OAI/Probability/Perceptron/Variational/RightDerivativeIntegral.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptronFreeEnergy.rightDerivative_translate line 11
2. lemma OAI.SphericalPerceptronFreeEnergy.integral_hasDerivWithinAt_right line 24
3. lemma OAI.SphericalPerceptronFreeEnergy.sourceConditional_field_continuous line 49
4. lemma OAI.SphericalPerceptronFreeEnergy.sourceConditional_field_slope line 62
5. lemma OAI.SphericalPerceptronFreeEnergy.sourceConditional_field_slope_at line 78
6. lemma OAI.SphericalPerceptronFreeEnergy.sourceConditional_field_direction_bound line 96
7. theorem OAI.SphericalPerceptronFreeEnergy.sourceExpectedPressure_field_right_derivative line 119