ArtinOrders.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Continuing finite Euler-product identities to zero orders

The cyclic permutation identity is first applied to Euler products in the half-plane of absolute convergence. After clearing the pole at one, the factors are entire. The identity theorem then gives the corresponding integer relation among their zero orders everywhere.

theorem OAI.DukePrimeDegree.analytic_off_zero_one_eq_of_real_eq line 25
Source documentation
The actual Dedekind and Hecke continuations are analytic away from zero and one. Equality on their Dirichlet-series ray determines them on that connected domain, without choosing pole-clearing factors.
```
theorem analytic_off_zero_one_eq_of_real_eq
    {f g : ℂ → ℂ}
    (hf : AnalyticOnNhd ℂ f ({0, 1} : Set ℂ)ᶜ)
    (hg : AnalyticOnNhd ℂ g ({0, 1} : Set ℂ)ᶜ)
    (heq : ∀ s : ℝ, 1 < s → f s = g s) :
    EqOn f g ({0, 1} : Set ℂ)ᶜ := by
…
```

theorem OAI.DukePrimeDegree.entire_product_orders_eq_of_real_eq line 46

Source documentation

Equality of two finite products of entire factors on the real ray above one determines the equality of their weighted zero orders.

theorem entire_product_orders_eq_of_real_eq
    {I : Type*} [Fintype I]
    (f : I → ℂ → ℂ) (hf : ∀ i, Differentiable ℂ (f i))
    (p q : I → ℕ)
    (heq : ∀ s : ℝ, 1 < s → (∏ i, f i s ^ p i) = ∏ i, f i s ^ q i)
    (β : ℂ) :
    (∑ i, (p i : WithTop ℤ) * meromorphicOrderAt (f i) β) =
      ∑ i, (q i : WithTop ℤ) * meromorphicOrderAt (f i) β := by
…

theorem OAI.DukePrimeDegree.integer_orders_eq_of_entire_products line 77

Source documentation

When the factors have finite orders, the continued product identity is an equality of ordinary integer zero orders.

theorem integer_orders_eq_of_entire_products
    {I : Type*} [Fintype I]
    (f : I → ℂ → ℂ) (hf : ∀ i, Differentiable ℂ (f i))
    (p q : I → ℕ)
    (heq : ∀ s : ℝ, 1 < s → (∏ i, f i s ^ p i) = ∏ i, f i s ^ q i)
    (β : ℂ) (m : I → ℤ)
    (hm : ∀ i, meromorphicOrderAt (f i) β = (m i : WithTop ℤ)) :
    (∑ i, (p i : ℤ) * m i) = ∑ i, (q i : ℤ) * m i := by
…

theorem OAI.DukePrimeDegree.product_orders_eq_off_zero_one line 91

Source documentation

A Dirichlet-series product identity gives its zero-order relation at every point away from the possible poles at zero and one.

theorem product_orders_eq_off_zero_one
    {I : Type*} [Fintype I]
    (f : I → ℂ → ℂ)
    (hf : ∀ i, AnalyticOnNhd ℂ (f i) ({0, 1} : Set ℂ)ᶜ)
    (p q : I → ℕ)
    (heq : ∀ s : ℝ, 1 < s → (∏ i, f i s ^ p i) = ∏ i, f i s ^ q i)
    (β : ℂ) (hβ0 : β ≠ 0) (hβ1 : β ≠ 1) :
    (∑ i, (p i : WithTop ℤ) * meromorphicOrderAt (f i) β) =
      ∑ i, (q i : WithTop ℤ) * meromorphicOrderAt (f i) β := by
…