OAI/Analysis/HardSphere/Geometry/HeatScalar.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HardSphere.cfc_eigen_apply line 16
  2. def OAI.HardSphere.heatScalar line 41
  3. lemma OAI.HardSphere.heatScalar_smooth line 43
  4. lemma OAI.HardSphere.heatScalar_nonneg line 47
  5. lemma OAI.HardSphere.heatScalar_zero line 50
  6. lemma OAI.HardSphere.heatScalar_of_pos line 52
  7. lemma OAI.HardSphere.heatScalar_resolvent line 60
  8. lemma OAI.HardSphere.heatScalar_add line 67
  9. def OAI.HardSphere.formHeat line 80
  10. lemma OAI.HardSphere.formHeat_add line 83
  11. lemma OAI.HardSphere.formHeat_nonneg line 89
  12. lemma OAI.HardSphere.IsGroundVector.heat_eigenvector line 93
  13. lemma OAI.HardSphere.strong_apply_tendsto line 106
  14. lemma OAI.HardSphere.strong_pow_tendsto line 118
  15. lemma OAI.HardSphere.strong_polynomial_tendsto line 128
  16. lemma OAI.HardSphere.strong_cfc_tendsto line 139
  17. lemma OAI.HardSphere.formHeat_innerRadius_tendsto line 188