Counting exact-order characters on positive-density prime sets

Open

HorizontalPadicL.supportedPrimePowerCharacters_logLowerBound

by davidloeffler · Sep 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

dirichlet-charactersnumber-theoryp-adic-l-functions

Counting exact-order characters supported on a positive-density set of primes congruent to 1 modulo p^m, after finitely many primes are excluded. The strict slack in alpha avoids an endpoint asymptotic from mere natural density. Intended proof: weighted squarefree counting (a weakened form of Kriz--Nordentoft Lemma 5.7), followed by removing lower-order characters. Source: https://arxiv.org/pdf/2310.20678 .

Preamble

import Definitions.Def_KN_PrimePowerPropagation

set_option autoImplicit false
noncomputable section
open scoped BigOperators

Formal statement

namespace HorizontalPadicL

/-- Counting exact-order characters supported on a positive-density set of
primes congruent to 1 modulo p^m, after finitely many primes are excluded.
The strict slack in alpha avoids an endpoint asymptotic from mere natural
density. Intended proof: weighted squarefree counting (a weakened form of
Kriz--Nordentoft Lemma 5.7), followed by removing lower-order characters.
Source: https://arxiv.org/pdf/2310.20678 . -/
theorem supportedPrimePowerCharacters_logLowerBound
    (p m : ℕ) [Fact p.Prime] (hm : 0 < m)
    (ℓ : ℕ → ℕ) (hprime : ∀ n, (ℓ n).Prime)
    (hinj : Function.Injective ℓ) (hcong : ∀ n, Nat.ModEq (p ^ m) (ℓ n) 1)
    (δ : ℝ) (hδ : 0 < δ)
    (hdensity : HasPrimeNaturalDensity (Set.range ℓ) δ)
    (A : Finset ℕ) :
    ∃ α : ℝ, 0 < α ∧ α < ((p ^ m - 1 : ℕ) : ℝ) * δ ∧
      HasLogPowerLowerBound
        (characterConductorCount (supportedPrimePowerCharacters ℓ A p m)) α := by
  sorry

end HorizontalPadicL

Source

Kriz--Nordentoft, Horizontal p-adic L-functions, https://arxiv.org/pdf/2310.20678, Section 2.3.3, Lemma 5.7, Theorem 5.9 and Corollary 5.10.

View graph