OAI/Probability/SphericalField/Heat/Logarithm.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SphericalPerceptron.heatLog line 16
  2. lemma OAI.SphericalPerceptron.heatLog_abs_le line 19
  3. lemma OAI.SphericalPerceptron.heatLog_continuous line 33
  4. def OAI.SphericalPerceptron.heatLogBCF line 40
  5. lemma OAI.SphericalPerceptron.heatLogBCF_coe line 46
  6. lemma OAI.SphericalPerceptron.exp_heatLog line 49
  7. lemma OAI.SphericalPerceptron.heatLog_zero line 55
  8. lemma OAI.SphericalPerceptron.heatLog_semigroup line 60
  9. structure OAI.SphericalPerceptron.Jet3 line 72
  10. lemma OAI.SphericalPerceptron.Jet3.deriv_eq line 81
  11. lemma OAI.SphericalPerceptron.Jet3.deriv2_eq line 82
  12. lemma OAI.SphericalPerceptron.Jet3.deriv3_eq line 85
  13. lemma OAI.SphericalPerceptron.Jet3.contDiff line 89
  14. def OAI.SphericalPerceptron.Jet3.gaussianAverage line 100
  15. lemma OAI.SphericalPerceptron.Jet3.gaussianAverage_norms line 109
  16. def OAI.SphericalPerceptron.Jet3.exp line 117