OAI/Analysis/CoulombRadii/FieldAnalysis/RotatedDensityPower.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Coulomb.flat_fine_density_kinetic_lower_euclidean line 118
2. lemma OAI.Coulomb.commonIsometry_symm line 132
3. lemma OAI.Coulomb.fixed_rotation_fine_density_kinetic_lower line 137
4. def OAI.Coulomb.rotatedDensityPower line 160
5. lemma OAI.Coulomb.rotatedDensityPower_nonneg line 163
6. lemma OAI.Coulomb.rotatedDensityPower_le line 166
7. lemma OAI.Coulomb.rotation_configuration_continuous line 170
8. lemma OAI.Coulomb.rotatedDensityPower_measurable line 181
9. lemma OAI.Coulomb.fineDensityPower_configuration_measurable line 187
10. lemma OAI.Coulomb.fineDensityPower_nonneg line 198
11. lemma OAI.Coulomb.fineDensityPower_bound line 202
12. lemma OAI.Coulomb.weighted_rotatedDensityPower_integrable_prod line 211
13. lemma OAI.Coulomb.weighted_fineDensityPower_integrable line 222
14. lemma OAI.Coulomb.weighted_fineDensityPower_le_angular line 232
15. theorem OAI.Coulomb.fine_density_kinetic_lower line 246