MRTRestrictedEnergy.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Finite energy bounds on arbitrary measurable frequency classes. They retain the explicit coarse-bin count and permit the coefficient bounds to vary from bin to bin.

lemma OAI.TwoPointCorrelations.mrt_continuous_square_integrable line 14
Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTRestrictedEnergy.lean:14 (same declaration text).
lemma OAI.TwoPointCorrelations.mrt_restricted_square_le_interval line 22
Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTRestrictedEnergy.lean:22 (same declaration text).

theorem OAI.TwoPointCorrelations.mrt_restricted_product_sum_energy line 33

Source documentation

Frequency-restricted Cauchy--Schwarz, with the actual pointwise short-prime bounds and the cofactor energies left explicit.

Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTRestrictedEnergy.lean:33 (same declaration text).

theorem mrt_restricted_product_sum_energy {ι : Type*} (J : Finset ι)
    (Q R : ι → ℝ → ℂ) (hR : ∀ j ∈ J, Continuous (R j))
    (A : ι → ℝ)
    {T : ℝ} (hT : 0 ≤ T) {E : Set ℝ} (hE : E ⊆ Set.Ioc (-T) T)
    (hQ : ∀ j ∈ J, ∀ t ∈ E, ‖Q j t‖ ≤ A j) :
    (∫ t in E, ‖∑ j ∈ J, Q j t * R j t‖ ^ 2) ≤
      (J.card : ℝ) * ∑ j ∈ J, (A j) ^ 2 *
        (∫ t in -T..T, ‖R j t‖ ^ 2) := by
…

theorem OAI.TwoPointCorrelations.mrt_restricted_energy_split line 66
Source documentation
Split a polynomial into a coarse approximation and its actual error on a frequency class, bounding only the error by its full-interval energy.
Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTRestrictedEnergy.lean:66 (same declaration text).
```
theorem mrt_restricted_energy_split (F G : ℝ → ℂ)
    (hF : Continuous F) (hG : Continuous G)
    {T : ℝ} (hT : 0 ≤ T) {E : Set ℝ} (hE : E ⊆ Set.Ioc (-T) T) :
    (∫ t in E, ‖F t‖ ^ 2) ≤
      2 * (∫ t in -T..T, ‖F t - G t‖ ^ 2) + 2 * (∫ t in E, ‖G t‖ ^ 2) := by
…
```