OAI/NumberTheory/CubicMoment/Estimates/ShortConvolutionMoments.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CubicFirstMoment.primaryUnsplitTuple line 16
2. lemma OAI.CubicFirstMoment.unsplit_partition_moment line 22
3. theorem OAI.CubicFirstMoment.first_unsplit_tuple_power_saving line 56

   Source documentation

   The first exceptional family, with no smooth coordinate weights left.

   theorem first_unsplit_tuple_power_saving (hpub : PrimitiveResidueHeckeInput)
       (V : ℝ → ℂ) (hV : HasCompactSupport V) (hpos : tsupport V ⊆ Ioi 0)
       (hsm : ContDiff ℝ ∞ V) (hVlo : ∀ x, x < 1 → V x = 0)
       (hVhi : ∀ x, 2 < x → V x = 0)
       (hGI : ∀ m : ℕ, GammaInverseFiniteOrder (1/2-(m:ℝ)) 2)
       (hGQ : ∀ m : ℕ, GammaQuotientStripBound (1/2-(m:ℝ))) :
       ∃ ε : ℝ, 0 < ε ∧ ∃ Y₀ : ℝ, ∀ (F Y : ℝ)
         (A : ι → EisensteinArithmeticFunction) (q : ι → Eisenstein)
         (η : (i : ι) → MulChar (Residues (q i)) ℂ) (t : ι → ℝ) (P : Finset Eisenstein),
         Y₀ ≤ Y → F ≤ 2*Y → (∀ i, ShortArithmeticFactor F (A i)) →
         (∀ i, q i ≠ 0) → (∀ i, ∀ e : Eisensteinˣ, η i (Ideal.Quotient.mk (modulus (q i)) e) = 1) →
         (∀ i, norm (q i) ≤ Y^(1/100000:ℝ)) → (∀ i, |t i| ≤ Y^(361/1000:ℝ)) →
   …

   Mentions: OAI.CubicFirstMoment.PrimitiveResidueHeckeInput, OAI.CubicFirstMoment.GammaInverseFiniteOrder, OAI.CubicFirstMoment.GammaQuotientStripBound, OAI.CubicFirstMoment.EisensteinArithmeticFunction, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.Residues, OAI.CubicFirstMoment.ShortArithmeticFactor, OAI.CubicFirstMoment.modulus, OAI.CubicFirstMoment.norm