OAI/Analysis/CoulombRadii/FieldAnalysis/FlatDensityPower.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Coulomb.finiteCubeMeasure_real_univ line 118
2. lemma OAI.Coulomb.finiteCubeMeasure_neZero line 122
3. lemma OAI.Coulomb.translatedGridDensity_nonneg line 131
4. lemma OAI.Coulomb.translatedGridDensity_le line 137
5. lemma OAI.Coulomb.translatedGridDensity_measurable line 145
6. lemma OAI.Coulomb.translatedGridDensity_integrable line 151
7. lemma OAI.Coulomb.translatedGridDensity_power_integrable_translation line 157
8. lemma OAI.Coulomb.flatFineKernel_Jensen line 169
9. lemma OAI.Coulomb.gridCellDensity_power_integrable line 185
10. lemma OAI.Coulomb.translatedGridDensity_power_integrable_space line 205
11. lemma OAI.Coulomb.sameCell1_measurable_pair line 213
12. lemma OAI.Coulomb.translatedGridDensity_measurable_pair line 220
13. lemma OAI.Coulomb.translatedGridDensity_power_integrable_prod line 236
14. lemma OAI.Coulomb.flatFineKernel_measurable line 265
15. lemma OAI.Coulomb.flatFineKernel_nonneg line 272
16. lemma OAI.Coulomb.flatFineKernel_power_integral_le line 275
17. lemma OAI.Coulomb.shifted_grid_count_kinetic_lower line 306
18. lemma OAI.Coulomb.translated_count_measurable line 334
19. lemma OAI.Coulomb.translated_count_integrable line 344
20. def OAI.Coulomb.flatDensityPower line 379
21. lemma OAI.Coulomb.flatDensityPower_nonneg line 383
22. lemma OAI.Coulomb.flatDensityPower_measurable line 390
23. lemma OAI.Coulomb.weighted_flatDensityPower_integrable line 404
24. lemma OAI.Coulomb.weighted_flatDensityPower_le line 418
25. theorem OAI.Coulomb.flat_fine_density_kinetic_lower line 437
26. def OAI.Coulomb.commonIsometry line 493