OAI/NumberTheory/CubicMoment/Estimates/PrimeCoordinateCollection.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Exact collection of the original independently weighted prime tuples, with the individual support and the global norm cutoff both retained.

  1. def OAI.CubicFirstMoment.coordinateFactor line 14
  2. def OAI.CubicFirstMoment.coordinateSupport line 19
  3. lemma OAI.CubicFirstMoment.coordinateSupport_primary line 23
  4. lemma OAI.CubicFirstMoment.coordinateSupport_lower line 29
  5. lemma OAI.CubicFirstMoment.coordinateFactor_bound line 42
  6. lemma OAI.CubicFirstMoment.coordinate_convolution_collection line 54

    Source documentation

    Collection and support restriction are identities for arbitrary coefficient functions; the prime and normalized prime cases specialize it.

    lemma coordinate_convolution_collection (A : Eisenstein → ℂ)
    (a b : Eisenstein) (ha : primary a) (hb : primary b)
    (q : ι → Eisenstein) (η : (i : ι) → MulChar (Residues (q i)) ℂ) (t : ι → ℝ)
    (W : ι → ℝ → ℂ) (X : ι → ℝ) (V : ℝ → ℂ) (Y : ℝ) :
    (∑ n ∈ Fintype.piFinset (fun _ : ι => primaryElementBall (2*Y)),
      (∏ i, A (n i)*W i (norm (n i)/X i)*
        (mixedCubic a b (n i)*η i (Ideal.Quotient.mk (modulus (q i)) (n i))*
          mellinPhase (t i) (norm (n i))))*V ((∏ i, norm (n i))/Y)) =
    ∑ z ∈ orderedConvolutionSupport (coordinateSupport W X Y),
      orderedConvolution (coordinateSupport W X Y)
        (fun i n => A n*coordinateFactor q η t W X i n) z*
        (mixedCubic a b z*V (norm z/Y)) := by
…

    Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.Residues, OAI.CubicFirstMoment.primaryElementBall, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.mixedCubic, OAI.CubicFirstMoment.modulus, OAI.CubicFirstMoment.mellinPhase, OAI.CubicFirstMoment.orderedConvolutionSupport, OAI.CubicFirstMoment.coordinateSupport, OAI.CubicFirstMoment.orderedConvolution, OAI.CubicFirstMoment.coordinateFactor