OAI/NumberTheory/TwoPoint/ShortIntervals/MRTLargeValues.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TwoPointCorrelations.mrt_dirichlet_derivative_mass line 13

   Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTLargeValues.lean:13 (same declaration text).

2. theorem OAI.TwoPointCorrelations.mrt_dirichlet_separated_samples line 30

   Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTLargeValues.lean:30 (same declaration text).

3. theorem OAI.TwoPointCorrelations.mrt_prime_separated_moment line 79

   Source documentation

   The sampled 2r-th moment of an actual prime Dirichlet polynomial. The extra logarithmic square comes only from sampling the continuous moment on unit intervals.

   Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTLargeValues.lean:79 (same declaration text).

   theorem mrt_prime_separated_moment (P : Finset ℕ) (a : ℕ → ℂ)
       (N r : ℕ) (hP : ∀ p ∈ P, p.Prime) (hN : ∀ p ∈ P, p ≤ N)
       (S : Finset ℝ) {T : ℝ} (hT : 0 ≤ T)
       (hS : ∀ t ∈ S, |t| ≤ T)
       (hsep : ∀ x ∈ S, ∀ y ∈ S, x ≠ y → 1 ≤ |x - y|) :
       (∑ t ∈ S, ‖mrtExponentialPolynomial P a (fun p => -Real.log (p : ℝ)) t‖ ^
         (2 * r)) ≤
         8 * Real.exp 1 * (T + 1 + (N ^ r : ℕ)) *
           (2 + (Real.log (N ^ r : ℕ)) ^ 2) *
           (r.factorial : ℝ) * (∑ p ∈ P, ‖a p‖ ^ 2) ^ r := by
   …

   Mentions: OAI.TwoPointCorrelations.mrtExponentialPolynomial

4. theorem OAI.TwoPointCorrelations.mrt_prime_large_values line 107

   Source documentation

   A cardinality bound for one-separated large values.

   Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTLargeValues.lean:107 (same declaration text).

   theorem mrt_prime_large_values (P : Finset ℕ) (a : ℕ → ℂ)
       (N r : ℕ) (hP : ∀ p ∈ P, p.Prime) (hN : ∀ p ∈ P, p ≤ N)
       (S : Finset ℝ) {T V : ℝ} (hT : 0 ≤ T) (hV : 0 < V)
       (hS : ∀ t ∈ S, |t| ≤ T)
       (hsep : ∀ x ∈ S, ∀ y ∈ S, x ≠ y → 1 ≤ |x - y|)
       (hlarge : ∀ t ∈ S,
         V ≤ ‖mrtExponentialPolynomial P a (fun p => -Real.log (p : ℝ)) t‖) :
       (S.card : ℝ) ≤
         (8 * Real.exp 1 * (T + 1 + (N ^ r : ℕ)) *
           (2 + (Real.log (N ^ r : ℕ)) ^ 2) *
           (r.factorial : ℝ) * (∑ p ∈ P, ‖a p‖ ^ 2) ^ r) / V ^ (2 * r) := by
   …

   Mentions: OAI.TwoPointCorrelations.mrtExponentialPolynomial

5. theorem OAI.TwoPointCorrelations.mrt_prime_large_values_geometric line 131

   Source documentation

   A convenient geometric-decay form. The hypothesis compares the moment order times the coefficient square mass with the large-value threshold, rather than hiding this numerical requirement in an input.

   Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTLargeValues.lean:131 (same declaration text).

   theorem mrt_prime_large_values_geometric (P : Finset ℕ) (a : ℕ → ℂ)
       (N r : ℕ) (hP : ∀ p ∈ P, p.Prime) (hN : ∀ p ∈ P, p ≤ N)
       (S : Finset ℝ) {T V ρ : ℝ} (hT : 0 ≤ T) (hV : 0 < V)
       (hmass : (r : ℝ) * (∑ p ∈ P, ‖a p‖ ^ 2) ≤ ρ * V ^ 2)
       (hS : ∀ t ∈ S, |t| ≤ T)
       (hsep : ∀ x ∈ S, ∀ y ∈ S, x ≠ y → 1 ≤ |x - y|)
       (hlarge : ∀ t ∈ S,
         V ≤ ‖mrtExponentialPolynomial P a (fun p => -Real.log (p : ℝ)) t‖) :
       (S.card : ℝ) ≤
         (8 * Real.exp 1 * (T + 1 + (N ^ r : ℕ)) *
           (2 + (Real.log (N ^ r : ℕ)) ^ 2)) * ρ ^ r := by
   …

   Mentions: OAI.TwoPointCorrelations.mrtExponentialPolynomial