OAI/Geometry/PinnedDistances/PartitionIntegrals.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakPinned.Hierarchy.Depth.sum_by_cells line 15
2. lemma OAI.WeakPinned.Hierarchy.Depth.sum_cell_value line 29
3. lemma OAI.WeakPinned.Bounded.weighted_test_bound line 47
4. lemma OAI.WeakPinned.Bounded.partition_test_bound line 57
5. lemma OAI.WeakPinned.Bounded.cellProb_compl line 85
6. def OAI.WeakPinned.Bounded.meanCellDiscrep line 93
7. lemma OAI.WeakPinned.Bounded.meanCellDiscrep_nonneg line 96
8. lemma OAI.WeakPinned.Bounded.meanCellDiscrep_compl line 99
9. lemma OAI.WeakPinned.Bounded.meanCellDiscrep_small line 108
10. lemma OAI.WeakPinned.Bounded.meanCellDiscrep_young line 121
11. def OAI.WeakPinned.Hierarchy.Depth.transformCell line 163
12. lemma OAI.WeakPinned.Hierarchy.Depth.sum_transformCell line 165
13. lemma OAI.WeakPinned.Bounded.meanCellDiscrep_transform line 184
14. lemma OAI.WeakPinned.Bounded.active_meanDiscrep_bound line 192
15. def OAI.WeakPinned.Bounded.testDiscrep line 220
16. lemma OAI.WeakPinned.Bounded.testDiscrep_nonneg line 223
17. lemma OAI.WeakPinned.Bounded.family_partition_test_bound line 226
18. lemma OAI.WeakPinned.Bounded.grid_test_data line 271
19. lemma OAI.WeakPinned.Bounded.le_unit_integral line 338
20. lemma OAI.WeakPinned.Grid.side_unit_bounds line 356
21. lemma OAI.WeakPinned.Bounded.grid_test_integrated line 379
22. lemma OAI.WeakPinned.Bounded.arch_test_bound line 416