OAI/Analysis/HardSphere/Operators/Regularize.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HilbertRegularization.regularize line 17
  2. def OAI.HilbertRegularization.differential line 19
  3. lemma OAI.HilbertRegularization.smooth line 22
  4. lemma OAI.HilbertRegularization.zero line 31
  5. lemma OAI.HilbertRegularization.hasFDerivAt line 34
  6. lemma OAI.HilbertRegularization.sqroot_ge_norm line 48
  7. lemma OAI.HilbertRegularization.differential_apply_le line 51
  8. lemma OAI.HilbertRegularization.differential_le line 64
  9. lemma OAI.HilbertRegularization.fderiv_eq line 69
  10. lemma OAI.HilbertRegularization.lipschitz line 72
  11. lemma OAI.HilbertRegularization.norm_le line 76
  12. lemma OAI.HilbertRegularization.tendsto_regularize line 81