OAI/Analysis/CoulombIonization/ThomasFermi/ContractFunction.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CoulombPauli.memLp_slice_ae line 22
2. def OAI.CoulombPauli.contractFunction line 28
3. lemma OAI.CoulombPauli.contractFunction_slice line 32
4. lemma OAI.CoulombPauli.contractFunction_sq_le line 41
5. lemma OAI.CoulombPauli.contractFunction_memLp line 54
6. def OAI.CoulombPauli.contractL2 line 65
7. lemma OAI.CoulombPauli.contractL2_ae line 68
8. lemma OAI.CoulombPauli.tensorRight_adjoint_eq_contract line 71
9. lemma OAI.CoulombPauli.tensorRight_slice_parseval line 99