OAI/Analysis/CoulombIonization/Ionization/IntegratedStability.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CoulombAtom.linearMap_ne_zero_ae line 16
  2. lemma OAI.CoulombAtom.configuration_ae_nonsingular line 33
  3. lemma OAI.CoulombAtom.nuclear_hardy line 61
  4. lemma OAI.CoulombAtom.integrated_potential_stability line 76
  5. theorem OAI.CoulombAtom.formEnergy_uniform_lower_bound line 131
  6. def OAI.CoulombAtom.DeficitSecants line 150
  7. theorem OAI.CoulombAtom.DeficitSecants.monotoneOn line 154
  8. theorem OAI.CoulombAtom.grid_increment_error line 163
  9. theorem OAI.CoulombAtom.deficit_secant_increments_tendsto line 212
  10. theorem OAI.CoulombAtom.deficit_secant_energy_tendsto line 252
  11. def OAI.CoulombAtom.limitPriceEnergy line 295
  12. def OAI.CoulombAtom.limitDeficit line 297
  13. theorem OAI.CoulombAtom.hasDerivAt_limitPriceEnergy line 299
  14. theorem OAI.CoulombAtom.deficitSecants_limitPriceEnergy line 311
  15. def OAI.CoulombAtom.limitSectorEnergy line 332
  16. theorem OAI.CoulombAtom.limitPriceEnergy_add line 334
  17. theorem OAI.CoulombAtom.continuous_limitPriceEnergy line 341
  18. theorem OAI.CoulombAtom.continuous_limitDeficit line 344
  19. theorem OAI.CoulombAtom.continuous_limitSectorEnergy line 347
  20. theorem OAI.CoulombAtom.limitDeficit_strictMonoOn line 350
  21. theorem OAI.CoulombAtom.limitDeficit_target line 355
  22. theorem OAI.CoulombAtom.limitSectorEnergy_target line 361
  23. theorem OAI.CoulombAtom.priced_energy_limits line 375
  24. theorem OAI.CoulombAtom.tendsto_of_deficit_brackets line 388
  25. def OAI.CoulombAtom.PriceMinimizes line 429
  26. def OAI.CoulombAtom.priceEnergy line 432
  27. theorem OAI.CoulombAtom.priceEnergy_eq_of_minimizes line 434
  28. theorem OAI.CoulombAtom.exists_priceMinimizes line 446
  29. theorem OAI.CoulombAtom.priceMinimizes_antitone line 464
  30. theorem OAI.CoulombAtom.priceMinimizes_strict_binding line 471
  31. theorem OAI.CoulombAtom.priceEnergy_secants line 477
  32. theorem OAI.CoulombAtom.priceEnergy_neutral_bounds line 486
  33. def OAI.CoulombAtom.scaledPrice line 495
  34. def OAI.CoulombAtom.scaledDeficit line 499
  35. theorem OAI.CoulombAtom.rpow_seven_thirds line 501
  36. theorem OAI.CoulombAtom.scaledDeficit_mul line 505
  37. theorem OAI.CoulombAtom.scaledPrice_sector line 510
  38. theorem OAI.CoulombAtom.scaledPrice_secants line 518
  39. theorem OAI.CoulombAtom.scaledPrice_zero_bounds line 539
  40. theorem OAI.CoulombAtom.scaledPrice_nonpos line 552
  41. theorem OAI.CoulombAtom.scaledPrice_limits line 559
  42. theorem OAI.CoulombAtom.fixed_sector_limit_of_priced_deficit line 591
  43. theorem OAI.CoulombAtom.energy_uniform_lower_bound line 630
  44. theorem OAI.CoulombAtom.energy_range_bddBelow line 641
  45. theorem OAI.CoulombAtom.quantum_exists_priceMinimizes line 647