MRTMeanSquare.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Finite Dirichlet-polynomial mean squares, using the integrable exponential majorant and its exact quadratic-decay Fourier transform.

def OAI.TwoPointCorrelations.mrtExponentialPolynomial line 14
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTMeanSquare.lean:14 (same declaration text).
lemma OAI.TwoPointCorrelations.mrt_phase_pair line 18
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTMeanSquare.lean:18 (same declaration text).
lemma OAI.TwoPointCorrelations.mrt_weighted_square_expansion line 27
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTMeanSquare.lean:27 (same declaration text).
lemma OAI.TwoPointCorrelations.mrt_weighted_square_integrable line 47
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTMeanSquare.lean:47 (same declaration text).
theorem OAI.TwoPointCorrelations.mrt_weighted_mean_square line 69
Source documentation
Exact finite mean-square formula. This identity is valid for arbitrary real frequencies; separation is needed only for the subsequent bound.
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTMeanSquare.lean:69 (same declaration text).
```
theorem mrt_weighted_mean_square {ι : Type*} (S : Finset ι)
    (a : ι → ℂ) (freq : ι → ℝ) {T : ℝ} (hT : 0 < T) :
    (∫ t : ℝ, Real.exp (-|t| / T) * ‖mrtExponentialPolynomial S a freq t‖ ^ 2) =
      ∑ i ∈ S, ∑ j ∈ S, (a i * conj (a j)).re *
        (2 * T / (1 + T ^ 2 * (freq i - freq j) ^ 2)) := by
…
```
Mentions: OAI.TwoPointCorrelations.mrtExponentialPolynomial

lemma OAI.TwoPointCorrelations.mrt_weighted_mean_square_le line 97

Source documentation

The exact integral is bounded by the positive kernel quadratic form.

Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTMeanSquare.lean:97 (same declaration text).

lemma mrt_weighted_mean_square_le {ι : Type*} (S : Finset ι)
    (a : ι → ℂ) (freq : ι → ℝ) {T : ℝ} (hT : 0 < T) :
    (∫ t : ℝ, Real.exp (-|t| / T) * ‖mrtExponentialPolynomial S a freq t‖ ^ 2) ≤
      ∑ i ∈ S, ∑ j ∈ S, ‖a i‖ * ‖a j‖ *
        (2 * T / (1 + T ^ 2 * (freq i - freq j) ^ 2)) := by
…

Mentions: OAI.TwoPointCorrelations.mrtExponentialPolynomial

lemma OAI.TwoPointCorrelations.mrt_symmetric_row_bound line 112

Source documentation

A symmetric positive kernel is bounded on the squared norm by its largest row sum. The numerical row estimate is proved separately.

Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTMeanSquare.lean:112 (same declaration text).

lemma mrt_symmetric_row_bound {ι : Type*} (S : Finset ι) (K : ι → ι → ℝ)
    (v : ι → ℝ) (C : ℝ) (hK : ∀ i ∈ S, ∀ j ∈ S, 0 ≤ K i j)
    (hsymm : ∀ i ∈ S, ∀ j ∈ S, K i j = K j i)
    (hrow : ∀ i ∈ S, ∑ j ∈ S, K i j ≤ C) :
    (∑ i ∈ S, ∑ j ∈ S, v i * v j * K i j) ≤ C * ∑ i ∈ S, (v i) ^ 2 := by
…

theorem OAI.TwoPointCorrelations.mrt_weighted_mean_square_of_rows line 143
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTMeanSquare.lean:143 (same declaration text).
lemma OAI.TwoPointCorrelations.mrtExponentialPolynomial_continuous line 154
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTMeanSquare.lean:154 (same declaration text).
lemma OAI.TwoPointCorrelations.mrt_unweighted_mean_square_le line 159
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTMeanSquare.lean:159 (same declaration text).
theorem OAI.TwoPointCorrelations.mrt_dirichlet_mean_square line 196
Source documentation
The standard Dirichlet-polynomial mean-value bound, with an absolute constant and no logarithmic loss. Arbitrary complex coefficients are allowed.
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTMeanSquare.lean:196 (same declaration text).
```
theorem mrt_dirichlet_mean_square (N : ℕ) (a : ℕ → ℂ) {T : ℝ} (hT : 0 < T) :
    (∫ t in -T..T,
      ‖mrtExponentialPolynomial (Finset.Ioc 0 N) a (fun n => -Real.log (n : ℝ)) t‖ ^ 2) ≤
      8 * Real.exp 1 * (T + (N : ℝ)) * ∑ n ∈ Finset.Ioc 0 N, ‖a n‖ ^ 2 := by
…
```
Mentions: OAI.TwoPointCorrelations.mrtExponentialPolynomial