OAI/Analysis/CoulombRadii/FieldAnalysis/IntegrableIntegralAeTendsto.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Coulomb.integrable_and_integral_le_of_ae_tendsto line 22
2. lemma OAI.Coulomb.pi_exhaustion line 56
3. lemma OAI.Coulomb.density_power_exhaustion line 67
4. lemma OAI.Coulomb.spinCubeEquiv_full_measurePreserving line 114
5. lemma OAI.Coulomb.H1Vector.spinSpace_memLp line 124
6. lemma OAI.Coulomb.H1Vector.cubeState_full_memLp line 137
7. lemma OAI.Coulomb.cubeState_full_mass line 141
8. lemma OAI.Coulomb.centeredSpinCube_monotone line 154
9. lemma OAI.Coulomb.centeredSpinCube_exhaustion line 161
10. theorem OAI.Coulomb.global_spin_density_power_bound line 172