OAI/Probability/LatticeSurface/Coercivity/GridTrace.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.GridTrace.NatGrid.Vertex line 13
2. def OAI.GridTrace.NatGrid.rect line 15
3. def OAI.GridTrace.NatGrid.grad₁ line 18
4. def OAI.GridTrace.NatGrid.grad₂ line 21
5. def OAI.GridTrace.NatGrid.avg line 24
6. lemma OAI.GridTrace.NatGrid.line_bound line 26
7. lemma OAI.GridTrace.NatGrid.rect_pointwise line 44
8. lemma OAI.GridTrace.NatGrid.rect_pair_bound line 56
9. lemma OAI.GridTrace.NatGrid.avg_diff_identity line 73
10. lemma OAI.GridTrace.NatGrid.avg_subset_bound line 81
11. lemma OAI.GridTrace.NatGrid.rect_avg_bound line 94