"Scaled" polynomials and power series (the coefficient of u^e has valuation ≥ e, i.e. G(p u) with G integral) and the disc factorization predicate Good: F(p u - d) = p^E u^E R(u) with R scaled and R(0) a p-adic unit.

def Zeta32.PrimeEdge.Scaled (p : ℕ) (f : Polynomial ℚ) : Prop

The coefficient of u^e has valuation ≥ e.

Equations

• Zeta32.PrimeEdge.Scaled p f = ∀ (e : ℕ), Zeta5Irrational.VG p (f.coeff e) ↑e

def Zeta32.PrimeEdge.ScaledPS (p : ℕ) (f : PowerSeries ℚ) : Prop

Coefficientwise valuation lower bound for a power series scaled by its degree.

Equations

• Zeta32.PrimeEdge.ScaledPS p f = ∀ (e : ℕ), Zeta5Irrational.VG p ((PowerSeries.coeff e) f) ↑e

def Zeta32.PrimeEdge.IsUnitV (p : ℕ) (q : ℚ) : Prop

A nonzero rational of valuation 0.

Equations

• Zeta32.PrimeEdge.IsUnitV p q = (q ≠ 0 ∧ padicValRat p q = 0)

theorem Zeta32.PrimeEdge.IsUnitV.mul {p : ℕ} [Fact (Nat.Prime p)] {q q' : ℚ} (h : IsUnitV p q) (h' : IsUnitV p q') : IsUnitV p (q * q')

theorem Zeta32.PrimeEdge.IsUnitV.inv {p : ℕ} [Fact (Nat.Prime p)] {q : ℚ} (h : IsUnitV p q) : IsUnitV p q⁻¹

theorem Zeta32.PrimeEdge.IsUnitV.one {p : ℕ} : IsUnitV p 1

theorem Zeta32.PrimeEdge.IsUnitV.VG {p : ℕ} {q : ℚ} (h : IsUnitV p q) : Zeta5Irrational.VG p q 0

theorem Zeta32.PrimeEdge.IsUnitV.pow {p : ℕ} [Fact (Nat.Prime p)] {q : ℚ} (h : IsUnitV p q) (n : ℕ) : IsUnitV p (q ^ n)

theorem Zeta32.PrimeEdge.IsUnitV.prod {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_1} (s : Finset ι) {f : ι → ℚ} (h : ∀ i ∈ s, IsUnitV p (f i)) : IsUnitV p (∏ i ∈ s, f i)

theorem Zeta32.PrimeEdge.isUnitV_sub {p : ℕ} [Fact (Nat.Prime p)] {j d : ℕ} (h : j % p ≠ d % p) : IsUnitV p (↑j - ↑d)

j - d is a unit when j ≢ d (mod p).

Scaled polynomials

theorem Zeta32.PrimeEdge.Scaled.mul {p : ℕ} [Fact (Nat.Prime p)] {f g : Polynomial ℚ} (hf : Scaled p f) (hg : Scaled p g) : Scaled p (f * g)

theorem Zeta32.PrimeEdge.Scaled.one {p : ℕ} : Scaled p 1

theorem Zeta32.PrimeEdge.Scaled.pow {p : ℕ} [Fact (Nat.Prime p)] {f : Polynomial ℚ} (hf : Scaled p f) (n : ℕ) : Scaled p (f ^ n)

theorem Zeta32.PrimeEdge.Scaled.prod {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_1} (s : Finset ι) {f : ι → Polynomial ℚ} (h : ∀ i ∈ s, Scaled p (f i)) : Scaled p (∏ i ∈ s, f i)

theorem Zeta32.PrimeEdge.Scaled.lin {p : ℕ} [hp : Fact (Nat.Prime p)] {α : ℚ} (hα : Zeta5Irrational.VG p α 0) : Scaled p (Polynomial.C α + Polynomial.C ↑p * Polynomial.X)

α + p u with α integral.

Scaled power series

theorem Zeta32.PrimeEdge.ScaledPS.coe {p : ℕ} {f : Polynomial ℚ} (hf : Scaled p f) : ScaledPS p ↑f

theorem Zeta32.PrimeEdge.ScaledPS.mul {p : ℕ} [Fact (Nat.Prime p)] {f g : PowerSeries ℚ} (hf : ScaledPS p f) (hg : ScaledPS p g) : ScaledPS p (f * g)

theorem Zeta32.PrimeEdge.ScaledPS.inv {p : ℕ} [Fact (Nat.Prime p)] {f : PowerSeries ℚ} (hf : ScaledPS p f) (hu : IsUnitV p (PowerSeries.constantCoeff f)) : ScaledPS p f⁻¹

Inverse of a scaled series with unit constant term.

The disc factorization predicate

def Zeta32.PrimeEdge.Good (p d : ℕ) (F : Polynomial ℚ) (E : ℕ) : Prop

F(p u - d) = p^E u^E R(u), R scaled with unit constant term.

Equations

• One or more equations did not get rendered due to their size.

theorem Zeta32.PrimeEdge.Good.congr {p d : ℕ} {F : Polynomial ℚ} {E E' : ℕ} (h : Good p d F E) (hE : E = E') : Good p d F E'

theorem Zeta32.PrimeEdge.Good.mul {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} {F G : Polynomial ℚ} {E E' : ℕ} (hF : Good p d F E) (hG : Good p d G E') : Good p d (F * G) (E + E')

theorem Zeta32.PrimeEdge.Good.one {p d : ℕ} : Good p d 1 0

theorem Zeta32.PrimeEdge.Good.pow {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} {F : Polynomial ℚ} {E : ℕ} (hF : Good p d F E) (n : ℕ) : Good p d (F ^ n) (n * E)

theorem Zeta32.PrimeEdge.Good.prod {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} {ι : Type u_1} (s : Finset ι) {f : ι → Polynomial ℚ} {E : ι → ℕ} (h : ∀ i ∈ s, Good p d (f i) (E i)) : Good p d (∏ i ∈ s, f i) (∑ i ∈ s, E i)

theorem Zeta32.PrimeEdge.Good.lin {p : ℕ} [Fact (Nat.Prime p)] {d ℓ : ℕ} (hd : d < p) (hℓ : ℓ < p) : Good p d (Polynomial.X + Polynomial.C ↑ℓ) (if ℓ = d then 1 else 0)

A linear factor t + ℓ with 0 ≤ ℓ, d < p on the disc t = p u - d.

theorem Zeta32.PrimeEdge.Good.X_self {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} (hd : d < p) : Good p d Polynomial.X (if 0 = d then 1 else 0)