Bounded-multiplicity maps preserve logarithmic lower bounds

Open

HorizontalPadicL.CharacterCountingTransfer.logLowerBound

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

dirichlet-charactersnumber-theoryp-adic-l-functions

A map with uniformly bounded finite fibres and bounded conductor growth preserves logarithmic-power lower bounds. Explicit finiteness assumptions prevent Set.ncard of an infinite set from silently becoming zero.

Preamble

import Definitions.Def_KN_PrimePowerPropagation

set_option autoImplicit false
noncomputable section
open scoped BigOperators

Formal statement

namespace HorizontalPadicL

/-- A map with uniformly bounded finite fibres and bounded conductor growth
preserves logarithmic-power lower bounds. Explicit finiteness assumptions
prevent Set.ncard of an infinite set from silently becoming zero. -/
theorem CharacterCountingTransfer.logLowerBound
    {S T : Set DirichletCharacterWithLevel}
    (F : CharacterCountingTransfer S T)
    (hS : ∀ X : ℝ, {χ | χ ∈ S ∧ (χ.2.conductor : ℝ) ≤ X}.Finite)
    (hT : ∀ X : ℝ, {χ | χ ∈ T ∧ (χ.2.conductor : ℝ) ≤ X}.Finite)
    (α : ℝ) (hα : 0 < α)
    (hcount : HasLogPowerLowerBound (characterConductorCount S) α) :
    HasLogPowerLowerBound (characterConductorCount T) α := 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