OAI/NumberTheory/TwoPoint/ShortIntervals/MRTFinalBandBudget.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The existing MRT first-band budget supplies the alternative needed for the common final-band construction. No separate second-band-size hypothesis is required.

  1. lemma OAI.TwoPointCorrelations.mrt_final_band_budget_alternative line 13
  2. theorem OAI.TwoPointCorrelations.mrt_common_final_band_from_budget line 52