OAI/Combinatorics/SumProduct/Alignment/GlobalPoint01.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.GlobalPointLaw.cell line 25
2. lemma OAI.GlobalPointLaw.mem_cell line 28
3. lemma OAI.GlobalPointLaw.normalized_mem line 33
4. lemma OAI.GlobalPointLaw.exists_unique_partition_cell line 41
5. lemma OAI.GlobalPointLaw.sum_cells line 61
6. def OAI.GlobalPointLaw.riemann line 97
7. lemma OAI.GlobalPointLaw.partition_endpoints line 100
8. lemma OAI.GlobalPointLaw.riemann_error line 111
9. lemma OAI.GlobalPointLaw.prefix_count_error line 156
10. lemma OAI.GlobalPointLaw.interval_filter_card line 175
11. lemma OAI.GlobalPointLaw.cell_card line 191
12. lemma OAI.GlobalPointLaw.prefix_density line 216
13. lemma OAI.GlobalPointLaw.cell_density line 244
14. lemma OAI.GlobalPointLaw.test_integrable line 259
15. lemma OAI.GlobalPointLaw.integral_lipschitz line 266
16. lemma OAI.GlobalPointLaw.continuous_integral line 276
17. def OAI.GlobalPointLaw.empirical line 282
18. def OAI.GlobalPointLaw.frozen line 286
19. lemma OAI.GlobalPointLaw.empirical_frozen_error line 292
20. def OAI.GlobalPointLaw.betaMixture line 332
21. def OAI.GlobalPointLaw.mixedRiemann line 335
22. lemma OAI.GlobalPointLaw.mixed_riemann_error line 339
23. lemma OAI.GlobalPointLaw.frozen_tendsto line 366
24. lemma OAI.GlobalPointLaw.local_mass_limit line 403
25. theorem OAI.GlobalPointLaw.global_point_law line 426
26. theorem OAI.GlobalPointLaw.global_point_law_of_local_haar line 463