OAI/Analysis/HardSphere/Geometry/KilledEigenvector.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HardSphere.IsGroundVector.killed_eigenvector line 25
  2. def OAI.HardSphere.regularHeat line 50
  3. lemma OAI.HardSphere.regularHeat_zero line 54
  4. lemma OAI.HardSphere.regularHeat_pos line 57
  5. lemma OAI.HardSphere.regularHeat_add line 61
  6. lemma OAI.HardSphere.regularHeat_commute line 72
  7. lemma OAI.HardSphere.regularHeat_contract line 79
  8. lemma OAI.HardSphere.regularHeat_apply_contract line 94
  9. lemma OAI.HardSphere.regularHeat_generator line 99
  10. lemma OAI.HardSphere.regularHeat_range_bound line 105
  11. lemma OAI.HardSphere.regularHeat_range_lipschitz line 114
  12. lemma OAI.HardSphere.regularHeat_range_continuousOn line 137
  13. lemma OAI.HardSphere.hasDerivWithinAt_Ici_of_slope_right line 141
  14. lemma OAI.HardSphere.regularHeat_range_generator_tendsto line 158
  15. lemma OAI.HardSphere.regularHeat_range_hasDerivWithinAt line 168