OAI/NumberTheory/TwoPoint/Walks/RetainedFinalScale.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The retained graph contribution at the final fixed parameter choice. The interval exponent is chosen before all affine coefficients.

  1. lemma OAI.TwoPointCorrelations.retained_spectral_scale line 15
  2. theorem OAI.TwoPointCorrelations.ModFiveThetaInput.eventually_canonical_retained_saving line 66
  3. theorem OAI.TwoPointCorrelations.ModFiveThetaInput.eventually_canonical_retained_weighted_saving line 107