Ihara constant

DefinitionNormalized Ihara ratio#✓fully proved

For a sequence \(N : \mathbb{N} \to \mathbb{N}\) and \(g \in \mathbb{N}\), the normalized ratio of \(N\) at \(g\) is the extended nonnegative real \(N(g)/g\) when \(g > 0\), and \(0\) when \(g = 0\).

noncomputable def iharaRatio (N : ℕ → ℕ) (g : ℕ) : ENNReal :=
  if g = 0 then 0 else (N g : ENNReal) / (g : ENNReal)

Used by 10

Used byAbstract Ihara constant of a sequence · The abstract Ihara constant ignores finitely many values · Eventual linear upper bound on the abstract Ihara constant · Eventual ratio bounds bound the abstract Ihara constant · Monotonicity of the abstract Ihara constant · Linear upper bound on a normalized ratio · Monotonicity of the normalized ratio · Lower bound for the Ihara constant from a linear bound · Lower bound for the Ihara constant from the normalized ratios · Lower bound for one normalized Ihara ratio

DefinitionAbstract Ihara constant of a sequence#✓fully proved

For a sequence \(N : \mathbb{N} \to \mathbb{N}\), the abstract Ihara constant of \(N\) is \(\limsup_{g \to \infty} N(g)/g \in [0, \infty]\), the limit superior as \(g \to \infty\) of the normalized ratios of \(N\).

noncomputable def iharaConstantOf (N : ℕ → ℕ) : ENNReal :=
  Filter.limsup (iharaRatio N) atTop

Uses 1 · Used by 8

Statement usesNormalized Ihara ratio

Used byThe abstract Ihara constant ignores finitely many values · Agreement from an index onward preserves the abstract Ihara constant · Eventual linear upper bound on the abstract Ihara constant · Eventual affine upper bound on the abstract Ihara constant · Eventual ratio bounds bound the abstract Ihara constant · Monotonicity of the abstract Ihara constant · Lower bound for the Ihara constant from a linear bound · Lower bound for the Ihara constant from the normalized ratios

TheoremEventual ratio bounds bound the abstract Ihara constant#✓fully proved

Let \(N : \mathbb{N} \to \mathbb{N}\) and \(c \in [0, \infty]\). If the normalized ratio of \(N\) at \(g\) is at most \(c\) for all sufficiently large \(g\), then the abstract Ihara constant of \(N\) is at most \(c\).

theorem iharaConstantOf_le_of_eventually_ratio_le (N : ℕ → ℕ) {c : ENNReal}
    (h : ∀ᶠ g in atTop, iharaRatio N g ≤ c) :
    iharaConstantOf N ≤ c

Uses 2 · Used by 1

Statement usesAbstract Ihara constant of a sequence · Normalized Ihara ratio

Used byEventual linear upper bound on the abstract Ihara constant

TheoremLower bound for the Ihara constant from the normalized ratios#✓fully proved

Let \(N : \mathbb{N} \to \mathbb{N}\), let \(c \in [0, \infty]\), and for each \(g \in \mathbb{N}\) let \(r_N(g) \in [0, \infty]\) be the normalized ratio \(N(g)/g\), with \(r_N(0) = 0\). If \(c \le r_N(g)\) for infinitely many \(g\), then \(c \le \limsup_{g \to \infty} r_N(g)\), the Ihara constant of \(N\).

theorem le_iharaConstantOf_of_frequently_ratio_le (N : ℕ → ℕ) {c : ENNReal}
    (h : ∃ᶠ g in atTop, c ≤ iharaRatio N g) :
    c ≤ iharaConstantOf N

Uses 2 · Used by 1

Statement usesAbstract Ihara constant of a sequence · Normalized Ihara ratio

Used byLower bound for the Ihara constant from a linear bound

TheoremLinear upper bound on a normalized ratio#✓fully proved

Let \(N : \mathbb{N} \to \mathbb{N}\), \(g \in \mathbb{N}\) and \(c \in [0, \infty]\). If \(N(g) \le c \cdot g\) in \([0, \infty]\), then the normalized ratio of \(N\) at \(g\) is at most \(c\).

theorem iharaRatio_le_of_le_mul (N : ℕ → ℕ) {c : ENNReal} {g : ℕ}
    (h : (N g : ENNReal) ≤ c * (g : ENNReal)) :
    iharaRatio N g ≤ c

Uses 1 · Used by 1

Statement usesNormalized Ihara ratio

Used byEventual linear upper bound on the abstract Ihara constant

TheoremLower bound for one normalized Ihara ratio#✓fully proved

Let \(N : \mathbb{N} \to \mathbb{N}\), \(c \in [0, \infty]\) and \(g > 0\) an integer. If \(c \cdot g \le N(g)\) in \([0, \infty]\), then \(c \le N(g)/g\), where the normalized ratio \(N(g)/g\) is taken in \([0, \infty]\).

theorem le_iharaRatio_of_mul_le (N : ℕ → ℕ) {c : ENNReal} {g : ℕ}
    (hg : 0 < g) (h : c * (g : ENNReal) ≤ (N g : ENNReal)) :
    c ≤ iharaRatio N g

Uses 1 · Used by 1

Statement usesNormalized Ihara ratio

Used byLower bound for the Ihara constant from a linear bound

TheoremEventual linear upper bound on the abstract Ihara constant#✓fully proved

