OAI/Analysis/CoulombIonization/Variational/BlockEnergy.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CoulombAtom.tensor_pair_right line 16
2. lemma OAI.CoulombAtom.sum_pair_blocks line 27
3. def OAI.CoulombAtom.blockTensorCross line 54
4. lemma OAI.CoulombAtom.formRepulsion_tensor line 59
5. lemma OAI.CoulombAtom.formEnergy_tensor line 81
6. theorem OAI.CoulombAtom.energy_le_block_insertion line 88
7. lemma OAI.CoulombAtom.tensor_cross_pair_integrable line 101
8. lemma OAI.CoulombAtom.tensor_cross_pair_left_integrable line 110
9. lemma OAI.CoulombAtom.tensor_cross_pair line 121
10. lemma OAI.CoulombAtom.blockCross_inner_integrable line 140
11. lemma OAI.CoulombAtom.blockTensorCross_fubini line 148