AngularShortTuplePartition.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Exact reconstruction of the original finite convolution from smooth norm pieces. The common ball is forced by the global product cutoff.

def OAI.CubicFirstMoment.primaryAngularTupleCore line 16
lemma OAI.CubicFirstMoment.primaryAngularShortTupleSum_eq_core line 23
lemma OAI.CubicFirstMoment.primaryAngularTupleCore_support line 45
lemma OAI.CubicFirstMoment.primaryAngularShortTupleSum_common_ball line 62

theorem OAI.CubicFirstMoment.primaryAngularShortTupleSum_partition line 92

Source documentation

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

theorem primaryAngularShortTupleSum_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)),
      primaryAngularTupleCore ℓ A a b q η t V Z n) =
      ∑ k : ι → Fin (normPartitionCount (2*Z)),
        primaryAngularShortTupleSum ℓ (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.primaryAngularTupleCore, OAI.CubicFirstMoment.normPartitionCount, OAI.CubicFirstMoment.primaryAngularShortTupleSum, OAI.CubicFirstMoment.normPartitionWeight