OAI/NumberTheory/TwoPoint/ShortIntervals/MRTBandCostSum.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Summing the actual amplified cofactor cost over the preceding witness bins and current small-polynomial bins.

  1. def OAI.TwoPointCorrelations.mrtMixedBinCost line 14

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTBandCostSum.lean:14 (same declaration text).

  2. lemma OAI.TwoPointCorrelations.mrt_mixed_bin_cost_bound line 22

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTBandCostSum.lean:22 (same declaration text).

  3. theorem OAI.TwoPointCorrelations.mrt_mixed_bin_cost_sum line 45

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTBandCostSum.lean:45 (same declaration text).