Atlas.NumberTheoryI.code.DirichletL

@[reducible, inline]

abbrev DirichletLFunction.DirichletCharacterMod (N : ℕ) :

Instances For

theorem DirichletLFunction.dirichletLFunction_eq_LSeries {N : ℕ} [NeZero N] (χ : DirichletCharacter ℂ N) {s : ℂ} (hs : 1 < s.re) :

DirichletCharacter.LFunction χ s = LSeries (fun (x : ℕ) => χ ↑x) s

source

@[deprecated DirichletLFunction.dirichletLFunction_eq_LSeries (since := "2024-12-18")]

theorem DirichletLFunction.def_18_19_L_function_eq_dirichlet_series {N : ℕ} [NeZero N] (χ : DirichletCharacter ℂ N) {s : ℂ} (hs : 1 < s.re) :

DirichletCharacter.LFunction χ s = LSeries (fun (x : ℕ) => χ ↑x) s

Alias of DirichletLFunction.dirichletLFunction_eq_LSeries.

source

theorem DirichletLFunction.dirichletLSeries_eulerProduct_hasProd {N : ℕ} (χ : DirichletCharacter ℂ N) {s : ℂ} (hs : 1 < s.re) :

HasProd (fun (p : Nat.Primes) => (1 - χ ↑↑p * ↑↑p ^ (-s))⁻¹) (LSeries (fun (n : ℕ) => χ ↑n) s)

source

@[deprecated DirichletLFunction.dirichletLSeries_eulerProduct_hasProd (since := "2024-12-18")]

theorem DirichletLFunction.def_18_19_euler_product_hasProd {N : ℕ} (χ : DirichletCharacter ℂ N) {s : ℂ} (hs : 1 < s.re) :

HasProd (fun (p : Nat.Primes) => (1 - χ ↑↑p * ↑↑p ^ (-s))⁻¹) (LSeries (fun (n : ℕ) => χ ↑n) s)

Alias of DirichletLFunction.dirichletLSeries_eulerProduct_hasProd.

source

theorem DirichletLFunction.dirichletLSeries_eulerProduct_tprod {N : ℕ} (χ : DirichletCharacter ℂ N) {s : ℂ} (hs : 1 < s.re) :

∏' (p : Nat.Primes), (1 - χ ↑↑p * ↑↑p ^ (-s))⁻¹ = LSeries (fun (n : ℕ) => χ ↑n) s

source

@[deprecated DirichletLFunction.dirichletLSeries_eulerProduct_tprod (since := "2024-12-18")]

theorem DirichletLFunction.def_18_19_euler_product_tprod {N : ℕ} (χ : DirichletCharacter ℂ N) {s : ℂ} (hs : 1 < s.re) :

∏' (p : Nat.Primes), (1 - χ ↑↑p * ↑↑p ^ (-s))⁻¹ = LSeries (fun (n : ℕ) => χ ↑n) s

Alias of DirichletLFunction.dirichletLSeries_eulerProduct_tprod.

source

theorem DirichletLFunction.dirichletLSeries_eulerProduct {N : ℕ} (χ : DirichletCharacter ℂ N) {s : ℂ} (hs : 1 < s.re) :

Filter.Tendsto (fun (n : ℕ) => ∏ p ∈ n.primesBelow, (1 - χ ↑p * ↑p ^ (-s))⁻¹) Filter.atTop (nhds (LSeries (fun (n : ℕ) => χ ↑n) s))

source

@[deprecated DirichletLFunction.dirichletLSeries_eulerProduct (since := "2024-12-18")]

theorem DirichletLFunction.def_18_19_euler_product {N : ℕ} (χ : DirichletCharacter ℂ N) {s : ℂ} (hs : 1 < s.re) :

Filter.Tendsto (fun (n : ℕ) => ∏ p ∈ n.primesBelow, (1 - χ ↑p * ↑p ^ (-s))⁻¹) Filter.atTop (nhds (LSeries (fun (n : ℕ) => χ ↑n) s))

Alias of DirichletLFunction.dirichletLSeries_eulerProduct.

source

theorem DirichletLFunction.dirichletLFunction_differentiableAt {N : ℕ} [NeZero N] (χ : DirichletCharacter ℂ N) {s : ℂ} (hs : 1 < s.re) :

DifferentiableAt ℂ (DirichletCharacter.LFunction χ) s

source

@[deprecated DirichletLFunction.dirichletLFunction_differentiableAt (since := "2024-12-18")]

