OAI/Analysis/CoulombRadii/FieldAnalysis/CorePointMeasurable.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Coulomb.potentialForm_coreSlice_point_aestronglyMeasurable line 14
2. lemma OAI.Coulomb.coreScreenedField_slice_point_aestronglyMeasurable line 30
3. lemma OAI.Coulomb.patchTFScreenedField_slice_aestronglyMeasurable line 51
4. lemma OAI.Coulomb.ae_position_ne line 67
5. def OAI.Coulomb.patchFieldTransferError line 94
6. lemma OAI.Coulomb.patchFieldTransferError_aestronglyMeasurable line 100
7. def OAI.Coulomb.patchTransferRemainder line 109
8. lemma OAI.Coulomb.patchTransferRemainder_weight_integrable line 118
9. lemma OAI.Coulomb.patchFieldTransferError_ae_bound line 136
10. theorem OAI.Coulomb.patchFieldTransferError_integrable_mean line 155