OAI/NumberTheory/TwoPoint/Walks/ProhibitedTraceTerms.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Literal centered and designated terms of the prohibited-vertex trace expansion.

  1. def OAI.TwoPointCorrelations.prohibitedCenteredAverage line 13
  2. def OAI.TwoPointCorrelations.prohibitedDesignatedTerm line 22
  3. lemma OAI.TwoPointCorrelations.prohibitedDesignatedTerm_nonneg line 34
  4. theorem OAI.TwoPointCorrelations.prohibited_centering_bound line 49