OAI/Analysis/CoulombIonization/RadialBounds/BarrierTowerBarrier.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CoulombBarrier.innerSource line 22
  2. def OAI.CoulombBarrier.outerCoefficient line 25
  3. lemma OAI.CoulombBarrier.outerCoefficient_measurable line 27
  4. lemma OAI.CoulombBarrier.outerCoefficient_bound line 31
  5. lemma OAI.CoulombBarrier.outerCoefficient_nonneg line 35
  6. lemma OAI.CoulombBarrier.outerCoefficient_zero line 39
  7. lemma OAI.CoulombBarrier.innerSource_measurable line 42
  8. lemma OAI.CoulombBarrier.innerSource_bound line 49
  9. lemma OAI.CoulombBarrier.conditionalField_innerSource line 67
  10. theorem OAI.CoulombBarrier.original_barrier_source_forgetting line 83
  11. def OAI.CoulombBarrier.outerBarrier line 125
  12. lemma OAI.CoulombBarrier.radialPower_neg_two line 128
  13. lemma OAI.CoulombBarrier.radialPower_neg_three line 134
  14. lemma OAI.CoulombBarrier.outerBarrier_eq_combination line 140
  15. lemma OAI.CoulombBarrier.outerBarrier_contDiffAt line 146
  16. lemma OAI.CoulombBarrier.outerBarrier_laplacian line 152
  17. lemma OAI.CoulombBarrier.outerBarrier_bounds line 161
  18. theorem OAI.CoulombBarrier.outerBarrier_subsolution line 177