OAI/NumberTheory/TwoPoint/Bounds/ShiftedDegreeDeletion.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Pair-dependent endpoint shifts do not change the degree cost.

  1. theorem OAI.TwoPointCorrelations.BravermanDepth22Input.eventually_shifted_tuple_degree_deletion line 12