OAI/Probability/Perceptron/Cascade/CascadeHeat.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SphericalPerceptronFreeEnergy.cascadeHeatWord line 13
2. lemma OAI.SphericalPerceptronFreeEnergy.cascadeHeatWord_nonneg line 17
3. def OAI.SphericalPerceptronFreeEnergy.coordinateDepthField line 27
4. lemma OAI.SphericalPerceptronFreeEnergy.coordinateDepthField_step line 30
5. lemma OAI.SphericalPerceptronFreeEnergy.integral_pi_standardGaussian line 36
6. lemma OAI.SphericalPerceptronFreeEnergy.integrable_pi_standardGaussian line 43
7. lemma OAI.SphericalPerceptronFreeEnergy.coordinateRecursion_eq_backward line 50
8. lemma OAI.SphericalPerceptronFreeEnergy.decoratedAngularFactor_eq_terminal_log line 85
9. lemma OAI.SphericalPerceptronFreeEnergy.coordinateAngularLog_conditional_expectation line 99
10. lemma OAI.SphericalPerceptronFreeEnergy.amplitudeSphereValue_eq_backward line 113