OAI/Analysis/CoulombRadii/FieldAnalysis/SlotTensor.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Coulomb.slotTensor line 32
2. lemma OAI.Coulomb.slotTensor_factor line 36
3. lemma OAI.Coulomb.slotTensor_memLp line 48
4. lemma OAI.Coulomb.slotTensor_inner_integral line 59
5. def OAI.Coulomb.slotDeterminant line 80
6. lemma OAI.Coulomb.slotDeterminant_memLp line 84
7. lemma OAI.Coulomb.slotDeterminant_bilinear line 90
8. lemma OAI.Coulomb.slotDeterminant_inner_integral line 105
9. lemma OAI.Coulomb.slotDeterminant_total_norm_sq line 130