OAI/Probability/LatticeSurface/Coercivity/GridSpreadTrace.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.GridTrace.Vertex line 18
  2. def OAI.GridTrace.square line 20
  3. def OAI.GridTrace.dist₁ line 23
  4. def OAI.GridTrace.ball line 26
  5. def OAI.GridTrace.mean line 29
  6. def OAI.GridTrace.energy line 32
  7. def OAI.GridTrace.embedNat line 38
  8. lemma OAI.GridTrace.embedNat_injective line 40
  9. lemma OAI.GridTrace.square_map line 49
  10. lemma OAI.GridTrace.sum_square line 66
  11. lemma OAI.GridTrace.embed_dist line 71
  12. lemma OAI.GridTrace.ball_map line 74
  13. lemma OAI.GridTrace.sum_ball line 81
  14. lemma OAI.GridTrace.embed_mem_square line 86
  15. lemma OAI.GridTrace.avg_embed line 91
  16. lemma OAI.GridTrace.sum_nat_Icc line 97
  17. lemma OAI.GridTrace.sum_nat_Ico line 110
  18. lemma OAI.GridTrace.energy_embed line 123
  19. theorem OAI.GridTrace.spread_trace line 136