ShortMoebius.lean`

38 declarations, 0 contain sorry, 0 declared as axioms

The short Möbius identity on Eisenstein ideals

Nonzero Eisenstein ideals are represented by their finite prime-ideal exponent vectors. Their arithmetic functions form the multivariate power series ring: its multiplication is exactly finite Dirichlet convolution. The norm below is the norm of the product of prime representatives, so the support statements retain the actual multiplicative ideal norm.

abbrev OAI.CubicFirstMoment.EisensteinIdealPrime line 22
abbrev OAI.CubicFirstMoment.EisensteinIdealExponent line 23
abbrev OAI.CubicFirstMoment.EisensteinArithmeticFunction line 24
def OAI.CubicFirstMoment.idealPrimeRepresentative line 26
lemma OAI.CubicFirstMoment.idealPrimeRepresentative_irreducible line 28
def OAI.CubicFirstMoment.idealExponentGenerator line 34
Source documentation
A generator of the ideal represented by its prime exponent vector.
```
def idealExponentGenerator (ν : EisensteinIdealExponent) : Eisenstein :=
…
```
Mentions: OAI.CubicFirstMoment.EisensteinIdealExponent, OAI.CubicFirstMoment.Eisenstein
def OAI.CubicFirstMoment.idealExponentNorm line 37
lemma OAI.CubicFirstMoment.idealExponentGenerator_add line 40
lemma OAI.CubicFirstMoment.idealExponentGenerator_of_multiset line 44
def OAI.CubicFirstMoment.idealExponentOf line 53
Source documentation
The exponent vector of every nonzero Eisenstein principal ideal.
```
def idealExponentOf (a : Eisenstein) : EisensteinIdealExponent :=
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.EisensteinIdealExponent
lemma OAI.CubicFirstMoment.idealExponentOf_associated line 56
lemma OAI.CubicFirstMoment.idealExponentOf_mul line 81
lemma OAI.CubicFirstMoment.idealExponentOf_norm line 90
lemma OAI.CubicFirstMoment.idealExponentGenerator_ne_zero line 95
lemma OAI.CubicFirstMoment.idealExponentNorm_ge_one line 101
lemma OAI.CubicFirstMoment.idealExponentNorm_pos line 106
lemma OAI.CubicFirstMoment.idealExponentNorm_add line 109
lemma OAI.CubicFirstMoment.idealExponentNorm_mono line 113
def OAI.CubicFirstMoment.idealZeta line 118
lemma OAI.CubicFirstMoment.idealExponentNorm_single line 120
lemma OAI.CubicFirstMoment.coeff_mul_zeta_single line 132
Source documentation
On the powers of one prime ideal, Dirichlet convolution with the constant-one function is the ordinary partial sum of coefficients.
```
lemma coeff_mul_zeta_single (A : EisensteinArithmeticFunction)
    (p : EisensteinIdealPrime) (n : ℕ) :
    MvPowerSeries.coeff (Finsupp.single p n) (A * idealZeta) =
      ∑ k ∈ Finset.range (n + 1), MvPowerSeries.coeff (Finsupp.single p k) A := by
…
```
Mentions: OAI.CubicFirstMoment.EisensteinArithmeticFunction, OAI.CubicFirstMoment.EisensteinIdealPrime, OAI.CubicFirstMoment.idealZeta
lemma OAI.CubicFirstMoment.coeff_single_eq_zeta_difference line 142
def OAI.CubicFirstMoment.idealMoebiusSeries line 152
Source documentation
The ideal Möbius function, characterized as the Dirichlet inverse of the constant-one arithmetic function.
```
def idealMoebiusSeries : EisensteinArithmeticFunction := idealZeta⁻¹
```
Mentions: OAI.CubicFirstMoment.EisensteinArithmeticFunction, OAI.CubicFirstMoment.idealZeta
lemma OAI.CubicFirstMoment.idealMoebiusSeries_mul_zeta line 154
lemma OAI.CubicFirstMoment.idealZeta_mul_moebiusSeries line 159
lemma OAI.CubicFirstMoment.idealMoebiusSeries_prime_power line 164
Source documentation
The convolution inverse has the usual arithmetic Möbius values on all positive powers of a prime ideal.
```
lemma idealMoebiusSeries_prime_power (p : EisensteinIdealPrime) (n : ℕ) :
    MvPowerSeries.coeff (Finsupp.single p (n + 1)) idealMoebiusSeries =
      if n = 0 then -1 else 0 := by
…
```
Mentions: OAI.CubicFirstMoment.EisensteinIdealPrime, OAI.CubicFirstMoment.idealMoebiusSeries
def OAI.CubicFirstMoment.shortIdealMoebius line 171
def OAI.CubicFirstMoment.shortMoebiusResidual line 174
lemma OAI.CubicFirstMoment.exponent_fst_le line 177
lemma OAI.CubicFirstMoment.exponent_snd_le line 185
lemma OAI.CubicFirstMoment.shortMoebiusResidual_low_norm line 195
Source documentation
The truncated Möbius inverse agrees with the full inverse on every divisor of an ideal whose norm is at most the truncation threshold.
```
lemma shortMoebiusResidual_low_norm (F : ℝ) (ν : EisensteinIdealExponent)
    (hν : idealExponentNorm ν ≤ Real.sqrt F) :
    MvPowerSeries.coeff ν (shortMoebiusResidual F) = 0 := by
…
```
Mentions: OAI.CubicFirstMoment.EisensteinIdealExponent, OAI.CubicFirstMoment.idealExponentNorm, OAI.CubicFirstMoment.shortMoebiusResidual
lemma OAI.CubicFirstMoment.shortMoebiusResidual_sq_low_norm line 210
Source documentation
Both nonzero factors of the residual must have norm greater than sqrt F; hence its square vanishes throughout the actual norm ball F.
```
lemma shortMoebiusResidual_sq_low_norm {F : ℝ} (hF : 0 ≤ F)
    (ν : EisensteinIdealExponent) (hν : idealExponentNorm ν ≤ F) :
    MvPowerSeries.coeff ν ((shortMoebiusResidual F) ^ 2) = 0 := by
…
```
Mentions: OAI.CubicFirstMoment.EisensteinIdealExponent, OAI.CubicFirstMoment.idealExponentNorm, OAI.CubicFirstMoment.shortMoebiusResidual
lemma OAI.CubicFirstMoment.shortMoebiusResidual_sq_mul_low_norm line 230
def OAI.CubicFirstMoment.idealLogNorm line 240
def OAI.CubicFirstMoment.idealVonMangoldt line 243
Source documentation
The usual convolution definition of the ideal von Mangoldt function.
```
def idealVonMangoldt : EisensteinArithmeticFunction := idealMoebiusSeries * idealLogNorm
```
Mentions: OAI.CubicFirstMoment.EisensteinArithmeticFunction, OAI.CubicFirstMoment.idealMoebiusSeries, OAI.CubicFirstMoment.idealLogNorm
lemma OAI.CubicFirstMoment.idealZeta_mul_vonMangoldt line 245
lemma OAI.CubicFirstMoment.idealVonMangoldt_prime_power line 250
Source documentation
The ideal von Mangoldt weight on every positive prime power is exactly the logarithm of the prime-ideal norm.
```
lemma idealVonMangoldt_prime_power (p : EisensteinIdealPrime) (n : ℕ) :
    MvPowerSeries.coeff (Finsupp.single p (n + 1)) idealVonMangoldt =
      Real.log (normNat (idealPrimeRepresentative p)) := by
…
```
Mentions: OAI.CubicFirstMoment.EisensteinIdealPrime, OAI.CubicFirstMoment.idealVonMangoldt, OAI.CubicFirstMoment.normNat, OAI.CubicFirstMoment.idealPrimeRepresentative
theorem OAI.CubicFirstMoment.short_moebius_identity line 261
Source documentation
The short Möbius convolution identity throughout the sharp norm ball.
```
theorem short_moebius_identity {F : ℝ} (hF : 0 ≤ F)
    (ν : EisensteinIdealExponent) (hν : idealExponentNorm ν ≤ F) :
    MvPowerSeries.coeff ν idealVonMangoldt =
      MvPowerSeries.coeff ν
        ((2 * shortIdealMoebius F - shortIdealMoebius F * shortIdealMoebius F * idealZeta) *
          idealLogNorm) := by
…
```
Mentions: OAI.CubicFirstMoment.EisensteinIdealExponent, OAI.CubicFirstMoment.idealExponentNorm, OAI.CubicFirstMoment.idealVonMangoldt, OAI.CubicFirstMoment.shortIdealMoebius, OAI.CubicFirstMoment.idealZeta, OAI.CubicFirstMoment.idealLogNorm