OAI/NumberTheory/TwoPoint/Walks/FiveColorBilinear.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Recover a directed short-range kernel from ten tests of its symmetric kernel.

  1. abbrev OAI.TwoPointCorrelations.ForwardColorCode line 13
  2. abbrev OAI.TwoPointCorrelations.sourceColor line 15
  3. abbrev OAI.TwoPointCorrelations.targetColor line 18
  4. lemma OAI.TwoPointCorrelations.color_test_sum line 21
  5. def OAI.TwoPointCorrelations.sourceColorFunction line 47
  6. def OAI.TwoPointCorrelations.targetColorFunction line 51
  7. lemma OAI.TwoPointCorrelations.sourceColorFunction_norm_le line 55
  8. lemma OAI.TwoPointCorrelations.targetColorFunction_norm_le line 63
  9. theorem OAI.TwoPointCorrelations.five_color_bilinear_identity line 71
  10. theorem OAI.TwoPointCorrelations.five_color_bilinear_bound line 112