Newman's theorem: valuations, the local constants, and the element γ_p of Lemma 3

• vz p x is the p-adic valuation of an integer (0 at 0); vv B p x is the same but equal to the large value B at 0, so that zero entries can be handled by omega uniformly.
• the ultrametric relation for e = αδ − βγ in terms of vv;
• v_p(h), v_p(ε), v_p(n) in terms of ν = v_p(N);
• exists_gamma_p: for p ∣ N an element [[x, y], [N, t]] ∈ Γ₀(N) with min(v_p(t − x), ν) = v_p(ε) (x ≡ 3 or 2 mod p^ν by the Chinese remainder theorem).

def CongruenceNormalizers.vz (p : ℕ) (x : ℤ) : ℕ

p-adic valuation of an integer (junk value 0 at 0).

Equations

• CongruenceNormalizers.vz p x = x.natAbs.factorization p

theorem CongruenceNormalizers.vz_mul {p : ℕ} {x y : ℤ} (hx : x ≠ 0) (hy : y ≠ 0) : vz p (x * y) = vz p x + vz p y

theorem CongruenceNormalizers.vz_neg (p : ℕ) (x : ℤ) : vz p (-x) = vz p x

theorem CongruenceNormalizers.vz_natCast (p n : ℕ) : vz p ↑n = n.factorization p

theorem CongruenceNormalizers.pow_dvd_iff_le_vz {p : ℕ} (hp : Nat.Prime p) {x : ℤ} (hx : x ≠ 0) (m : ℕ) : ↑p ^ m ∣ x ↔ m ≤ vz p x

theorem CongruenceNormalizers.vz_le_of_dvd (p : ℕ) {x y : ℤ} (hy : y ≠ 0) (hxy : x ∣ y) : vz p x ≤ vz p y

theorem CongruenceNormalizers.vz_eq_zero_of_not_dvd {p : ℕ} {x : ℤ} (h : ¬↑p ∣ x) : vz p x = 0

def CongruenceNormalizers.vv (B p : ℕ) (x : ℤ) : ℕ

Valuation with value B at 0.

Equations

• CongruenceNormalizers.vv B p x = if x = 0 then B else CongruenceNormalizers.vz p x

theorem CongruenceNormalizers.vv_of_ne {B p : ℕ} {x : ℤ} (hx : x ≠ 0) : vv B p x = vz p x

theorem CongruenceNormalizers.vv_neg (B p : ℕ) (x : ℤ) : vv B p (-x) = vv B p x

theorem CongruenceNormalizers.le_vv2 {B p : ℕ} {X K x y : ℤ} (hK : K ≠ 0) (hB : vz p X ≤ B) (h : X ∣ K * (x * y)) : vz p X ≤ vz p K + vv B p x + vv B p y

From X ∣ K·x·y: v(X) ≤ v(K) + v(x) + v(y).

theorem CongruenceNormalizers.le_vv_sq {B p : ℕ} {X K x : ℤ} (hK : K ≠ 0) (hB : vz p X ≤ B) (h : X ∣ K * x ^ 2) : vz p X ≤ vz p K + 2 * vv B p x

From X ∣ K·x²: v(X) ≤ v(K) + 2v(x).

The ultrametric inequality

theorem CongruenceNormalizers.vz_sub_ge {p : ℕ} (hp : Nat.Prime p) {A C : ℤ} (hAC : A - C ≠ 0) (hA : A ≠ 0) (hC : C ≠ 0) : min (vz p A) (vz p C) ≤ vz p (A - C)

theorem CongruenceNormalizers.vz_sub_eq {p : ℕ} (hp : Nat.Prime p) {A C : ℤ} (hAC : A - C ≠ 0) (hA : A ≠ 0) (hC : C ≠ 0) (hne : vz p A ≠ vz p C) : vz p (A - C) = min (vz p A) (vz p C)

theorem CongruenceNormalizers.ultra_vv {B p : ℕ} (hp : Nat.Prime p) {α β γ δ : ℤ} (he : α * δ - β * γ ≠ 0) (hB : vz p (α * δ - β * γ) < B) : min (vv B p α + vv B p δ) (vv B p β + vv B p γ) ≤ vz p (α * δ - β * γ) ∧ (vv B p α + vv B p δ ≠ vv B p β + vv B p γ → vz p (α * δ - β * γ) = min (vv B p α + vv B p δ) (vv B p β + vv B p γ))

The ultrametric relation for e = αδ − βγ, in terms of vv.

The local constants

theorem CongruenceNormalizers.factorization_24 (p : ℕ) : (Nat.factorization 24) p = if p = 2 then 3 else if p = 3 then 1 else 0

theorem CongruenceNormalizers.factorization_two (p : ℕ) : (Nat.factorization 2) p = if p = 2 then 1 else 0

theorem CongruenceNormalizers.factorization_hPart (N p : ℕ) : (hPart N).factorization p = if p = 2 then min 3 (N.factorization 2 / 2) else if p = 3 then min 1 (N.factorization 3 / 2) else 0

theorem CongruenceNormalizers.factorization_epsPart {N : ℕ} (hN : N ≠ 0) (p : ℕ) : (epsPart N).factorization p = min (N.factorization p) ((Nat.factorization 24) p)

theorem CongruenceNormalizers.local_constants {N p : ℕ} (hN : N ≠ 0) : (p = 2 ∧ (epsPart N).factorization p = min (N.factorization p) 3 ∧ (Nat.factorization 2) p = 1 ∨ p = 3 ∧ (epsPart N).factorization p = min (N.factorization p) 1 ∧ (Nat.factorization 2) p = 0 ∨ (epsPart N).factorization p = 0 ∧ (Nat.factorization 2) p = 0) ∧ (hPart N).factorization p = min ((epsPart N).factorization p) (N.factorization p / 2)

The local data at p: ν = v_p(N), j = v_p(ε), k = v_p(h), e₂ = v_p(2).

theorem CongruenceNormalizers.factorization_nPart {N p : ℕ} (hN : N ≠ 0) : (nPart N).factorization p + 2 * (hPart N).factorization p = N.factorization p

The element γ_p of Lemma 3

theorem CongruenceNormalizers.gamma_val {p ν ρ : ℕ} (hp : Nat.Prime p) {N x y t r : ℤ} (hdet : x * t - y * N = 1) (hN : ↑p ^ ν ∣ N) (hxr : ↑p ^ ν ∣ r - x) (hpx : IsCoprime (↑p) x) (hρ1 : ↑p ^ ρ ∣ 1 - r ^ 2) (hρ2 : ¬↑p ^ (ρ + 1) ∣ 1 - r ^ 2) : ν ≤ ρ ∨ ρ < ν ∧ t - x ≠ 0 ∧ vz p (t - x) = ρ

If x t − y N = 1, p^ν ∣ N, x ≡ r (mod p^ν), p ∤ x, p^ρ ∥ 1 − r², then either ν ≤ ρ, or t − x ≠ 0 with v_p(t − x) = ρ.

theorem CongruenceNormalizers.exists_gamma_p {N p : ℕ} (hN : N ≠ 0) (hp : Nat.Prime p) (hpN : p ∣ N) : ∃ (x : ℤ) (y : ℤ) (t : ℤ), x * t - y * ↑N = 1 ∧ (N.factorization p = (epsPart N).factorization p ∨ t - x ≠ 0 ∧ vz p (t - x) = (epsPart N).factorization p)

Lemma 3, locally: for p ∣ N there is [[x, y], [N, t]] ∈ Γ₀(N) with min(v_p(t − x), v_p(N)) = v_p(ε).