OAI/NumberTheory/TwoPoint/Bounds/ActualRetainedPrefix.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Apply the spectral block estimate to the actual retained correlation. The conclusion records all boundary errors before their asymptotic absorption.

  1. def OAI.TwoPointCorrelations.retainedPrimePrefix line 15
  2. theorem OAI.TwoPointCorrelations.ModFiveThetaInput.eventually_actual_retained_prefix_uniform line 23
  3. theorem OAI.TwoPointCorrelations.ModFiveThetaInput.eventually_actual_retained_prefix line 114