OAI/Analysis/CoulombIonization/Variational/PatchBounded.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CoulombAnalysis.tfBallPotential_nonneg line 17
  2. lemma OAI.CoulombAnalysis.tfPatchMinimizer_ae_bound line 23
  3. def OAI.CoulombAnalysis.boundedPatchRepresentative line 36
  4. lemma OAI.CoulombAnalysis.boundedPatchRepresentative_measurable line 39
  5. lemma OAI.CoulombAnalysis.boundedPatchRepresentative_nonneg line 44
  6. lemma OAI.CoulombAnalysis.boundedPatchRepresentative_le line 48
  7. lemma OAI.CoulombAnalysis.boundedPatchRepresentative_support line 56
  8. lemma OAI.CoulombAnalysis.boundedPatchRepresentative_ae line 60
  9. lemma OAI.CoulombAnalysis.boundedPatchRepresentative_ae_ball line 71
  10. lemma OAI.CoulombAnalysis.boundedPatchRepresentative_mass line 78
  11. lemma OAI.CoulombAnalysis.boundedPatchRepresentative_kinetic line 84
  12. lemma OAI.CoulombAnalysis.boundedPatchRepresentative_coulomb line 95
  13. lemma OAI.CoulombAnalysis.boundedPatchRepresentative_field line 107
  14. def OAI.CoulombAnalysis.patchMeasure line 122
  15. lemma OAI.CoulombAnalysis.patch_translation_preserving line 124
  16. lemma OAI.CoulombAnalysis.patch_untranslation_preserving line 134
  17. def OAI.CoulombAnalysis.patchPull line 138
  18. def OAI.CoulombAnalysis.patchPush line 142
  19. lemma OAI.CoulombAnalysis.patchPull_coe line 146
  20. lemma OAI.CoulombAnalysis.patchPush_coe line 151
  21. lemma OAI.CoulombAnalysis.patchPull_push line 156
  22. lemma OAI.CoulombAnalysis.patchPush_pull line 163
  23. lemma OAI.CoulombAnalysis.patchPull_norm line 170
  24. lemma OAI.CoulombAnalysis.patchPull_nonneg line 174
  25. lemma OAI.CoulombAnalysis.patchPush_nonneg line 180
  26. lemma OAI.CoulombAnalysis.patchPull_integral_pair line 186
  27. lemma OAI.CoulombAnalysis.patchPull_coulomb line 198
  28. def OAI.CoulombAnalysis.patchFunctional line 216
  29. lemma OAI.CoulombAnalysis.patchFunctional_pull line 222
  30. theorem OAI.CoulombAnalysis.patchFunctional_existsUnique line 228