theorem DirichletLFunction.def_18_19_L_function_holomorphic {N : ℕ} [NeZero N] (χ : DirichletCharacter ℂ N) {s : ℂ} (hs : 1 < s.re) :

DifferentiableAt ℂ (DirichletCharacter.LFunction χ) s

Alias of DirichletLFunction.dirichletLFunction_differentiableAt.

source

theorem DirichletLFunction.dirichletLSeries_ne_zero_of_one_lt_re {N : ℕ} (χ : DirichletCharacter ℂ N) {s : ℂ} (hs : 1 < s.re) :

LSeries (fun (n : ℕ) => χ ↑n) s ≠ 0

source

@[deprecated DirichletLFunction.dirichletLSeries_ne_zero_of_one_lt_re (since := "2024-12-18")]

theorem DirichletLFunction.def_18_19_L_function_ne_zero_of_one_lt_re {N : ℕ} (χ : DirichletCharacter ℂ N) {s : ℂ} (hs : 1 < s.re) :

LSeries (fun (n : ℕ) => χ ↑n) s ≠ 0

Alias of DirichletLFunction.dirichletLSeries_ne_zero_of_one_lt_re.

source

theorem DirichletLFunction.dirichletLFunction_modOne_eq_riemannZeta {χ : DirichletCharacter ℂ 1} :

DirichletCharacter.LFunction χ = riemannZeta

source

@[deprecated DirichletLFunction.dirichletLFunction_modOne_eq_riemannZeta (since := "2024-12-18")]

theorem DirichletLFunction.L_trivial_eq_zeta {χ : DirichletCharacter ℂ 1} :

DirichletCharacter.LFunction χ = riemannZeta

Alias of DirichletLFunction.dirichletLFunction_modOne_eq_riemannZeta.

source

theorem DirichletLFunction.dirichletLFunction_differentiable_of_ne_one {N : ℕ} [NeZero N] {χ : DirichletCharacter ℂ N} (hχ : χ ≠ 1) :

Differentiable ℂ (DirichletCharacter.LFunction χ)

source

@[deprecated DirichletLFunction.dirichletLFunction_differentiable_of_ne_one (since := "2024-12-18")]

theorem DirichletLFunction.prop_18_20_differentiable_LFunction {N : ℕ} [NeZero N] {χ : DirichletCharacter ℂ N} (hχ : χ ≠ 1) :

Differentiable ℂ (DirichletCharacter.LFunction χ)

Alias of DirichletLFunction.dirichletLFunction_differentiable_of_ne_one.

source

theorem DirichletLFunction.dirichletLFunction_ne_zero_at_one {N : ℕ} [NeZero N] {χ : DirichletCharacter ℂ N} (hχ : χ ≠ 1) :

DirichletCharacter.LFunction χ 1 ≠ 0

source

@[deprecated DirichletLFunction.dirichletLFunction_ne_zero_at_one (since := "2024-12-18")]

theorem DirichletLFunction.thm_18_key_L_one_ne_zero {N : ℕ} [NeZero N] {χ : DirichletCharacter ℂ N} (hχ : χ ≠ 1) :

DirichletCharacter.LFunction χ 1 ≠ 0

Alias of DirichletLFunction.dirichletLFunction_ne_zero_at_one.

source

theorem DirichletLFunction.dirichletLFunction_ne_zero_of_one_le_re {N : ℕ} [NeZero N] (χ : DirichletCharacter ℂ N) {s : ℂ} (hχs : χ ≠ 1 ∨ s ≠ 1) (hs : 1 ≤ s.re) :

DirichletCharacter.LFunction χ s ≠ 0

source

@[deprecated DirichletLFunction.dirichletLFunction_ne_zero_of_one_le_re (since := "2024-12-18")]

theorem DirichletLFunction.thm_18_key_L_ne_zero_of_one_le_re {N : ℕ} [NeZero N] (χ : DirichletCharacter ℂ N) {s : ℂ} (hχs : χ ≠ 1 ∨ s ≠ 1) (hs : 1 ≤ s.re) :

DirichletCharacter.LFunction χ s ≠ 0

Alias of DirichletLFunction.dirichletLFunction_ne_zero_of_one_le_re.

source

theorem DirichletLFunction.infinite_primes_in_residueClass_zmod {q : ℕ} [NeZero q] {a : ZMod q} (ha : IsUnit a) :

{p : ℕ | Nat.Prime p ∧ ↑p = a}.Infinite

source

@[deprecated DirichletLFunction.infinite_primes_in_residueClass_zmod (since := "2024-12-18")]

