Class-wise partial fractions

For a numerator A ∈ ℚ[x] and a finite set Pl ⊆ ℤ of simple poles:

• polyPart A Pl = A /ₘ ∏ (x - r), resP A Pl r = A(r) / ∏_{s ≠ r} (r - s);
• partial_fractionsP : A = polyPart · ∏ (x - r) + ∑_r res_r ∏_{s ≠ r} (x - s);
• Adm p A e : for every integer m, A(m + p x) has Gauss valuation ≥ e (m mod p);
• VG_res : v_p(res_r) ≥ e_c - ℓ_c + 1 (c the class of r, ℓ_c the number of poles in it);
• VG_polyPart_eval : a class-wise lower bound for the values of the polynomial part at integers.

Integer valuations

theorem Zeta32.Arith.Local.zmod_eq_iff_dvd {p : ℕ} {a b : ℤ} : ↑a = ↑b ↔ ↑p ∣ a - b

theorem Zeta32.Arith.Local.VG_int_one {p : ℕ} [hp : Fact (Nat.Prime p)] {z : ℤ} (h : ↑p ∣ z) : VG p (↑z) 1

theorem Zeta32.Arith.Local.padicValRat_int_eq_zero {p : ℕ} [hp : Fact (Nat.Prime p)] {z : ℤ} (h : ¬↑p ∣ z) : padicValRat p ↑z = 0

theorem Zeta32.Arith.Local.padicValRat_int_le_one {p : ℕ} [hp : Fact (Nat.Prime p)] {z : ℤ} (h2 : ¬↑p ^ 2 ∣ z) : padicValRat p ↑z ≤ 1

The class-count predicate

def Zeta32.Arith.Local.Adm (p : ℕ) (A : Polynomial ℚ) (e : ZMod p → ℤ) : Prop

A(m + p x) has Gauss valuation ≥ e (m mod p) for every integer m.

Equations

• Zeta32.Arith.Local.Adm p A e = ∀ (m : ℤ), Zeta5Irrational.GV p (A.comp (Polynomial.C ↑m + Polynomial.C ↑p * Polynomial.X)) ↑(e ↑m)

theorem Zeta32.Arith.Local.Adm.mono {p : ℕ} {A : Polynomial ℚ} {e e' : ZMod p → ℤ} (h : Adm p A e) (he : ∀ (c : ZMod p), e' c ≤ e c) : Adm p A e'

theorem Zeta32.Arith.Local.Adm.one {p : ℕ} : Adm p 1 0

