IdealVonMangoldt.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

The convolution definition of ideal von Mangoldt has exactly its usual prime-power coefficients. This is the arithmetic bridge for prime replacement in the short Möbius decomposition.

lemma OAI.CubicFirstMoment.idealLogNorm_prime_difference line 14
lemma OAI.CubicFirstMoment.coeff_logNorm_finite_nonempty line 29
lemma OAI.CubicFirstMoment.idealVonMangoldt_coeff_eq_finite line 63
lemma OAI.CubicFirstMoment.idealVonMangoldt_coeff line 77
Source documentation
The von Mangoldt coefficient is supported precisely on prime-ideal powers and has weight the logarithm of that prime-ideal norm.
```
lemma idealVonMangoldt_coeff (ν : EisensteinIdealExponent) :
    MvPowerSeries.coeff ν idealVonMangoldt =
      if ν.support.card = 1 then
        ∑ p ∈ ν.support, Real.log (normNat (idealPrimeRepresentative p)) else 0 := by
…
```
Mentions: OAI.CubicFirstMoment.EisensteinIdealExponent, OAI.CubicFirstMoment.idealVonMangoldt, OAI.CubicFirstMoment.normNat, OAI.CubicFirstMoment.idealPrimeRepresentative
lemma OAI.CubicFirstMoment.idealVonMangoldt_not_prime_power line 91
lemma OAI.CubicFirstMoment.idealVonMangoldt_two_primes line 97
Source documentation
Two distinct prime ideal factors annihilate the von Mangoldt weight.
```
lemma idealVonMangoldt_two_primes {ν : EisensteinIdealExponent}
    {p q : EisensteinIdealPrime} (hp : p ∈ ν.support) (hq : q ∈ ν.support)
    (hpq : p ≠ q) : MvPowerSeries.coeff ν idealVonMangoldt = 0 := by
…
```
Mentions: OAI.CubicFirstMoment.EisensteinIdealExponent, OAI.CubicFirstMoment.EisensteinIdealPrime, OAI.CubicFirstMoment.idealVonMangoldt
lemma OAI.CubicFirstMoment.idealVonMangoldt_coeff_nonneg line 109
lemma OAI.CubicFirstMoment.idealVonMangoldt_coeff_le_logNorm line 120
lemma OAI.CubicFirstMoment.idealVonMangoldt_coeff_abs_le_logNorm line 135
lemma OAI.CubicFirstMoment.idealVonMangoldt_at_prime line 140
lemma OAI.CubicFirstMoment.idealVonMangoldt_primary_support line 158
Source documentation
A nonzero von Mangoldt coefficient at an actual primary element comes from an actual power of a primary prime, with no residual unit.
```
lemma idealVonMangoldt_primary_support {a : Eisenstein} (ha : primary a)
    (hΛ : MvPowerSeries.coeff (idealExponentOf a) idealVonMangoldt ≠ 0) :
    ∃ p : Eisenstein, ∃ j : ℕ, primaryPrime p ∧ 0 < j ∧ a = p ^ j := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.idealExponentOf, OAI.CubicFirstMoment.idealVonMangoldt, OAI.CubicFirstMoment.primaryPrime
lemma OAI.CubicFirstMoment.idealVonMangoldt_primary_nonprime_support line 188