OAI/Analysis/CoulombIonization/RadialBounds/BarrierTruncationBarrier.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CoulombAtom.innerPotential line 19
  2. lemma OAI.CoulombAtom.innerPotential_eq_tfPotential line 22
  3. lemma OAI.CoulombAtom.innerPotential_nonneg line 30
  4. lemma OAI.CoulombAtom.masterWidth_le_half_radius line 33
  5. lemma OAI.CoulombAtom.masterKernel_zero_inner line 45
  6. lemma OAI.CoulombAtom.inner_master_potential_measurable line 59
  7. lemma OAI.CoulombAtom.inner_master_potential_le line 66
  8. theorem OAI.CoulombAtom.inner_master_potential_raw_bound line 73
  9. lemma OAI.CoulombAtom.inner_master_configuration_integrable line 96
  10. theorem OAI.CoulombAtom.inner_master_configuration_fubini line 113
  11. def OAI.CoulombBarrier.DeterministicLocalBound line 144