OAI/NumberTheory/CubicMoment/Estimates/PrimeConvolutionMoments.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CubicFirstMoment.primeConvolutionEnergy line 14
2. lemma OAI.CubicFirstMoment.primeConvolutionEnergy_nonneg line 18
3. theorem OAI.CubicFirstMoment.orderedConvolution_energy_le line 24

   Source documentation

   Collecting ordered tuples loses at most their exact uniform fiber bound, once, in the quadratic coefficient energy.

   theorem orderedConvolution_energy_le (S : ι → Finset Eisenstein)
       (w : ι → Eisenstein → ℂ) (hS : ∀ i, ∀ p ∈ S i, primaryPrime p) :
       (∑ b ∈ orderedConvolutionSupport S, ‖orderedConvolution S w b‖^2) ≤
         ((Fintype.card ι)^(Fintype.card ι):ℕ)*primeConvolutionEnergy S w := by
   …

   Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primaryPrime, OAI.CubicFirstMoment.orderedConvolutionSupport, OAI.CubicFirstMoment.orderedConvolution, OAI.CubicFirstMoment.primeConvolutionEnergy

4. lemma OAI.CubicFirstMoment.orderedConvolution_twisted_energy_le line 56
5. def OAI.CubicFirstMoment.primeCubicProductPolynomial line 68
6. lemma OAI.CubicFirstMoment.primeCubicProductPolynomial_eq line 72
7. theorem OAI.CubicFirstMoment.primeConvolution_cubic_moment line 82

   Source documentation

   The actual product polynomial inherits the unrestricted cubic sieve with the proved fixed-length coefficient energy.

   theorem primeConvolution_cubic_moment {ε : ℝ} (hε : 0 < ε) (hε₁ : ε ≤ 1) :
       ∃ C : ℝ, 0 < C ∧ ∀ (S : ι → Finset Eisenstein) (w : ι → Eisenstein → ℂ),
         (∀ i, ∀ p ∈ S i, primaryPrime p) → ∀ (P : Finset Eisenstein) (N Y : ℝ),
         1 ≤ N → 1 ≤ Y →
         (∀ a ∈ P, primary a ∧ Squarefree a ∧ norm a ≤ N) →
         (∀ f ∈ Fintype.piFinset S, norm (∏ i, f i) ≤ Y) →
         (∑ a ∈ P, ‖primeCubicProductPolynomial S w a‖^2) ≤
           C*(N*Y)^ε*(N*Y^(1/3:ℝ)+(N*Y)^(2/3:ℝ)+Y^(4/3:ℝ)+Y)*
             (((Fintype.card ι)^(Fintype.card ι):ℕ)*primeConvolutionEnergy S w) := by
   …

   Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primaryPrime, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.primeCubicProductPolynomial, OAI.CubicFirstMoment.primeConvolutionEnergy

8. theorem OAI.CubicFirstMoment.primeConvolution_twisted_cubic_moment line 112

   Source documentation

   Norm-at-most-one fixed coefficient twists cost nothing in this moment estimate, whether or not they factor over the prime tuple.

   theorem primeConvolution_twisted_cubic_moment {ε : ℝ} (hε : 0 < ε) (hε₁ : ε ≤ 1) :
       ∃ C : ℝ, 0 < C ∧ ∀ (S : ι → Finset Eisenstein) (w : ι → Eisenstein → ℂ),
         (∀ i, ∀ p ∈ S i, primaryPrime p) → ∀ (P : Finset Eisenstein) (N Y : ℝ),
         1 ≤ N → 1 ≤ Y →
         (∀ a ∈ P, primary a ∧ Squarefree a ∧ norm a ≤ N) →
         (∀ f ∈ Fintype.piFinset S, norm (∏ i, f i) ≤ Y) →
         ∀ χ : Eisenstein → ℂ, (∀ b ∈ orderedConvolutionSupport S, ‖χ b‖ ≤ 1) →
         (∑ a ∈ P, ‖∑ b ∈ orderedConvolutionSupport S,
           (orderedConvolution S w b*χ b)*cubicSymbol a b‖^2) ≤
           C*(N*Y)^ε*(N*Y^(1/3:ℝ)+(N*Y)^(2/3:ℝ)+Y^(4/3:ℝ)+Y)*
             (((Fintype.card ι)^(Fintype.card ι):ℕ)*primeConvolutionEnergy S w) := by
   …

   Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primaryPrime, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.orderedConvolutionSupport, OAI.CubicFirstMoment.orderedConvolution, OAI.CubicFirstMoment.cubicSymbol, OAI.CubicFirstMoment.primeConvolutionEnergy

9. lemma OAI.CubicFirstMoment.eisenstein_norm_finset_prod line 136
10. theorem OAI.CubicFirstMoment.primePolynomial_even_moment line 146

    Source documentation

    Repeating one prime polynomial gives its actual 2k-th character moment, with coefficient energy k^k times the k-th power of its original quadratic energy.

    theorem primePolynomial_even_moment (k : ℕ) {ε : ℝ}
        (hε : 0 < ε) (hε₁ : ε ≤ 1) :
        ∃ C : ℝ, 0 < C ∧ ∀ (S : Finset Eisenstein) (w : Eisenstein → ℂ),
          (∀ p ∈ S, primaryPrime p) → ∀ (P : Finset Eisenstein) (N X : ℝ),
          1 ≤ N → 1 ≤ X →
          (∀ a ∈ P, primary a ∧ Squarefree a ∧ norm a ≤ N) →
          (∀ p ∈ S, norm p ≤ X) →
          (∑ a ∈ P, ‖∑ p ∈ S, w p*cubicSymbol a p‖^(2*k)) ≤
            C*(N*X^k)^ε*(N*(X^k)^(1/3:ℝ)+(N*X^k)^(2/3:ℝ)+(X^k)^(4/3:ℝ)+X^k)*
              ((k^k:ℕ)*(∑ p ∈ S, ‖w p‖^2)^k) := by
    …

    Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primaryPrime, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.cubicSymbol