OAI/Analysis/CoulombIonization/FieldAnalysis/SmearTestRecovery.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CoulombNeumann.varthetaScaled_test_bound line 17
  2. lemma OAI.CoulombNeumann.varthetaScaled_test_integrable line 35
  3. theorem OAI.CoulombNeumann.varthetaScaled_test_error line 44
  4. lemma OAI.CoulombNeumann.retainedSmear_test_integrable line 71
  5. lemma OAI.CoulombNeumann.integral_retainedSmear_test line 77
  6. theorem OAI.CoulombNeumann.retainedSmear_test_error line 84
  7. theorem OAI.CoulombNeumann.retainedPatch_test_error line 93
  8. lemma OAI.CoulombNeumann.varthetaScaled_test_zero_of_far line 110
  9. theorem OAI.CoulombNeumann.retainedSmear_local_test_error line 134
  10. lemma OAI.CoulombAtom.radialCut_core_distance line 158
  11. theorem OAI.CoulombAtom.radialCut_retained_test_eq_raw line 171
  12. theorem OAI.CoulombAtom.radialCut_local_smear_error line 207