OAI/Analysis/CoulombRadii/FormDomain/HilbertBasisSumSqInner.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Coulomb.hilbertBasis_hasSum_sq_inner line 76
2. lemma OAI.Coulomb.frameOperator_hasSum_diagonal line 87
3. lemma OAI.Coulomb.frameOperator_spectral_hasSum line 110
4. lemma OAI.Coulomb.compactSpectralBasis_quadratic_hasSum line 123