Documentation

TauCeti.NumberTheory.ArithmeticDirichletSeries.Convolution

Ideal convolution of ideal arithmetic functions #

The Dirichlet convolution of two arithmetic functions on the nonzero ideals of the ring of integers of a number field K sums over the factorizations B * C = A of a nonzero ideal A. This file constructs that index set, defines the convolution, and proves that it makes TauCeti.IdealArithmeticFunction K a commutative monoid with identity TauCeti.IdealArithmeticFunction.delta, bilinear over the pointwise additive structure. It also transports this operation through TauCeti.normCoeff to Mathlib's Dirichlet convolution on ArithmeticFunction β„‚.

Main definitions #

Main results #

Implementation notes #

TauCeti.IdealArithmeticFunction K is a Pi type, so it already carries Mathlib's pointwise CommRing structure, in which f * g is fun A => f A * g A and 1 is the everywhere-one function. Convolution is therefore deliberately not registered as a Mul instance and its identity is the separate function TauCeti.IdealArithmeticFunction.delta; this is the roadmap's convention that pointwise multiplication and ideal convolution stay distinct operations on one carrier. The monoid laws are stated as ordinary theorems about TauCeti.IdealArithmeticFunction.convolution, and TauCeti.IdealArithmeticFunction.convolution_one_one_ne_mul records that the two products really do differ. Consequently iterated convolution is the explicit TauCeti.IdealArithmeticFunction.convolutionPow rather than a Monoid.npow.

Excluding the zero ideal from the carrier is what makes the index set finite: βŠ₯ * J = βŠ₯ for every J, so the zero ideal has infinitely many factorizations while a nonzero ideal has only finitely many, by Mathlib's UniqueFactorizationMonoid.fintypeSubtypeDvd for the unique factorization monoid Ideal (π“ž K).

Roadmap role #

This is Layer 2.1 of TauCetiRoadmap/ArithmeticDirichletSeries/README.md, built on the Layer 0.1 carrier of TauCeti/NumberTheory/ArithmeticDirichletSeries/Basic.lean. Its consumers are the ideal MΓΆbius function and von Mangoldt transform of Layer 2 and the local factors of Layer 3.

References #

The convolution identity #

source
noncomputable def TauCeti.IdealArithmeticFunction.delta {K : Type u_1} [Field K] :
IdealArithmeticFunction K

