OAI/Analysis/CoulombIonization/Ionization/BarrierInitialEventBarrier.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CoulombAtom.jointMasterPosterior_inner_eq_kernel line 21
  2. lemma OAI.CoulombAtom.jointMasterPosterior_inner_integrable line 34
  3. lemma OAI.CoulombAtom.jointMasterPosterior_inner_event line 46
  4. theorem OAI.CoulombAtom.normalized_inner_event_bound line 62
  5. theorem OAI.CoulombAtom.normalized_inner_event_global_bound line 89
  6. lemma OAI.CoulombAtom.jointMasterPosterior_inner_measurable line 128
  7. lemma OAI.CoulombAtom.threshold_event_mean_ge line 139
  8. theorem OAI.CoulombAtom.actual_initial_pointwise_exceptional line 150