OAI/NumberTheory/TwoPoint/Bounds/ActiveStateComparison.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Arbitrary functions of the bounded active sets at the trace vertices are compared at every finite interval, using their exact state expansion.

  1. theorem OAI.TwoPointCorrelations.BravermanDepth22Input.eventually_active_state_comparison line 13