SmallPartTransfer.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Exact transfer from an original row fiber to its coprime outside parts.

lemma OAI.CubicFirstMoment.primarySmallTwistSmoothSum_factor line 13
lemma OAI.CubicFirstMoment.small_part_fiber_smooth_moment line 30
theorem OAI.CubicFirstMoment.first_smalltwist_smooth_fiber_power line 54

theorem OAI.CubicFirstMoment.first_smalltwist_smooth_partition_power line 118

Source documentation

The small-prime parts are summed over an actual partition of the rows. Their number is bounded arithmetically, so no partition cost is assumed.

theorem first_smalltwist_smooth_partition_power (hpub : PrimitiveResidueHeckeInput)
    (W : ℝ → ℂ) (hW : HasCompactSupport W) (hpos : tsupport W ⊆ Ioi 0)
    (hsm : ContDiff ℝ ∞ W)
    (hGI : ∀ m : ℕ, GammaInverseFiniteOrder (1/2-(m:ℝ)) 2)
    (hGQ : ∀ m : ℕ, GammaQuotientStripBound (1/2-(m:ℝ))) :
    ∃ C Y₀ : ℝ, 0 ≤ C ∧ 1 ≤ Y₀ ∧
      ∀ (P : Finset Eisenstein) (v b q : Eisenstein) (η : MulChar (Residues q) ℂ)
        (N Y Z t : ℝ), Y₀ ≤ Y → primary b → Squarefree b → v ≠ 0 → q ≠ 0 →
      (3:Eisenstein) ∣ v → q ∣ v →
      (∀ e : Eisensteinˣ, η (Ideal.Quotient.mk (modulus q) e) = 1) →
      1 ≤ N → N ≤ Y^(1001/1000:ℝ) → Z ≤ Y^(1001/1000:ℝ) → Y^(999/1000:ℝ) ≤ Z →
      norm b*(9*norm v^2*norm q)^2 ≤ Y^(1/1000:ℝ) → |t| ≤ Y^(37/100:ℝ) →
…

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