OAI/Probability/SphericalField/Heat/Derivatives.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptron.inv_bcf_bound line 16
2. def OAI.SphericalPerceptron.invBCF line 21
3. lemma OAI.SphericalPerceptron.invBCF_apply line 28
4. lemma OAI.SphericalPerceptron.invBCF_norm_le line 31
5. lemma OAI.SphericalPerceptron.invBCF_hasDerivAt line 36
6. def OAI.SphericalPerceptron.Jet3.heatLogPos line 42
7. def OAI.SphericalPerceptron.Jet3.heatLog line 76
8. lemma OAI.SphericalPerceptron.Jet3.heatLog_f line 79
9. lemma OAI.SphericalPerceptron.gaussianAverage_jet_error line 85
10. lemma OAI.SphericalPerceptron.log_linear_error_le line 96
11. lemma OAI.SphericalPerceptron.gaussianAverage_ge_const line 113
12. lemma OAI.SphericalPerceptron.log_gaussian_generator_error line 118