EndpointFourierBounds.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

First and second Fourier bounds for signed endpoint masses

def OAI.JointDickman.endpointFourierSum line 12

theorem OAI.JointDickman.endpoint_weight_domination line 18

Source documentation

Pointwise domination of each weighted endpoint coefficient.

theorem endpoint_weight_domination {B n : ℕ} {a X D M : ℝ}
    {γ : ℕ → ℝ} {w : ℝ → ℝ} (hB : 0 < B) (ha : 0 < a) (hX : 0 < X)
    (hD : 0 ≤ D) (_hM : 0 ≤ M) (hn : a*X < n)
    (hγ : |γ n| ≤ D*coefficientWeight B n/((B : ℝ)*n))
    (hw : |w (n/X)| ≤ M) :
    |γ n*w (n/X)| ≤ (D*M/((B : ℝ)*(a*X)))*coefficientWeight B n := by
…

Mentions: OAI.JointDickman.coefficientWeight

theorem OAI.JointDickman.endpoint_fourier_bounds line 36

Source documentation

Finite-window form of both endpoint Fourier estimates.

theorem endpoint_fourier_bounds {B : ℕ} {a b X D M : ℝ}
    (hB : 0 < B) (ha : 0 < a) (hX : 0 < X) (hD : 0 ≤ D) (hM : 0 ≤ M)
    (g : Finset ℕ → ℝ) (w : ℝ → ℝ)
    (hγ : ∀ n ∈ Ioc ⌊a*X⌋₊ ⌊b*X⌋₊,
      |signedSplitProductMass (auxiliaryPrimes B) g n| ≤
        D*coefficientWeight B n/((B : ℝ)*n))
    (hw : ∀ t, |w t| ≤ M) :
    (∀ θ, ‖endpointFourierSum B a b X g w θ‖ ≤
      (D*M/((B : ℝ)*(a*X)))*∑ n ∈ Ioc 0 ⌊b*X⌋₊, coefficientWeight B n) ∧
    (∫ θ in (0 : ℝ)..1, ‖endpointFourierSum B a b X g w θ‖^2) ≤
      (D*M/((B : ℝ)*(a*X)))^2*∑ n ∈ Ioc 0 ⌊b*X⌋₊, coefficientWeight B n^2 := by
…

Mentions: OAI.JointDickman.signedSplitProductMass, OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.coefficientWeight, OAI.JointDickman.endpointFourierSum