OAI/Analysis/CoulombRadii/LimitTheory/UniformGroundStateCountControl.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.NeutralAtom.rawExpectation_perm line 13
  2. theorem OAI.NeutralAtom.integrable_siteWeight line 29
  3. theorem OAI.NeutralAtom.rawExpectation_site line 40
  4. theorem OAI.NeutralAtom.rawExpectation_count_factor line 48
  5. theorem OAI.NeutralAtom.density_integral_eq_first_site line 67
  6. theorem OAI.NeutralAtom.rawExpectation_count_eq_density line 94
  7. theorem OAI.NeutralAtom.exceptional_event_bound line 100
  8. theorem OAI.NeutralAtom.expectation_error_bound line 124
  9. theorem OAI.NeutralAtom.expectation_tendsto_of_good_events line 163
  10. theorem OAI.NeutralAtom.rawCount_nonneg line 183
  11. theorem OAI.NeutralAtom.rawCount_le_number line 189
  12. theorem OAI.NeutralAtom.measurable_rawCount line 198
  13. theorem OAI.NeutralAtom.integrable_count_squared_weight line 204
  14. theorem OAI.NeutralAtom.rawExpectation_count_squared_le line 217
  15. theorem OAI.NeutralAtom.normalized_count_l2_le_number line 230
  16. def OAI.NeutralAtom.UniformGroundStateCountControl line 240
  17. def OAI.NeutralAtom.rawLaw line 251
  18. theorem OAI.NeutralAtom.integral_rawLaw line 254
  19. theorem OAI.NeutralAtom.rawLaw_isProbability line 265
  20. theorem OAI.NeutralAtom.rawCount_memLp line 272
  21. theorem OAI.NeutralAtom.rawExpectation_sphere_eq_zero line 281
  22. def OAI.NeutralAtom.packetExponent line 287
  23. def OAI.NeutralAtom.packetWidth line 289
  24. def OAI.NeutralAtom.packetKernel line 292
  25. theorem OAI.NeutralAtom.packetWidth_pos line 296
  26. theorem OAI.NeutralAtom.packetKernel_eq_wavepacket_sq line 302
  27. theorem OAI.NeutralAtom.packetKernel_nonneg line 314
  28. theorem OAI.NeutralAtom.integral_packetKernel line 320
  29. theorem OAI.NeutralAtom.integrable_packetKernel line 331
  30. theorem OAI.NeutralAtom.packetKernel_support line 339
  31. theorem OAI.NeutralAtom.packetWidth_le line 352
  32. theorem OAI.NeutralAtom.packetKernel_relative_support line 365
  33. theorem OAI.NeutralAtom.packetKernel_clamped_support line 379
  34. def OAI.NeutralAtom.packetMass line 390
  35. theorem OAI.NeutralAtom.packetMass_nonneg line 394
  36. theorem OAI.NeutralAtom.packetMass_le_rawCount line 400