OAI/Probability/LatticeSurface/Coercivity/GridTraceKernel.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.GridTrace.NatGrid.dist₁ line 13
2. def OAI.GridTrace.NatGrid.ball line 15
3. def OAI.GridTrace.NatGrid.localKernel line 18
4. lemma OAI.GridTrace.NatGrid.local_mem_dist line 22
5. lemma OAI.GridTrace.NatGrid.square_dist line 35
6. lemma OAI.GridTrace.NatGrid.localKernel_nonneg line 51
7. lemma OAI.GridTrace.NatGrid.localKernel_sup line 56
8. lemma OAI.GridTrace.NatGrid.localKernel_sum line 93