OAI/NumberTheory/CubicMoment/Estimates/ShortTuplePartition.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CubicFirstMoment.sum_primary_pi line 14
2. def OAI.CubicFirstMoment.primaryTupleCore line 28
3. lemma OAI.CubicFirstMoment.primaryShortTupleSum_eq_core line 35
4. lemma OAI.CubicFirstMoment.primaryTupleCore_support line 57
5. lemma OAI.CubicFirstMoment.primaryShortTupleSum_common_ball line 74
6. theorem OAI.CubicFirstMoment.primaryShortTupleSum_partition line 104

   Source documentation

   The unsplit finite tuple sum is exactly the sum of its explicit smooth pieces. No decomposition hypothesis is assumed.

   theorem primaryShortTupleSum_partition (A : ι → EisensteinArithmeticFunction)
       (a b : Eisenstein) (q : ι → Eisenstein)
       (η : (i : ι) → MulChar (Residues (q i)) ℂ) (t : ι → ℝ)
       (V : ℝ → ℂ) {Z : ℝ} (hZ : 1 ≤ Z) (hV : ∀ x, 2 < x → V x = 0) :
       (∑ n ∈ Fintype.piFinset (fun _ : ι => primaryElementBall (2*Z)),
         primaryTupleCore A a b q η t V Z n) =
         ∑ k : ι → Fin (normPartitionCount (2*Z)),
           primaryShortTupleSum (fun i => (4/3:ℝ)^(k i).val) A a b q η
             (fun _ => normPartitionWeight) t V Z := by
   …

   Mentions: OAI.CubicFirstMoment.EisensteinArithmeticFunction, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.Residues, OAI.CubicFirstMoment.primaryElementBall, OAI.CubicFirstMoment.primaryTupleCore, OAI.CubicFirstMoment.normPartitionCount, OAI.CubicFirstMoment.primaryShortTupleSum, OAI.CubicFirstMoment.normPartitionWeight