OAI/Analysis/CoulombIonization/RadialBounds/ShellResidualControl.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CoulombAtom.norm_sub_square_bound line 17
  2. def OAI.CoulombAtom.shellGraphConstant line 22
  3. lemma OAI.CoulombAtom.shellGraphConstant_nonneg line 24
  4. lemma OAI.CoulombAtom.dyadicShell_sum_graph_bound line 27
  5. lemma OAI.CoulombAtom.dyadicShell_residual_square line 45
  6. lemma OAI.CoulombAtom.dyadicShell_residual_le line 58
  7. lemma OAI.CoulombAtom.multiplier_weight_integrable line 74
  8. lemma OAI.CoulombAtom.multiplier_weightedMass_eq_integral line 78
  9. lemma OAI.CoulombAtom.weightedMass_finite_sum line 82
  10. lemma OAI.CoulombAtom.smoothExteriorWeight_count_sub line 88
  11. lemma OAI.CoulombAtom.dyadicShell_total_sum_nonneg line 100
  12. lemma OAI.CoulombAtom.dyadicShell_total_sum_bound line 104
  13. lemma OAI.CoulombAtom.dyadicInside_tendsto line 112
  14. lemma OAI.CoulombAtom.dyadicShell_total_sum_tendsto line 120
  15. lemma OAI.CoulombAtom.dyadicShell_mass_sum_tendsto line 130
  16. lemma OAI.CoulombAtom.sum_linear_inequality line 147
  17. theorem OAI.CoulombAtom.actual_smooth_exterior_number line 154
  18. lemma OAI.CoulombAtom.rawAnnularCount_graph_integrable line 185
  19. theorem OAI.CoulombAtom.actual_exterior_number_absorbed line 190