OAI/Geometry/TranslativeCovering/LatticeAveraging.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LatticeAveraging.Space line 13
2. def OAI.LatticeAveraging.field line 15
3. lemma OAI.LatticeAveraging.measurable_field line 19
4. lemma OAI.LatticeAveraging.one_coset line 28
5. lemma OAI.LatticeAveraging.averaging line 48
6. lemma OAI.LatticeAveraging.periodic line 61
7. def OAI.LatticeAveraging.uniformWindow line 72
8. lemma OAI.LatticeAveraging.normalized_averaging line 75
9. lemma OAI.LatticeAveraging.probability_window line 85
10. lemma OAI.LatticeAveraging.count_integral line 92
11. lemma OAI.LatticeAveraging.covolume_intensity line 100