The delta function on nonzero ideals: 1 at the unit ideal and 0 elsewhere. It is the identity for ideal convolution. It is not the pointwise unit (1 : IdealArithmeticFunction K), which is the everywhere-one function.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.IdealArithmeticFunction.delta_one {K : Type u_1} [Field K] :
    delta 1 = 1

    The delta function takes the value 1 at the unit ideal.

    source
    @[simp]
    theorem TauCeti.IdealArithmeticFunction.delta_of_ne_one {K : Type u_1} [Field K] {A : β†₯(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))} (hA : A β‰  1) :
    delta A = 0

    The delta function vanishes away from the unit ideal.

    source
    theorem TauCeti.IdealArithmeticFunction.isMultiplicative_delta {K : Type u_1} [Field K] :
    delta.IsMultiplicative

    The convolution identity is multiplicative.

    The antidiagonal of a nonzero ideal #

    source
    theorem TauCeti.Ideal.finite_setOf_mul_eq {K : Type u_1} [Field K] [NumberField K] (A : β†₯(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))) :
    {p : β†₯(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K))) Γ— β†₯(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K))) | p.1 * p.2 = A}.Finite

    A nonzero ideal admits only finitely many factorizations into two nonzero ideals. This is where the exclusion of βŠ₯ from the carrier bites: every ideal J satisfies βŠ₯ * J = βŠ₯.

    source
    noncomputable def TauCeti.Ideal.divisorsAntidiagonal {K : Type u_1} [Field K] [NumberField K] (A : β†₯(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))) :
    Finset (β†₯(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K))) Γ— β†₯(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K))))

    The antidiagonal of a nonzero ideal A: the finite set of pairs (B, C) of nonzero ideals with B * C = A. It is the index set of the ideal Dirichlet convolution, and the ideal analogue of Mathlib's Nat.divisorsAntidiagonal.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.Ideal.mem_divisorsAntidiagonal {K : Type u_1} [Field K] [NumberField K] {A : β†₯(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))} {p : β†₯(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K))) Γ— β†₯(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))} :
      p ∈ divisorsAntidiagonal A ↔ p.1 * p.2 = A

      A pair lies in the antidiagonal of A exactly when its two entries multiply to A.

      source
      theorem TauCeti.Ideal.swap_mem_divisorsAntidiagonal {K : Type u_1} [Field K] [NumberField K] {A : β†₯(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))} {p : β†₯(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K))) Γ— β†₯(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))} (hp : p ∈ divisorsAntidiagonal A) :
      p.swap ∈ divisorsAntidiagonal A

      The antidiagonal is stable under swapping the two factors.

      source
      theorem TauCeti.Ideal.fst_dvd_of_mem_divisorsAntidiagonal {K : Type u_1} [Field K] [NumberField K] {A : β†₯(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))} {p : β†₯(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K))) Γ— β†₯(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))} (hp : p ∈ divisorsAntidiagonal A) :
      ↑p.1 ∣ ↑A

      The first entry of an antidiagonal pair divides A.

      source
      theorem TauCeti.Ideal.snd_dvd_of_mem_divisorsAntidiagonal {K : Type u_1} [Field K] [NumberField K] {A : β†₯(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))} {p : β†₯(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K))) Γ— β†₯(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))} (hp : p ∈ divisorsAntidiagonal A) :
      ↑p.2 ∣ ↑A

      The second entry of an antidiagonal pair divides A.

      source
      @[simp]
      theorem TauCeti.Ideal.divisorsAntidiagonal_one {K : Type u_1} [Field K] [NumberField K] :
      divisorsAntidiagonal 1 = {(1, 1)}

      The unit ideal factors only as 1 * 1.

      source
      theorem TauCeti.Ideal.one_lt_card_divisorsAntidiagonal {K : Type u_1} [Field K] [NumberField K] {A : β†₯(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))} (hA : A β‰  1) :
      1 < (divisorsAntidiagonal A).card

      Every nonzero ideal other than the unit ideal has at least the two factorizations 1 * A and A * 1.

      Ideal convolution #

      source
      noncomputable def TauCeti.IdealArithmeticFunction.convolution {K : Type u_1} [Field K] [NumberField K] (f g : IdealArithmeticFunction K) :
      IdealArithmeticFunction K

      The ideal Dirichlet convolution of two ideal arithmetic functions: the value at a nonzero ideal A is the sum of f B * g C over the factorizations B * C = A into nonzero ideals.

      Equations
      Instances For
        source
        @[simp]
        theorem TauCeti.IdealArithmeticFunction.convolution_apply {K : Type u_1} [Field K] [NumberField K] (f g : IdealArithmeticFunction K) (A : β†₯(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))) :
        f.convolution g A = βˆ‘ p ∈ Ideal.divisorsAntidiagonal A, f p.1 * g p.2

        The defining formula for ideal convolution.

        source
        theorem TauCeti.IdealArithmeticFunction.convolution_apply_one {K : Type u_1} [Field K] [NumberField K] (f g : IdealArithmeticFunction K) :
        f.convolution g 1 = f 1 * g 1

        At the unit ideal, convolution is the product of the two values there.

        The monoid laws #

        source
        theorem TauCeti.IdealArithmeticFunction.convolution_comm {K : Type u_1} [Field K] [NumberField K] (f g : IdealArithmeticFunction K) :
        f.convolution g = g.convolution f

        Ideal convolution is commutative.

        source
        theorem TauCeti.IdealArithmeticFunction.convolution_assoc {K : Type u_1} [Field K] [NumberField K] (f g h : IdealArithmeticFunction K) :
        (f.convolution g).convolution h = f.convolution (g.convolution h)

        Ideal convolution is associative.

        source
        @[simp]
        theorem TauCeti.IdealArithmeticFunction.delta_convolution {K : Type u_1} [Field K] [NumberField K] (f : IdealArithmeticFunction K) :
        delta.convolution f = f

        The delta function is a left identity for ideal convolution.

        source
        @[simp]
        theorem TauCeti.IdealArithmeticFunction.convolution_delta {K : Type u_1} [Field K] [NumberField K] (f : IdealArithmeticFunction K) :
        f.convolution delta = f

        The delta function is a right identity for ideal convolution.

        Bilinearity over the pointwise additive structure #

        source
        @[simp]
        theorem TauCeti.IdealArithmeticFunction.convolution_zero {K : Type u_1} [Field K] [NumberField K] (f : IdealArithmeticFunction K) :
        f.convolution 0 = 0

        Convolving with the zero function gives zero.

        source
        @[simp]
        theorem TauCeti.IdealArithmeticFunction.zero_convolution {K : Type u_1} [Field K] [NumberField K] (f : IdealArithmeticFunction K) :
        convolution 0 f = 0

        Convolving the zero function with anything gives zero.

        source
        theorem TauCeti.IdealArithmeticFunction.convolution_add {K : Type u_1} [Field K] [NumberField K] (f g h : IdealArithmeticFunction K) :
        f.convolution (g + h) = f.convolution g + f.convolution h

        Ideal convolution distributes over pointwise addition on the right.

        source
        theorem TauCeti.IdealArithmeticFunction.add_convolution {K : Type u_1} [Field K] [NumberField K] (f g h : IdealArithmeticFunction K) :
        (f + g).convolution h = f.convolution h + g.convolution h

        Ideal convolution distributes over pointwise addition on the left.

        source
        theorem TauCeti.IdealArithmeticFunction.convolution_smul {K : Type u_1} [Field K] [NumberField K] (c : β„‚) (f g : IdealArithmeticFunction K) :
        f.convolution (c β€’ g) = c β€’ f.convolution g

        Ideal convolution is homogeneous in its second argument.

        source
        theorem TauCeti.IdealArithmeticFunction.smul_convolution {K : Type u_1} [Field K] [NumberField K] (c : β„‚) (f g : IdealArithmeticFunction K) :
        (c β€’ f).convolution g = c β€’ f.convolution g

        Ideal convolution is homogeneous in its first argument.

        source
        theorem TauCeti.IdealArithmeticFunction.convolution_neg {K : Type u_1} [Field K] [NumberField K] (f g : IdealArithmeticFunction K) :
        f.convolution (-g) = -f.convolution g

        Ideal convolution commutes with pointwise negation on the right.

        source
        theorem TauCeti.IdealArithmeticFunction.neg_convolution {K : Type u_1} [Field K] [NumberField K] (f g : IdealArithmeticFunction K) :
        (-f).convolution g = -f.convolution g

        Ideal convolution commutes with pointwise negation on the left.

        source
        theorem TauCeti.IdealArithmeticFunction.convolution_sub {K : Type u_1} [Field K] [NumberField K] (f g h : IdealArithmeticFunction K) :
        f.convolution (g - h) = f.convolution g - f.convolution h

        Ideal convolution distributes over pointwise subtraction on the right.

        source
        theorem TauCeti.IdealArithmeticFunction.sub_convolution {K : Type u_1} [Field K] [NumberField K] (f g h : IdealArithmeticFunction K) :
        (f - g).convolution h = f.convolution h - g.convolution h

        Ideal convolution distributes over pointwise subtraction on the left.

        Iterated convolution #

        source
        noncomputable def TauCeti.IdealArithmeticFunction.convolutionPow {K : Type u_1} [Field K] [NumberField K] (f : IdealArithmeticFunction K) :
        β„• β†’ IdealArithmeticFunction K

        The n-fold ideal convolution power of f, with convolutionPow f 0 = delta.

        Equations
        Instances For
          source
          @[simp]
          theorem TauCeti.IdealArithmeticFunction.convolutionPow_zero {K : Type u_1} [Field K] [NumberField K] (f : IdealArithmeticFunction K) :
          f.convolutionPow 0 = delta

          The empty convolution power is the convolution identity.

          source
          @[simp]
          theorem TauCeti.IdealArithmeticFunction.convolutionPow_succ {K : Type u_1} [Field K] [NumberField K] (f : IdealArithmeticFunction K) (n : β„•) :
          f.convolutionPow (n + 1) = (f.convolutionPow n).convolution f

          The recursion defining the convolution powers.

          source
          theorem TauCeti.IdealArithmeticFunction.convolutionPow_one {K : Type u_1} [Field K] [NumberField K] (f : IdealArithmeticFunction K) :
          f.convolutionPow 1 = f

          The first convolution power is the function itself.

          source
          theorem TauCeti.IdealArithmeticFunction.convolutionPow_succ' {K : Type u_1} [Field K] [NumberField K] (f : IdealArithmeticFunction K) (n : β„•) :
          f.convolutionPow (n + 1) = f.convolution (f.convolutionPow n)

          The recursion defining the convolution powers, with the new factor on the left.

          source
          theorem TauCeti.IdealArithmeticFunction.convolutionPow_add {K : Type u_1} [Field K] [NumberField K] (f : IdealArithmeticFunction K) (m n : β„•) :
          f.convolutionPow (m + n) = (f.convolutionPow m).convolution (f.convolutionPow n)

          Convolution powers add exponents.

          Convolution is not the pointwise product #

          source
          theorem TauCeti.IdealArithmeticFunction.convolution_one_one_apply {K : Type u_1} [Field K] [NumberField K] (A : β†₯(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))) :
          convolution 1 1 A = ↑(Ideal.divisorsAntidiagonal A).card

          Convolving the everywhere-one function with itself counts the factorizations of a nonzero ideal: this is the ideal divisor-counting function.

          source
          theorem TauCeti.IdealArithmeticFunction.convolution_one_one_ne_mul {K : Type u_1} [Field K] [NumberField K] :
          convolution 1 1 β‰  1 * 1

          The rejection test against confusing the two products on IdealArithmeticFunction K: ideal convolution is not the pointwise multiplication carried by the Pi ring structure. The everywhere-one function is a pointwise unit, whereas convolving it with itself counts factorizations, and the ring of integers of a number field is not a field, so some nonzero ideal has more than one factorization.

          Compatibility with Dirichlet convolution #

          source
          @[simp]
          theorem TauCeti.normCoeff_delta (K : Type u_2) [Field K] [NumberField K] :
          (normCoeff K) IdealArithmeticFunction.delta = 1

          Regrouping sends the identity for ideal convolution to the identity for Mathlib's Dirichlet convolution.

          source
          @[simp]
          theorem TauCeti.normCoeff_convolution (K : Type u_2) [Field K] [NumberField K] (f g : IdealArithmeticFunction K) :
          (normCoeff K) (f.convolution g) = (normCoeff K) f * (normCoeff K) g

          Regrouping by absolute norm transports ideal convolution to Mathlib's Dirichlet convolution of arithmetic functions.

          source
          theorem TauCeti.normCoeff_convolutionPow (K : Type u_2) [Field K] [NumberField K] (f : IdealArithmeticFunction K) (n : β„•) :
          (normCoeff K) (f.convolutionPow n) = (normCoeff K) f ^ n

          Regrouping transports iterated ideal convolution to powers under Mathlib's Dirichlet convolution.