OAI/Analysis/CoulombRadii/Packets/PacketBridge.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.NeutralAtom.packetMass_annulus_localization line 15
  2. theorem OAI.NeutralAtom.packet_relative_width_tendsto line 44
  3. theorem OAI.NeutralAtom.packet_clamp_tendsto line 48
  4. theorem OAI.NeutralAtom.eventually_packet_localization line 54
  5. theorem OAI.NeutralAtom.eventually_packet_sandwich line 71
  6. theorem OAI.NeutralAtom.nuclear_clamp_ratio line 91
  7. theorem OAI.NeutralAtom.nuclear_clamp_tendsto line 98
  8. theorem OAI.NeutralAtom.tendsto_of_parameter_sandwich line 108
  9. theorem OAI.NeutralAtom.raw_annulus_tendsto_of_packet_sandwich line 126
  10. theorem OAI.NeutralAtom.rawCount_memLp_measure line 154
  11. theorem OAI.NeutralAtom.expected_raw_annulus_of_packets line 161
  12. theorem OAI.NeutralAtom.conditional_mass_l2 line 193
  13. theorem OAI.NeutralAtom.expectation_of_conditional_mass line 225
  14. theorem OAI.NeutralAtom.scaled_count_l2_bound line 234
  15. theorem OAI.NeutralAtom.integral_comp_measurePreserving line 257
  16. theorem OAI.NeutralAtom.conditional_packet_memLp line 265
  17. theorem OAI.NeutralAtom.conditional_packet_l2_bound line 279
  18. theorem OAI.NeutralAtom.expected_conditional_packet line 314
  19. theorem OAI.NeutralAtom.expected_packet_annulus_from_retained line 330