PrimaryConvolutionMass.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Sharp L1 mass of the actual finite primary convolutions. Collection by product costs no multiplicity loss in L1.

lemma OAI.CubicFirstMoment.orderedConvolution_mass_le line 14
lemma OAI.CubicFirstMoment.primaryConvolution_mass_le line 28
lemma OAI.CubicFirstMoment.short_convolution_mass line 48
lemma OAI.CubicFirstMoment.factor_le_total_product line 61

theorem OAI.CubicFirstMoment.short_convolution_mass_log line 72

Source documentation

Actual short Möbius/zeta/log coefficients on fixed dyads have only linear length mass and a fixed logarithmic power.

theorem short_convolution_mass_log (F : ℝ) (X : ι → ℝ)
    (A : ι → EisensteinArithmeticFunction) (u : ι → Eisenstein → ℂ)
    (hA : ∀ i, ShortArithmeticFactor F (A i)) (hX : ∀ i, 1 ≤ X i)
    (hu : ∀ i, ∀ a ∈ primaryElementBall (X i), ‖u i a‖ ≤ 1)
    {R : ℝ} (hR : 1 ≤ R) (hprod : (∏ i, X i) ≤ R) :
    (∑ b ∈ orderedConvolutionSupport (fun i => primaryElementBall (X i)),
      ‖orderedConvolution (fun i => primaryElementBall (X i))
        (fun i a => ((MvPowerSeries.coeff (idealExponentOf a) (A i):ℝ):ℂ)*u i a) b‖) ≤
      18^(Fintype.card ι)*R*(1+Real.log R)^(Fintype.card ι) := by
…

Mentions: OAI.CubicFirstMoment.EisensteinArithmeticFunction, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.ShortArithmeticFactor, OAI.CubicFirstMoment.primaryElementBall, OAI.CubicFirstMoment.orderedConvolutionSupport, OAI.CubicFirstMoment.orderedConvolution, OAI.CubicFirstMoment.idealExponentOf

theorem OAI.CubicFirstMoment.short_dyadic_convolution_mass line 97

Source documentation

The usual dyadic supports [X_i,2 X_i], with the lower cutoff allowed inside the bounded twist, give the precise coefficient mass needed for the Type-I level dyad.

theorem short_dyadic_convolution_mass (F : ℝ) (X : ι → ℝ)
    (A : ι → EisensteinArithmeticFunction) (u : ι → Eisenstein → ℂ)
    (hA : ∀ i, ShortArithmeticFactor F (A i)) (hX : ∀ i, 1 ≤ X i)
    (hu : ∀ i, ∀ a ∈ primaryElementBall (2*X i), ‖u i a‖ ≤ 1)
    {R : ℝ} (hR : 1 ≤ R) (hprod : (∏ i, X i) ≤ R) :
    (∑ b ∈ orderedConvolutionSupport (fun i => primaryElementBall (2*X i)),
      ‖orderedConvolution (fun i => primaryElementBall (2*X i))
        (fun i a => ((MvPowerSeries.coeff (idealExponentOf a) (A i):ℝ):ℂ)*u i a) b‖) ≤
      (36*(1+Real.log 2))^(Fintype.card ι)*R*(1+Real.log R)^(Fintype.card ι) := by
…