OAI/NumberTheory/TwoPoint/Bounds/StateCostComparison.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Exact finite-interval comparison for any bounded Q-state event, including the literal density cutoff after the low-degree test.

  1. theorem OAI.TwoPointCorrelations.BravermanDepth22Input.eventually_state_cost_comparison line 14
  2. theorem OAI.TwoPointCorrelations.BravermanDepth22Input.eventually_density_cost_comparison line 69