theorem Zeta32.Arith.Local.Adm.mul {p : ℕ} [hp : Fact (Nat.Prime p)] {A B : Polynomial ℚ} {e e' : ZMod p → ℤ} (hA : Adm p A e) (hB : Adm p B e') : Adm p (A * B) (e + e')

theorem Zeta32.Arith.Local.Adm.prod {p : ℕ} [hp : Fact (Nat.Prime p)] {ι : Type u_1} (s : Finset ι) (A : ι → Polynomial ℚ) (e : ι → ZMod p → ℤ) (h : ∀ i ∈ s, Adm p (A i) (e i)) : Adm p (∏ i ∈ s, A i) fun (c : ZMod p) => ∑ i ∈ s, e i c

theorem Zeta32.Arith.Local.Adm.pow {p : ℕ} [hp : Fact (Nat.Prime p)] {A : Polynomial ℚ} {e : ZMod p → ℤ} (h : Adm p A e) (k : ℕ) : Adm p (A ^ k) fun (c : ZMod p) => ↑k * e c

theorem Zeta32.Arith.Local.Adm.X_sub_C {p : ℕ} [hp : Fact (Nat.Prime p)] (ζ : ℤ) : Adm p (Polynomial.X - Polynomial.C ↑ζ) fun (c : ZMod p) => if ↑ζ = c then 1 else 0

theorem Zeta32.Arith.Local.Adm.eval {p : ℕ} {A : Polynomial ℚ} {e : ZMod p → ℤ} (h : Adm p A e) (x : ℤ) : VG p (Polynomial.eval (↑x) A) ↑(e ↑x)

Residues

def Zeta32.Arith.Local.plc (p : ℕ) (Pl : Finset ℤ) (c : ZMod p) : Finset ℤ

Poles in the class c.

Equations

• Zeta32.Arith.Local.plc p Pl c = {r ∈ Pl | ↑r = c}

def Zeta32.Arith.Local.Sep (p : ℕ) (Pl : Finset ℤ) : Prop

Poles in the same class differ by exactly one power of p.

Equations

• Zeta32.Arith.Local.Sep p Pl = ∀ r ∈ Pl, ∀ s ∈ Pl, r ≠ s → ↑r = ↑s → ¬↑p ^ 2 ∣ r - s

theorem Zeta32.Arith.Local.padicValRat_denom_le {p : ℕ} [hp : Fact (Nat.Prime p)] (Pl : Finset ℤ) (hsep : Sep p Pl) {r : ℤ} (hr : r ∈ Pl) : ↑(padicValRat p (∏ s ∈ Pl.erase r, (↑r - ↑s))) ≤ ↑(plc p Pl ↑r).card - 1

theorem Zeta32.Arith.Local.VG_res {p : ℕ} [hp : Fact (Nat.Prime p)] {A : Polynomial ℚ} {e : ZMod p → ℤ} (hA : Adm p A e) (Pl : Finset ℤ) (hsep : Sep p Pl) {r : ℤ} (hr : r ∈ Pl) : VG p (resP A Pl r) (↑(e ↑r) - ↑(plc p Pl ↑r).card + 1)

Residue bound: v_p(res_r) ≥ e_c - ℓ_c + 1 for the class c of r.

The polynomial part

theorem Zeta32.Arith.Local.prod_erase_split {f : ℤ → Polynomial ℚ} (S : Finset ℤ) (q : ℤ → Prop) [DecidablePred q] (r : ℤ) : ∏ s ∈ S.erase r, f s = (∏ s ∈ (Finset.filter q S).erase r, f s) * ∏ s ∈ {x ∈ S | ¬q x}.erase r, f s

theorem Zeta32.Arith.Local.GV_lin_comp_class {p : ℕ} [hp : Fact (Nat.Prime p)] (m ζ : ℤ) (h : ↑ζ = ↑m) : GV p ((Polynomial.X - Polynomial.C ↑ζ).comp (Polynomial.C ↑m + Polynomial.C ↑p * Polynomial.X)) 1

theorem Zeta32.Arith.Local.GV_lin_comp {p : ℕ} [hp : Fact (Nat.Prime p)] (m ζ : ℤ) : GV p ((Polynomial.X - Polynomial.C ↑ζ).comp (Polynomial.C ↑m + Polynomial.C ↑p * Polynomial.X)) 0

theorem Zeta32.Arith.Local.lin_comp_eq {p : ℕ} {m r : ℤ} (h : ↑p ∣ r - m) : (Polynomial.X - Polynomial.C ↑r).comp (Polynomial.C ↑m + Polynomial.C ↑p * Polynomial.X) = Polynomial.C ↑p * (Polynomial.X - Polynomial.C ↑((r - m) / ↑p))

(x - r)(m + p z) = p (z - ρ) with ρ = (r - m)/p, for r ≡ m.

theorem Zeta32.Arith.Local.VG_polyPart_eval {p : ℕ} [hp : Fact (Nat.Prime p)] {A : Polynomial ℚ} {e : ZMod p → ℤ} (hA : Adm p A e) (Pl : Finset ℤ) (hsep : Sep p Pl) (m : ℤ) (β : ℚ) (hβm : β ≤ ↑(e ↑m) - ↑(plc p Pl ↑m).card) (hβo : ∀ r ∈ Pl, ¬↑r = ↑m → β ≤ ↑(e ↑r) - ↑(plc p Pl ↑r).card + 1) : VG p (Polynomial.eval (↑m) (polyPart A Pl)) β

Class-wise bound for the polynomial part at an integer m: poles in the class of m enter through e_c - ℓ_c, poles in the other classes only through their residues.