MRTExtraMissing.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The actual additional-band sieve controls the dyadic coefficient error before any frequency partition or sampling.

lemma OAI.TwoPointCorrelations.mrt_single_band_not_typical line 15
lemma OAI.TwoPointCorrelations.mrt_supported_eq_single_band line 19
lemma OAI.TwoPointCorrelations.mrt_avoiding_dyadic_density line 33
theorem OAI.TwoPointCorrelations.mrt_extra_missing_energy line 43
Source documentation
One additional missing-band error costs only its actual density, with a constant independent of the number of original typical bands.
```
theorem mrt_extra_missing_energy : ∃ C : ℝ, 0 < C ∧
    ∀ᶠ L : ℝ in Filter.atTop, ∀ (F : ℕ → ℂ), OneBounded F →
    ∀ (N : ℕ), Real.exp L ≤ N → ∀ T : ℝ, 0 < T →
      (∫ t in -T..T, ‖mrtDyadicPolynomial F N t -
        mrtDyadicPolynomial (mrtSupportedCoefficient
          (mrtPrimeBand (mrtExtraPrimeLower L) (mrtExtraPrimeUpper L)) F) N t‖^2) ≤
        C*(T/N+1)*(Real.log L/L^(1/80:ℝ)) := by
…
```
Mentions: OAI.TwoPointCorrelations.OneBounded, OAI.TwoPointCorrelations.mrtDyadicPolynomial, OAI.TwoPointCorrelations.mrtSupportedCoefficient, OAI.TwoPointCorrelations.mrtPrimeBand, OAI.TwoPointCorrelations.mrtExtraPrimeLower, OAI.TwoPointCorrelations.mrtExtraPrimeUpper