OAI/Analysis/CoulombIonization/RadialBounds/BarrierOriginalForgettingBarrier.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CoulombBarrier.IsNuclearBarrier.forget_original line 20
2. lemma OAI.CoulombBarrier.event_integral_le_of_square_bounds line 47
3. lemma OAI.CoulombBarrier.bounded_density_square_data_integrable line 65
4. theorem OAI.CoulombBarrier.addedError_expected_mass_le line 75
5. def OAI.CoulombBarrier.barrierErrorExponent line 144
6. lemma OAI.CoulombBarrier.barrierErrorExponent_one_le line 146
7. lemma OAI.CoulombBarrier.barrierErrorExponent_pos line 149
8. lemma OAI.CoulombBarrier.addedError_expected_mass_power line 151
9. lemma OAI.CoulombBarrier.sum_dyadic_powers_le line 184
10. lemma OAI.CoulombBarrier.sum_dyadic_errors_le line 198
11. lemma OAI.CoulombBarrier.total_barrier_budget_tendsto_zero line 207
12. lemma OAI.CoulombBarrier.initial_budget_le_final_radius line 215