OAI/Analysis/CoulombRadii/RandomFields/ConditionalDensity.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.NeutralAtom.continuous_packetKernel line 13
2. theorem OAI.NeutralAtom.measurable_packetMass line 24
3. theorem OAI.NeutralAtom.packetMass_le_number line 32
4. theorem OAI.NeutralAtom.packetMass_memLp line 38
5. def OAI.NeutralAtom.rawPacketDensity line 48
6. theorem OAI.NeutralAtom.rawPacketDensity_nonneg line 52
7. theorem OAI.NeutralAtom.rawPacketDensity_integrable line 57
8. theorem OAI.NeutralAtom.rawPacketDensity_mass line 62
9. theorem OAI.NeutralAtom.continuous_rawPacketDensity line 70
10. theorem OAI.NeutralAtom.rawPacketDensity_prod_integrable line 85
11. def OAI.NeutralAtom.mixturePacketDensity line 102
12. theorem OAI.NeutralAtom.mixturePacketDensity_integrable line 106
13. theorem OAI.NeutralAtom.mixturePacketDensity_nonneg line 113
14. theorem OAI.NeutralAtom.mixturePacketDensity_mass line 118
15. theorem OAI.NeutralAtom.packetWidth_lower line 130
16. theorem OAI.NeutralAtom.compact_packet_function_bound line 141
17. theorem OAI.NeutralAtom.packetKernel_bound line 148
18. theorem OAI.NeutralAtom.rawPacketDensity_bound line 159
19. theorem OAI.NeutralAtom.rawPacketDensity_integrable_configuration line 169
20. theorem OAI.NeutralAtom.mixturePacketDensity_bounded line 183
21. theorem OAI.NeutralAtom.rawPacketDensity_setIntegral line 197
22. theorem OAI.NeutralAtom.rawPacketDensity_prod_restrict_integrable line 205
23. theorem OAI.NeutralAtom.mixturePacketDensity_setIntegral line 222
24. def OAI.NeutralAtom.conditionalPacketDensity line 235
25. theorem OAI.NeutralAtom.conditionalPacketDensity_mass line 241
26. theorem OAI.NeutralAtom.conditionalPacketDensity_nonneg line 249
27. theorem OAI.NeutralAtom.conditionalPacketDensity_bounded line 256
28. theorem OAI.NeutralAtom.conditionalPacketDensity_eq_condExp line 265
29. theorem OAI.NeutralAtom.conditionalPacketDensity_annulus_eq_condExp line 281