OAI/Analysis/CoulombRadii/FieldAnalysis/FirstParticleDensityNonneg.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Coulomb.firstParticleDensity_nonneg line 15
2. lemma OAI.Coulomb.highParticleDensity_nonneg line 20
3. lemma OAI.Coulomb.firstParticleDensity_integral line 26
4. lemma OAI.Coulomb.memLp_fiber_right_ae line 38
5. lemma OAI.Coulomb.first_density_low_high_cap line 45
6. lemma OAI.Coulomb.continuum_rumin_bound line 70
7. lemma OAI.Coulomb.neumannMode_sq_bound line 122
8. lemma OAI.Coulomb.cubeMode_sq_bound line 137
9. lemma OAI.Coulomb.spinCubeMode_sq_bound line 146
10. def OAI.Coulomb.coarseCubeModes line 154
11. lemma OAI.Coulomb.coarseCubeModes_card line 157
12. lemma OAI.Coulomb.coarseCubeModes_card_le line 160
13. lemma OAI.Coulomb.spinCubeMode_diagonal line 171
14. lemma OAI.Coulomb.coarseCubeModes_cutoff line 181