OAI/MeasureTheory/FalconerCompletion/Graphs/NearGrid.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Graph energies and pair estimates.

  1. def OAI.GraphLiteralSupport.Attempt4Near.nearGridND line 16
  2. instance OAI.GraphLiteralSupport.Attempt4Near.nearGridND_decidable line 19
  3. lemma OAI.GraphLiteralSupport.Attempt4Near.nearGridND_symm line 22
  4. theorem OAI.GraphLiteralSupport.Attempt4Near.nearGridND_partner_card line 26
  5. def OAI.GraphLiteralSupport.Attempt4Near.nearGridPairND line 39
  6. instance OAI.GraphLiteralSupport.Attempt4Near.nearGridPairND_decidable line 43
  7. lemma OAI.GraphLiteralSupport.Attempt4Near.nearGridPairND_symm line 46
  8. theorem OAI.GraphLiteralSupport.Attempt4Near.nearGridPairND_row_card line 50
  9. theorem OAI.GraphLiteralSupport.Attempt4Near.nearGridPairND_col_card line 66