Documentation

LeanPool.NairTenenbaum.NumberFields.ArithmeticLogDerivativeSupport

Prime-power support of a multiplicative logarithmic derivative #

The first-order logarithmic weighting is encoded in the square-zero extension of the real numbers. Multiplicativity there gives the coprime splitting identity.

source
noncomputable def NairTenenbaum.arithmeticLogJet (f : ArithmeticFunction ℝ) :
ArithmeticFunction (TrivSqZeroExt ℝ ℝ)

The first-order arithmetic jet whose tangent component carries the logarithmic weight.

Equations
Instances For
    source
    noncomputable def NairTenenbaum.arithmeticConstantJet (f : ArithmeticFunction ℝ) :
    ArithmeticFunction (TrivSqZeroExt ℝ ℝ)

    The constant first-order jet of an arithmetic function.

    Equations
    Instances For
      source
      @[simp]
      theorem NairTenenbaum.arithmeticLogJet_apply (f : ArithmeticFunction ℝ) (n : ℕ) :
      (arithmeticLogJet f) n = (f n, f n * Real.log ↑n)
      source
      @[simp]
      theorem NairTenenbaum.arithmeticConstantJet_apply (f : ArithmeticFunction ℝ) (n : ℕ) :
      (arithmeticConstantJet f) n = (f n, 0)
      source
      theorem NairTenenbaum.arithmeticLogJet_isMultiplicative {f : ArithmeticFunction ℝ} (hf : f.IsMultiplicative) :
      (arithmeticLogJet f).IsMultiplicative
      source
      theorem NairTenenbaum.arithmeticConstantJet_isMultiplicative {f : ArithmeticFunction ℝ} (hf : f.IsMultiplicative) :
      (arithmeticConstantJet f).IsMultiplicative
      source
      theorem NairTenenbaum.arithmeticLogJet_mul_fst (f g : ArithmeticFunction ℝ) (n : ℕ) :
      ((arithmeticLogJet f * arithmeticConstantJet g) n).fst = (f * g) n
      source
      theorem NairTenenbaum.arithmeticLogJet_mul_snd (f g : ArithmeticFunction ℝ) (n : ℕ) :
      ((arithmeticLogJet f * arithmeticConstantJet g) n).snd = (arithmeticLogDerivative f g) n
      source
      theorem NairTenenbaum.arithmeticLogDerivative_coprime {f g : ArithmeticFunction ℝ} (hf : f.IsMultiplicative) (hg : g.IsMultiplicative) {m n : ℕ} (hcop : m.Coprime n) :
      (arithmeticLogDerivative f g) (m * n) = (f * g) m * (arithmeticLogDerivative f g) n + (arithmeticLogDerivative f g) m * (f * g) n
      source
      theorem NairTenenbaum.arithmeticLogDerivative_eq_zero_of_not_primePower {f g : ArithmeticFunction ℝ} (hf : f.IsMultiplicative) (hg : g.IsMultiplicative) (hfg : f * g = 1) {n : ℕ} (hn : ¬IsPrimePow n) :
      (arithmeticLogDerivative f g) n = 0