OAI/NumberTheory/CubicMoment/Estimates/IndependentMellin.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Exact Mellin separation of independent coordinate weights on a finite arithmetic sum. The joint weight has explicitly factored L1 mass.

  1. lemma OAI.CubicFirstMoment.zeroLineMellin_point line 13
  2. lemma OAI.CubicFirstMoment.integrable_zeroLineMellin_phase line 31
  3. def OAI.CubicFirstMoment.independentMellinWeight line 46
  4. lemma OAI.CubicFirstMoment.independentMellinWeight_integrable line 49
  5. lemma OAI.CubicFirstMoment.independentMellinWeight_mass line 55
  6. theorem OAI.CubicFirstMoment.independent_mellin_finite line 63

    Source documentation

    All original factor weights are separated simultaneously. No cutoff or Mellin-tail assumption is used in this identity.

    theorem independent_mellin_finite (a : κ → ℂ) (N : ι → κ → ℝ)
    (hN : ∀ i n, 0 < N i n) (W : ι → ℝ → ℂ) (X : ι → ℝ)
    (hW : ∀ i, HasCompactSupport (W i)) (hpos : ∀ i, tsupport (W i) ⊆ Ioi 0)
    (hsm : ∀ i, ContDiff ℝ ∞ (W i)) (hX : ∀ i, 0 < X i) :
    (∑ n, a n*∏ i, W i (N i n/X i)) =
      ∫ τ : ι → ℝ, independentMellinWeight W X τ *
        ∑ n, a n*∏ i, mellinPhase (-(τ i)) (N i n) := by
…

    Mentions: OAI.CubicFirstMoment.independentMellinWeight, OAI.CubicFirstMoment.mellinPhase