OAI/Analysis/CoulombIonization/RadialBounds/ShellTelescoping.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CoulombAtom.dyadicShell line 20
  2. def OAI.CoulombAtom.dyadicInside line 21
  3. lemma OAI.CoulombAtom.dyadicShell_partition line 25
  4. lemma OAI.CoulombAtom.dyadicShell_sum line 30
  5. lemma OAI.CoulombAtom.dyadicShell_total_sum line 37
  6. lemma OAI.CoulombAtom.dyadicShell_graph_sum line 45
  7. lemma OAI.CoulombAtom.real_inner_sum_left line 52
  8. lemma OAI.CoulombAtom.dyadicShell_residual_sum line 58
  9. lemma OAI.CoulombAtom.oneBodySquareTotal_deriv line 70
  10. lemma OAI.CoulombAtom.oneBodySquareTotal_bound_one line 81
  11. lemma OAI.CoulombAtom.FermionMultiplier.graph_bound_explicit line 90
  12. lemma OAI.CoulombAtom.radialInside_square_graph_bound line 105
  13. def OAI.CoulombAtom.rawExteriorCount line 128
  14. lemma OAI.CoulombAtom.rawExteriorCount_nonneg line 130
  15. lemma OAI.CoulombAtom.rawExteriorCount_le line 132
  16. lemma OAI.CoulombAtom.rawExteriorCount_measurable line 135
  17. lemma OAI.CoulombAtom.rawExteriorCount_integrable line 139
  18. def OAI.CoulombAtom.smoothExteriorWeight line 144
  19. lemma OAI.CoulombAtom.smoothExteriorWeight_nonneg line 146
  20. lemma OAI.CoulombAtom.smoothExteriorWeight_measurable line 150
  21. lemma OAI.CoulombAtom.smoothExteriorWeight_bound line 153
  22. lemma OAI.CoulombAtom.smoothExteriorWeight_integrable line 156
  23. lemma OAI.CoulombAtom.exterior_count_le_smooth_annulus line 160
  24. lemma OAI.CoulombAtom.outer_count_le_smooth line 176
  25. lemma OAI.CoulombAtom.dyadic_gradient_weight_sum line 187
  26. lemma OAI.CoulombAtom.dyadic_gradient_error_sum line 200