OAI/Probability/ContinuumTransition/ProfileTail.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContinuumTemperature.attraction line 14
2. theorem OAI.ContinuumTemperature.summable_attraction_terms line 17
3. theorem OAI.ContinuumTemperature.attraction_nonneg line 26
4. theorem OAI.ContinuumTemperature.attraction_le line 33
5. theorem OAI.ContinuumTemperature.continuous_attraction line 43
6. theorem OAI.ContinuumTemperature.weighted_scaledKernelProfile_le line 55
7. theorem OAI.ContinuumTemperature.tendsto_weighted_attraction line 69
8. def OAI.ContinuumTemperature.physicalProfile line 97
9. theorem OAI.ContinuumTemperature.coreProfile_eq_zero line 100
10. theorem OAI.ContinuumTemperature.physicalProfile_nonpos line 112
11. theorem OAI.ContinuumTemperature.physicalProfile_isLittleO line 118
12. theorem OAI.ContinuumTemperature.integrable_tsum_real line 132
13. def OAI.ContinuumTemperature.radialWeighted line 148
14. theorem OAI.ContinuumTemperature.radialWeighted_nonneg line 151
15. theorem OAI.ContinuumTemperature.radialWeighted_eq line 157
16. theorem OAI.ContinuumTemperature.integrable_radialWeighted line 164
17. theorem OAI.ContinuumTemperature.integral_radialWeighted_le line 168
18. theorem OAI.ContinuumTemperature.integrable_weighted_attraction line 189