OAI/NumberTheory/TwoPoint/Circuits/CircuitSwitchingMass.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The weighted injection bounds the probability of canonical query walks of any specified length. The bound depends on term width and query count, and is independent of the number of terms.

  1. theorem OAI.TwoPointCorrelations.canonicalWalk_probability line 15