HalaszWeightedMeanSquare.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Weighted Schur estimates for the prime-supported polynomials in Halász's mean-value argument. The weight occurs only once in the squared coefficient sum, so a bound for the weighted frequency rows saves the extra logarithm that an unrestricted integer mean-value theorem would lose.

lemma OAI.TwoPointCorrelations.halasz_weighted_symmetric_row_bound line 15
Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszWeightedMeanSquare.lean:15 (same declaration text).

theorem OAI.TwoPointCorrelations.halasz_weighted_mean_square_of_rows line 58

Source documentation

The weighted frequency-row version of the finite mean-value theorem. The coefficients are a i * w i, and only one copy of w remains on the right. Zero weights are allowed.

Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszWeightedMeanSquare.lean:58 (same declaration text).

theorem halasz_weighted_mean_square_of_rows {ι : Type*} (S : Finset ι)
    (a : ι → ℂ) (w freq : ι → ℝ) {T C : ℝ} (hT : 0 < T)
    (hw : ∀ i ∈ S, 0 ≤ w i)
    (hrow : ∀ i ∈ S,
      ∑ j ∈ S, w j * (2 * T / (1 + T ^ 2 * (freq i - freq j) ^ 2)) ≤ C) :
    (∫ t : ℝ, Real.exp (-|t| / T) *
      ‖mrtExponentialPolynomial S (fun i => a i * (w i : ℂ)) freq t‖ ^ 2) ≤
      C * ∑ i ∈ S, ‖a i‖ ^ 2 * w i := by
…

Mentions: OAI.TwoPointCorrelations.mrtExponentialPolynomial

theorem OAI.TwoPointCorrelations.halasz_mean_square_of_weighted_rows line 85

Source documentation

Unweighted time integration costs just the fixed factor exp 1.

Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszWeightedMeanSquare.lean:85 (same declaration text).

theorem halasz_mean_square_of_weighted_rows {ι : Type*} (S : Finset ι)
    (a : ι → ℂ) (w freq : ι → ℝ) {T C : ℝ} (hT : 0 < T)
    (hw : ∀ i ∈ S, 0 ≤ w i)
    (hrow : ∀ i ∈ S,
      ∑ j ∈ S, w j * (2 * T / (1 + T ^ 2 * (freq i - freq j) ^ 2)) ≤ C) :
    (∫ t in -T..T,
      ‖mrtExponentialPolynomial S (fun i => a i * (w i : ℂ)) freq t‖ ^ 2) ≤
      Real.exp 1 * C * ∑ i ∈ S, ‖a i‖ ^ 2 * w i := by
…

Mentions: OAI.TwoPointCorrelations.mrtExponentialPolynomial