OAI/Analysis/CoulombIonization/Fermionic/DyadicPowerSq.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CoulombLT.dyadic_power_sq line 22
  2. lemma OAI.CoulombLT.dyadic_power_cube line 25
  3. lemma OAI.CoulombLT.dyadic_sum_bound line 29
  4. lemma OAI.CoulombLT.dyadic_tsum_bound line 49
  5. lemma OAI.CoulombLT.rpow_two_thirds_cube line 57
  6. lemma OAI.CoulombLT.dyadic_density_bound line 62
  7. abbrev OAI.CoulombLT.Space line 113
  8. lemma OAI.CoulombLT.ball_volume_le line 115
  9. def OAI.CoulombLT.familyDensity line 124
  10. def OAI.CoulombLT.highDensity line 127
  11. lemma OAI.CoulombLT.familyDensity_nonneg line 130
  12. lemma OAI.CoulombLT.highDensity_nonneg line 132
  13. lemma OAI.CoulombLT.familyDensity_integrable line 135
  14. lemma OAI.CoulombLT.highPart_integrable line 141
  15. lemma OAI.CoulombLT.highDensity_integrable line 150
  16. lemma OAI.CoulombLT.familyDensity_pointwise line 154
  17. lemma OAI.CoulombLT.highPart_lintegral line 167
  18. lemma OAI.CoulombLT.highDensity_lintegral line 177
  19. lemma OAI.CoulombLT.density_mass line 205
  20. lemma OAI.CoulombLT.dyadic_kinetic_bound line 216
  21. theorem OAI.CoulombLT.finite_lieb_thirring_lintegral line 261