OAI/Analysis/HardSphere/FormDomain/Energy.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HardSphere.Variational.energy line 16
2. def OAI.HardSphere.Variational.gradientPairing line 18
3. lemma OAI.HardSphere.Variational.energy_nonneg line 21
4. lemma OAI.HardSphere.Variational.energy_smul line 24
5. theorem OAI.HardSphere.Variational.rayleigh line 28
6. lemma OAI.HardSphere.Variational.norm_add_real_smul_sq line 46
7. lemma OAI.HardSphere.Variational.energy_add_real_smul line 52
8. lemma OAI.HardSphere.Variational.linear_term_zero line 60
9. theorem OAI.HardSphere.Variational.ground_pairing line 73