OAI/NumberTheory/TwoPoint/Bounds/ActualColumnTrace.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The four trace estimates applied to the actual matrix-path fiber. All caps, singleton costs, padding majorants and witness lengths are discharged.

  1. theorem OAI.TwoPointCorrelations.eventually_actual_column_trace line 16