OAI/Probability/SphericalField/Heat/Tilt.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SphericalPerceptron.heatTilt line 24
  2. lemma OAI.SphericalPerceptron.heatTilt_zero line 27
  3. lemma OAI.SphericalPerceptron.gaussianAverage_affine line 31
  4. lemma OAI.SphericalPerceptron.gaussian_exp_affine_deriv line 38
  5. lemma OAI.SphericalPerceptron.heatLog_directional_deriv line 72
  6. lemma OAI.SphericalPerceptron.gaussianAverage_add line 88
  7. lemma OAI.SphericalPerceptron.gaussianAverage_smul line 92
  8. lemma OAI.SphericalPerceptron.heatTilt_add line 96
  9. lemma OAI.SphericalPerceptron.heatTilt_smul line 103
  10. lemma OAI.SphericalPerceptron.heatTilt_const line 110
  11. lemma OAI.SphericalPerceptron.heatTilt_nonneg line 117
  12. lemma OAI.SphericalPerceptron.heatTilt_mono line 122
  13. lemma OAI.SphericalPerceptron.heatTilt_abs_le line 129
  14. lemma OAI.SphericalPerceptron.heatTilt_sq line 140
  15. lemma OAI.SphericalPerceptron.Jet3.heatLog_d1 line 156
  16. lemma OAI.SphericalPerceptron.Jet3.heatLog_d1_sq_le line 171
  17. lemma OAI.SphericalPerceptron.gaussian_exp_affine_mul_deriv line 176
  18. lemma OAI.SphericalPerceptron.heatTilt_directional_deriv line 208
  19. lemma OAI.SphericalPerceptron.heatTilt_directional_bound line 219