OAI/Analysis/HardSphere/Geometry/PositiveTimeSeqTendsto.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HardSphere.positiveTimeSeq_tendsto line 21
2. lemma OAI.HardSphere.SmoothTest.killed_generator line 26
3. lemma OAI.HardSphere.SmoothTest.allowedProjection line 44
4. lemma OAI.HardSphere.SmoothTest.killedLaplace_pairing line 56
5. lemma OAI.HardSphere.killedLaplace_variational line 86
6. lemma OAI.HardSphere.killedLaplace_eq_formResolvent line 110