OAI/NumberTheory/TwoPoint/Bounds/ShiftedRareDeletion.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The actual rare-event deletion bound is unchanged by separate endpoint shifts for each pair. All arithmetic and circuit budgets are supplied here.

  1. theorem OAI.TwoPointCorrelations.BravermanDepth22Input.eventually_shifted_actual_prohibited_deletion_uniform line 14
  2. theorem OAI.TwoPointCorrelations.BravermanDepth22Input.eventually_shifted_actual_prohibited_deletion line 79
  3. theorem OAI.TwoPointCorrelations.ModFiveThetaInput.eventually_shifted_canonical_rare_deletion_uniform line 109
  4. theorem OAI.TwoPointCorrelations.ModFiveThetaInput.eventually_shifted_canonical_rare_deletion line 195