theorem DirichletLFunction.thm_18_1_dirichlet_zmod {q : ℕ} [NeZero q] {a : ZMod q} (ha : IsUnit a) :

{p : ℕ | Nat.Prime p ∧ ↑p = a}.Infinite

Alias of DirichletLFunction.infinite_primes_in_residueClass_zmod.

source

theorem DirichletLFunction.exists_prime_gt_and_zmodEq (n : ℕ) {q : ℕ} {a : ℤ} (hq : q ≠ 0) (h : IsCoprime a ↑q) :

∃ p > n, Nat.Prime p ∧ ↑p ≡ a [ZMOD ↑q]

source

@[deprecated DirichletLFunction.exists_prime_gt_and_zmodEq (since := "2024-12-18")]

theorem DirichletLFunction.thm_18_1_dirichlet_int (n : ℕ) {q : ℕ} {a : ℤ} (hq : q ≠ 0) (h : IsCoprime a ↑q) :

∃ p > n, Nat.Prime p ∧ ↑p ≡ a [ZMOD ↑q]

Alias of DirichletLFunction.exists_prime_gt_and_zmodEq.

source

theorem DirichletLFunction.exists_prime_gt_and_modEq (n : ℕ) {q a : ℕ} (hq : q ≠ 0) (h : a.Coprime q) :

∃ p > n, Nat.Prime p ∧ p ≡ a [MOD q]

source

@[deprecated DirichletLFunction.exists_prime_gt_and_modEq (since := "2024-12-18")]

theorem DirichletLFunction.thm_18_1_dirichlet (n : ℕ) {q a : ℕ} (hq : q ≠ 0) (h : a.Coprime q) :

∃ p > n, Nat.Prime p ∧ p ≡ a [MOD q]

Alias of DirichletLFunction.exists_prime_gt_and_modEq.

source

theorem DirichletLFunction.infinite_primes_in_arithmeticProgression {q a : ℕ} (hq : q ≠ 0) (h : a.Coprime q) :

{p : ℕ | Nat.Prime p ∧ p ≡ a [MOD q]}.Infinite

source

@[deprecated DirichletLFunction.infinite_primes_in_arithmeticProgression (since := "2024-12-18")]

theorem DirichletLFunction.thm_18_1_dirichlet_infinite {q a : ℕ} (hq : q ≠ 0) (h : a.Coprime q) :

{p : ℕ | Nat.Prime p ∧ p ≡ a [MOD q]}.Infinite

Alias of DirichletLFunction.infinite_primes_in_arithmeticProgression.

source

theorem DirichletLFunction.frequently_prime_and_modEq {q a : ℕ} (hq : q ≠ 0) (h : a.Coprime q) :

∃ᶠ (p : ℕ) in Filter.atTop , Nat.Prime p ∧ p ≡ a [MOD q]

source

@[deprecated DirichletLFunction.frequently_prime_and_modEq (since := "2024-12-18")]

theorem DirichletLFunction.thm_18_1_dirichlet_frequently {q a : ℕ} (hq : q ≠ 0) (h : a.Coprime q) :

∃ᶠ (p : ℕ) in Filter.atTop , Nat.Prime p ∧ p ≡ a [MOD q]

Alias of DirichletLFunction.frequently_prime_and_modEq.

source

theorem DirichletLFunction.dirichletLSeries_changeLevel {M N : ℕ} [NeZero N] (hMN : M ∣ N) (χ : DirichletCharacter ℂ M) {s : ℂ} (hs : 1 < s.re) :

LSeries (fun (n : ℕ) => ((DirichletCharacter.changeLevel hMN) χ) ↑n) s = LSeries (fun (n : ℕ) => χ ↑n) s * ∏ p ∈ N.primeFactors, (1 - χ ↑p * ↑p ^ (-s))

source

@[deprecated DirichletLFunction.dirichletLSeries_changeLevel (since := "2024-12-18")]

theorem DirichletLFunction.L_series_change_level {M N : ℕ} [NeZero N] (hMN : M ∣ N) (χ : DirichletCharacter ℂ M) {s : ℂ} (hs : 1 < s.re) :

LSeries (fun (n : ℕ) => ((DirichletCharacter.changeLevel hMN) χ) ↑n) s = LSeries (fun (n : ℕ) => χ ↑n) s * ∏ p ∈ N.primeFactors, (1 - χ ↑p * ↑p ^ (-s))

Alias of DirichletLFunction.dirichletLSeries_changeLevel.