OAI/Probability/SphericalField/Heat/Boundary.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptron.heatLog_boundary_hasDerivAt line 23
  2. lemma OAI.SphericalPerceptron.weighted_list_tail_nonneg line 58
  3. def OAI.SphericalPerceptron.heatBoundaryTerms line 80
  4. def OAI.SphericalPerceptron.heatBoundarySum line 89
  5. lemma OAI.SphericalPerceptron.heatBoundarySum_cons line 92
  6. lemma OAI.SphericalPerceptron.heatGenerator_sub line 108
  7. def OAI.SphericalPerceptron.firstHeatGenerator line 116
  8. lemma OAI.SphericalPerceptron.parametricHeatVelocity_boundary line 121
  9. lemma OAI.SphericalPerceptron.heatBoundaryTerms_lower line 157
  10. lemma OAI.SphericalPerceptron.heatBoundaryTerms_ordered line 178
  11. lemma OAI.SphericalPerceptron.heatBoundarySum_nonneg line 197
  12. lemma OAI.SphericalPerceptron.parametricHeatJet_deriv_nonpos line 219