MRTExtraBinCost.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The full extra-bin multiplicity fits the cofactor saving. A crude Cauchy sum suffices; no loss involving the number of original bands occurs.

lemma OAI.TwoPointCorrelations.mrt_extra_bin_card line 12
theorem OAI.TwoPointCorrelations.mrt_extra_bin_cofactor_cost line 32
theorem OAI.TwoPointCorrelations.mrt_extra_bin_saved_cost line 66
Source documentation
The retained cofactor exponent 1/40 pays all extra-bin factors.
```
theorem mrt_extra_bin_saved_cost {L : ℝ} (hL : 1 ≤ L) (hlog : 1 ≤ Real.log L) :
    (L^(-1/40:ℝ))^2 *
      ((((mrtLogBins (mrtExtraPrimeResolution L) (mrtExtraPrimeLower L)
        (mrtExtraPrimeUpper L)).card:ℝ)^2) /
        (mrtExtraPrimeResolution L*(L^(79/80:ℝ))^2)) ≤ 4*L^(-1/80:ℝ) := by
…
```
Mentions: OAI.TwoPointCorrelations.mrtLogBins, OAI.TwoPointCorrelations.mrtExtraPrimeResolution, OAI.TwoPointCorrelations.mrtExtraPrimeLower, OAI.TwoPointCorrelations.mrtExtraPrimeUpper