OAI/Analysis/CoulombRadii/FieldAnalysis/FrameOperator.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Coulomb.frameOperator line 68
2. lemma OAI.Coulomb.rankOne_self_continuous line 71
3. lemma OAI.Coulomb.rankOne_integrable line 76
4. lemma OAI.Coulomb.frameOperator_apply line 83
5. lemma OAI.Coulomb.frameOperator_inner line 87
6. lemma OAI.Coulomb.frameOperator_quadratic line 97
7. lemma OAI.Coulomb.frameOperator_nonneg line 110
8. lemma OAI.Coulomb.rankOne_compact line 115
9. lemma OAI.Coulomb.integral_mem_closed_submodule line 119
10. lemma OAI.Coulomb.frameOperator_compact line 130
11. lemma OAI.Coulomb.frameOperator_symmetric line 135
12. lemma OAI.Coulomb.frameOperator_positive line 144
13. lemma OAI.Coulomb.id_sub_frameOperator_positive line 150