OAI/Analysis/HardSphere/Conditioning/PartialAlgebra.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HardSphere.smoothPartial_smooth line 20
  2. def OAI.HardSphere.partialAlgebra line 29
  3. def OAI.HardSphere.smoothLaplacian line 32
  4. lemma OAI.HardSphere.smooth_form_pairing line 35
  5. def OAI.HardSphere.SmoothTest.asSmooth line 45
  6. lemma OAI.HardSphere.SmoothTest.scalar_toLp line 48
  7. lemma OAI.HardSphere.SmoothTest.derivative_toLp line 53
  8. lemma OAI.HardSphere.SmoothTest.form_pairing line 59
  9. def OAI.HardSphere.SmoothTest.freeTest line 65
  10. lemma OAI.HardSphere.SmoothTest.free_resolvent line 74
  11. lemma OAI.HardSphere.SmoothTest.free_generator line 95