OAI/Probability/SphericalField/Cascade/HeatWord.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SphericalPerceptron.cascadeHeatWord line 15
2. lemma OAI.SphericalPerceptron.cascadeHeatWord_nonneg line 19
3. def OAI.SphericalPerceptron.coordinateDepthField line 29
4. lemma OAI.SphericalPerceptron.coordinateDepthField_step line 32
5. lemma OAI.SphericalPerceptron.integral_pi_standardGaussian line 38
6. lemma OAI.SphericalPerceptron.integrable_pi_standardGaussian line 45
7. lemma OAI.SphericalPerceptron.coordinateRecursion_eq_backward line 52
8. lemma OAI.SphericalPerceptron.decoratedAngularFactor_eq_terminal_log line 87
9. lemma OAI.SphericalPerceptron.coordinateAngularLog_conditional_expectation line 101
10. lemma OAI.SphericalPerceptron.amplitudeSphereValue_eq_backward line 115