Let \(N : \mathbb{N} \to \mathbb{N}\) and \(c \in [0, \infty]\). If \(N(g) \le c \cdot g\) in \([0, \infty]\) for all sufficiently large \(g\), then the abstract Ihara constant of \(N\) is at most \(c\).

theorem iharaConstantOf_le_of_eventually_le (N : ℕ → ℕ) {c : ENNReal}
    (h : ∀ᶠ g in atTop, (N g : ENNReal) ≤ c * (g : ENNReal)) :
    iharaConstantOf N ≤ c

Uses 4 · Used by 1

Statement usesAbstract Ihara constant of a sequence

Proof usesEventual ratio bounds bound the abstract Ihara constant · Normalized Ihara ratio · Linear upper bound on a normalized ratio

Used byEventual affine upper bound on the abstract Ihara constant

TheoremEventual affine upper bound on the abstract Ihara constant#✓fully proved

Let \(N : \mathbb{N} \to \mathbb{N}\), \(c \in [0, \infty]\) and \(d \in [0, \infty)\). If \(N(g) \le c \cdot g + d\) in \([0, \infty]\) for all sufficiently large \(g\), then the abstract Ihara constant of \(N\) is at most \(c\).

theorem iharaConstantOf_le_of_eventually_le_add (N : ℕ → ℕ) {c d : ENNReal}
    (hd : d ≠ ⊤)
    (h : ∀ᶠ g : ℕ in atTop, (N g : ENNReal) ≤ c * (g : ENNReal) + d) :
    iharaConstantOf N ≤ c

Uses 2

Statement usesAbstract Ihara constant of a sequence

Proof usesEventual linear upper bound on the abstract Ihara constant

TheoremLower bound for the Ihara constant from a linear bound#✓fully proved

Let \(N : \mathbb{N} \to \mathbb{N}\) and \(c \in [0, \infty]\). If there are infinitely many integers \(g > 0\) with \(c \cdot g \le N(g)\) in \([0, \infty]\), then \(c \le \limsup_{g \to \infty} N(g)/g\), the Ihara constant of \(N\), where the ratio \(N(g)/g\) is taken in \([0, \infty]\) and set to \(0\) at \(g = 0\).

theorem le_iharaConstantOf_of_frequently_le (N : ℕ → ℕ) {c : ENNReal}
    (h : ∃ᶠ g : ℕ in atTop, 0 < g ∧ c * (g : ENNReal) ≤ (N g : ENNReal)) :
    c ≤ iharaConstantOf N

Uses 4

Statement usesAbstract Ihara constant of a sequence

Proof usesNormalized Ihara ratio · Lower bound for the Ihara constant from the normalized ratios · Lower bound for one normalized Ihara ratio

TheoremMonotonicity of the normalized ratio#✓fully proved

Let \(N, M : \mathbb{N} \to \mathbb{N}\) and \(g \in \mathbb{N}\). If \(N(g) \le M(g)\), then the normalized ratio of \(N\) at \(g\) is at most the normalized ratio of \(M\) at \(g\).

theorem iharaRatio_mono {N M : ℕ → ℕ} {g : ℕ} (h : N g ≤ M g) :
    iharaRatio N g ≤ iharaRatio M g

Uses 1 · Used by 1

Statement usesNormalized Ihara ratio

Used byMonotonicity of the abstract Ihara constant

TheoremMonotonicity of the abstract Ihara constant#✓fully proved

Let \(N, M : \mathbb{N} \to \mathbb{N}\). If \(N(g) \le M(g)\) for all sufficiently large \(g\), then the abstract Ihara constant of \(N\) is at most that of \(M\).

theorem iharaConstantOf_mono_of_eventually_le {N M : ℕ → ℕ}
    (h : ∀ᶠ g in atTop, N g ≤ M g) :
    iharaConstantOf N ≤ iharaConstantOf M

Uses 3

Statement usesAbstract Ihara constant of a sequence

Proof usesNormalized Ihara ratio · Monotonicity of the normalized ratio

TheoremThe abstract Ihara constant ignores finitely many values#✓fully proved

Let \(N, M : \mathbb{N} \to \mathbb{N}\). If \(N(g) = M(g)\) for all sufficiently large \(g\), then \(N\) and \(M\) have the same abstract Ihara constant. In particular, changing finitely many values of \(N\) does not change its abstract Ihara constant.

theorem iharaConstantOf_congr {N M : ℕ → ℕ} (h : N =ᶠ[atTop] M) :
    iharaConstantOf N = iharaConstantOf M

Uses 2 · Used by 1

Statement usesAbstract Ihara constant of a sequence

Proof usesNormalized Ihara ratio

Used byAgreement from an index onward preserves the abstract Ihara constant

TheoremAgreement from an index onward preserves the abstract Ihara constant#✓fully proved

Let \(N, M : \mathbb{N} \to \mathbb{N}\) and \(G \in \mathbb{N}\). If \(N(g) = M(g)\) for every \(g \ge G\), then \(N\) and \(M\) have the same abstract Ihara constant.

theorem iharaConstantOf_eq_of_eventually_eq {N M : ℕ → ℕ} {G : ℕ}
    (h : ∀ g ≥ G, N g = M g) :
    iharaConstantOf N = iharaConstantOf M

Uses 2

Statement usesAbstract Ihara constant of a sequence

Proof usesThe abstract Ihara constant ignores finitely many values

13 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.