OAI/Probability/SLEGauge/FiniteProductLimit.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SLEExactGauge.MassVersions.tendsto_finiteMeasure_prod line 18
2. def OAI.SLEExactGauge.MassVersions.localizedFinite line 86
3. lemma OAI.SLEExactGauge.MassVersions.localizedFinite_integral line 94
4. theorem OAI.SLEExactGauge.MassVersions.localizedFinite_tendsto line 101
5. theorem OAI.SLEExactGauge.MassVersions.measure_le_of_nonnegative_compact_tests line 114
6. theorem OAI.SLEExactGauge.MassVersions.bind_le_of_weak_limit line 154
7. theorem OAI.SLEExactGauge.MassVersions.average_prod_le_of_weak_limit line 192
8. theorem OAI.SLEExactGauge.MassVersions.ae_nullSingleton_of_average_prod_diagonal line 210
9. lemma OAI.SLEExactGauge.MassVersions.diagonal_null_of_ac_prod line 234
10. theorem OAI.ExactSLEGreen.actual_mixed_density_product_bound line 256
11. def OAI.ExactSLEGreen.pairKernel line 299
12. lemma OAI.ExactSLEGreen.pairKernel_measurable line 302
13. lemma OAI.ExactSLEGreen.pairKernel_integrable_on_compact line 309
14. instance OAI.ExactSLEGreen.upperArea_atomless line 336
15. lemma OAI.SLEExactGauge.MassVersions.average_density_prod_le line 358
16. lemma OAI.SLEExactGauge.MassVersions.average_localized_density_prod_le line 380
17. lemma OAI.SLEExactGauge.MassVersions.convex_density_moment_le line 406
18. lemma OAI.SLEExactGauge.MassVersions.measurable_localizedFinite line 436
19. def OAI.ExactSLEGreen.actualConvexMass line 460
20. def OAI.ExactSLEGreen.actualConvexDensity line 464
21. lemma OAI.ExactSLEGreen.actualConvexDensity_measurable line 468
22. lemma OAI.ExactSLEGreen.actualConvexMass_density line 477
23. lemma OAI.ExactSLEGreen.actualConvexMass_measurable line 493
24. lemma OAI.ExactSLEGreen.actualConvexMass_finiteOnCompacts line 500
25. lemma OAI.ExactSLEGreen.actualConvexMass_integral line 512
26. lemma OAI.ExactSLEGreen.actual_pair_density_bound line 525
27. theorem OAI.ExactSLEGreen.actualConvexDensity_pair_bound line 544