OAI/NumberTheory/TwoPoint/Bounds/ActualWordBoolean.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual closed scalar word is precisely the bounded-state Boolean function to which weighted finite-interval comparison applies.

  1. def OAI.TwoPointCorrelations.actualWordBoolean line 15
  2. lemma OAI.TwoPointCorrelations.actualWordBoolean_integer line 26