OAI/Analysis/CoulombRadii/FieldAnalysis/RetainedFinePower.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Coulomb.retainedFinePower line 126
2. lemma OAI.Coulomb.retainedFinePower_nonneg line 130
3. lemma OAI.Coulomb.retainedFinePower_bound line 135
4. lemma OAI.Coulomb.retainedFinePower_measurable line 140
5. lemma OAI.Coulomb.core_finePower_integrable line 144
6. lemma OAI.Coulomb.retained_fine_kinetic_lower_all line 158
7. theorem OAI.Coulomb.block_retained_fine_kinetic_lower line 172
8. def OAI.Coulomb.retainedFineCoulomb line 199
9. lemma OAI.Coulomb.retainedFineCoulomb_nonneg line 204
10. lemma OAI.Coulomb.retainedFineCoulomb_measurable line 209
11. lemma OAI.Coulomb.ae_block_position_injective line 214
12. lemma OAI.Coulomb.ae_core_fine_pair_bound line 221
13. lemma OAI.Coulomb.core_fineCoulomb_integrable line 238
14. lemma OAI.Coulomb.potentialForm_le_add_const line 252
15. theorem OAI.Coulomb.block_retained_fine_pair_lower line 268
16. theorem OAI.Coulomb.block_retained_fine_energy_lower line 277