OAI/Probability/GaussianInformation/Dyadic/GridSpread.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RepeatedLocalization.euclideanGridCell line 11
2. lemma OAI.RepeatedLocalization.measurableSet_euclideanGridCell line 15
3. lemma OAI.RepeatedLocalization.volume_euclideanGridCell line 26
4. lemma OAI.RepeatedLocalization.euclideanGridCell_disjoint line 42
5. lemma OAI.RepeatedLocalization.dist_le_of_mem_euclideanGridCell line 57
6. lemma OAI.RepeatedLocalization.euclidean_closedBall_volume_le line 80
7. lemma OAI.RepeatedLocalization.grid_ball_count line 88
8. lemma OAI.RepeatedLocalization.exists_mem_euclideanGridCell line 129
9. lemma OAI.RepeatedLocalization.finite_grid_hitting_ball line 137
10. lemma OAI.RepeatedLocalization.measure_ball_le_of_grid line 150