structure Hex.DensePoly.PadeApproximant {F : Type u} [DecidableEq F] [Lean.Grind.Field F] {k : Nat} (s : TSeries F k) (m n : Nat) : Type u

A homogeneous Padé approximant of numerator degree at most m and denominator degree at most n. A nonzero denominator is stronger than the nontrivial-pair condition and is what the half-gcd construction supplies.

• p : DensePoly F

  Numerator polynomial.

• q : DensePoly F

  Denominator polynomial.

• p_size : self.p.size ≤ m + 1

  The numerator has degree at most the requested bound.

• q_size : self.q.size ≤ n + 1

  The denominator has degree at most the requested bound.

• q_ne : self.q ≠ 0

  The denominator is nonzero.

• congruent (i : Nat) : i < m + n + 1 → (self.q * polyOfSeries s - self.p).coeff i = 0

  The denominator times the input agrees with the numerator to the required order.

theorem Hex.DensePoly.size_low_le {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (len : Nat) (p : DensePoly F) : (low len p).size ≤ len

A low coefficient prefix has size at most its length.

theorem Hex.DensePoly.low_eq_self_of_size_le {F : Type u} [DecidableEq F] [Lean.Grind.Field F] {len : Nat} {p : DensePoly F} (hsize : p.size ≤ len) : low len p = p

A prefix covering the polynomial's support equals the polynomial.

def Hex.DensePoly.padeBoundary {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (plan : MulPlan F) {k : Nat} (s : TSeries F k) (m n : Nat) : GcdBoundaryResult F

The terminal half-gcd boundary underlying Padé construction.

Equations

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

def Hex.DensePoly.padeHomogeneous {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (plan : MulPlan F) {k : Nat} (s : TSeries F k) (m n : Nat) : PadeApproximant s m n

Compute a homogeneous Padé approximant with the selected multiplication plan. The half-gcd prefix stops precisely when the remainder crosses the numerator-size boundary.

Equations

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

theorem Hex.DensePoly.padeHomogeneous_q {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (plan : MulPlan F) {k : Nat} (s : TSeries F k) (m n : Nat) : (padeHomogeneous plan s m n).q = (padeBoundary plan s m n).matrix.a11

The homogeneous denominator is the lower-row continuant at the Padé boundary.

structure Hex.DensePoly.NormalizedPade {F : Type u} [DecidableEq F] [Lean.Grind.Field F] {k : Nat} (s : TSeries F k) (m n : Nat) : Type u

A Padé approximant whose denominator is normalized at the origin.

• p : DensePoly F

  Numerator polynomial.

• q : DensePoly F

  Denominator polynomial.

• p_size : self.p.size ≤ m + 1

  The numerator has degree at most the requested bound.

• q_size : self.q.size ≤ n + 1

  The denominator has degree at most the requested bound.

• q_zero : self.q.coeff 0 = 1

  The denominator is normalized to one at the origin.

• congruent (i : Nat) : i < m + n + 1 → (self.q * polyOfSeries s - self.p).coeff i = 0

  The denominator times the input agrees with the numerator to the required order.

def Hex.DensePoly.PadeApproximant.normalize {F : Type u} [DecidableEq F] [Lean.Grind.Field F] {k : Nat} {s : TSeries F k} {m n : Nat} (approx : PadeApproximant s m n) (hc : approx.q.coeff 0 ≠ 0) : NormalizedPade s m n

Scale a Padé pair by the inverse denominator constant to normalize it at the origin.

Equations

• approx.normalize hc = { p := Hex.DensePoly.scale (approx.q.coeff 0)⁻¹ approx.p, q := Hex.DensePoly.scale (approx.q.coeff 0)⁻¹ approx.q, p_size := ⋯, q_size := ⋯, q_zero := ⋯, congruent := ⋯ }

def Hex.DensePoly.pade? {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (plan : MulPlan F) {k : Nat} (s : TSeries F k) (m n : Nat) : Option (NormalizedPade s m n)

Compute the normalized rational-series Padé form when its denominator can be made a unit at the origin.

Equations

• Hex.DensePoly.pade? plan s m n = if hc : (Hex.DensePoly.padeHomogeneous plan s m n).q.coeff 0 = 0 then none else some ((Hex.DensePoly.padeHomogeneous plan s m n).normalize hc)

theorem Hex.DensePoly.pade?_eq_none_iff {F : Type u} [DecidableEq F] [Lean.Grind.Field F] (plan : MulPlan F) {k : Nat} (s : TSeries F k) (m n : Nat) : pade? plan s m n = none ↔ ¬Nonempty (NormalizedPade s m n)

Normalized Padé construction fails exactly when no denominator with constant coefficient one satisfies the requested bounds and congruence.