Documentation

Hironaka.Analytic.Rueckert.Specialize

Specialization of a polynomial over π’ͺ_m at a parameter point #

The polynomial Q_a(z) = Q(a_1, …, a_{nβˆ’1})(z) ∈ β„‚[z] for a fixed small parameter a of the proof of [Fre17, Ch. I, 5.1], and the polynomials in z_n over π’ͺ_{nβˆ’1} of [Fre17, Ch. I, Β§8]: for W ∈ π’ͺ_m[x_0] (Mathlib's Polynomial (Conv K m), sent to the series ring by convPolyEval) and a point x ∈ K^m, specialize W x ∈ K[X] is the polynomial whose coefficients are the values of the coefficients of W at x. Near 0 this specialization is a ring homomorphism in the sense of germs of maps: it preserves sums, products and the derivative for x in a neighbourhood of 0 depending on the finitely many coefficients involved (specialize_add_eventually, specialize_mul_eventually, specialize_derivative_eventually; evalSeries is multiplicative only where both factors converge, evalSeries_mul_eventually), it is exact on constants and on X, it preserves monicity and the degree of a monic polynomial, and the series convPolyEval W evaluates at (t, x) as the specialized polynomial at t (evalSeries_convPolyEval_eq_eval_specialize). Used by the hypersurface case of the Nullstellensatz through the specialization of a Bezout identity U W + V W' = D (Hypersurface.lean), and by the parametrization through the specialization of the Weierstrass polynomial (Parametrization.lean).

source
noncomputable def Analytic.specialize {K : Type u_1} [RCLike K] {m : β„•} (W : Polynomial β†₯(Conv K m)) (x : Fin m β†’ K) :
Polynomial K

The specialization of a polynomial over π’ͺ_m at a parameter point x ∈ K^m: the polynomial over K whose coefficients are the values of the coefficients at x.

Equations
Instances For
    source
    theorem Analytic.coeff_specialize {K : Type u_1} [RCLike K] {m : β„•} (W : Polynomial β†₯(Conv K m)) (x : Fin m β†’ K) (k : β„•) :
    (specialize W x).coeff k = evalSeries (↑(W.coeff k)) x

    The coefficients of the specialization are the values of the coefficients.

    source
    theorem Analytic.natDegree_specialize_le {K : Type u_1} [RCLike K] {m : β„•} (W : Polynomial β†₯(Conv K m)) (x : Fin m β†’ K) :
    (specialize W x).natDegree ≀ W.natDegree

    Specialization does not raise the degree.

    source
    theorem Analytic.eval_specialize {K : Type u_1} [RCLike K] {m : β„•} (W : Polynomial β†₯(Conv K m)) (x : Fin m β†’ K) (t : K) :
    Polynomial.eval t (specialize W x) = βˆ‘ k ∈ Finset.range (W.natDegree + 1), evalSeries (↑(W.coeff k)) x * t ^ k

    The value of the specialized polynomial as the finite sum βˆ‘ W_k(x) t^k.

    source
    theorem Analytic.evalSeries_convPolyEval_eq_eval_specialize {K : Type u_1} [RCLike K] {m : β„•} (W : Polynomial β†₯(Conv K m)) :
    βˆ€αΆ  (x : Fin (m + 1) β†’ K) in nhds 0, evalSeries (↑((convPolyEval K) W)) x = Polynomial.eval (x 0) (specialize W (Fin.tail x))

    Near 0, the series of a polynomial W ∈ π’ͺ_m[x_0] evaluates as the specialized polynomial at the tail, evaluated at the first coordinate.

    source
    theorem Analytic.specialize_C {K : Type u_1} [RCLike K] {m : β„•} (c : β†₯(Conv K m)) (x : Fin m β†’ K) :
    specialize (Polynomial.C c) x = Polynomial.C (evalSeries (↑c) x)

    Specialization is exact on constants.

    source
    theorem Analytic.specialize_X {K : Type u_1} [RCLike K] {m : β„•} (x : Fin m β†’ K) :
    specialize Polynomial.X x = Polynomial.X

    Specialization is exact on X.

    source
    theorem Analytic.specialize_add_eventually {K : Type u_1} [RCLike K] {m : β„•} (W₁ Wβ‚‚ : Polynomial β†₯(Conv K m)) :
    βˆ€αΆ  (x : Fin m β†’ K) in nhds 0, specialize (W₁ + Wβ‚‚) x = specialize W₁ x + specialize Wβ‚‚ x

    Near 0, specialization is additive (each coefficient converges on a neighbourhood of 0).

    source
    theorem Analytic.specialize_mul_eventually {K : Type u_1} [RCLike K] {m : β„•} (W₁ Wβ‚‚ : Polynomial β†₯(Conv K m)) :
    βˆ€αΆ  (x : Fin m β†’ K) in nhds 0, specialize (W₁ * Wβ‚‚) x = specialize W₁ x * specialize Wβ‚‚ x

    Near 0, specialization is multiplicative (the products of coefficients evaluate as products, evalSeries_mul_eventually).

    source
    theorem Analytic.coe_natCast_conv {K : Type u_1} [RCLike K] {m : β„•} (k : β„•) :
    ↑↑k = ↑k

    The natural numbers of π’ͺ_m are the constant series.

    source
    theorem Analytic.evalSeries_natCast {K : Type u_1} [RCLike K] {m : β„•} (k : β„•) (x : Fin m β†’ K) :
    evalSeries (↑↑k) x = ↑k

    A natural number, as a series, evaluates to itself.

    source
    theorem Analytic.specialize_derivative_eventually {K : Type u_1} [RCLike K] {m : β„•} (W : Polynomial β†₯(Conv K m)) :
    βˆ€αΆ  (x : Fin m β†’ K) in nhds 0, specialize (Polynomial.derivative W) x = Polynomial.derivative (specialize W x)

    Near 0, specialization commutes with the derivative in X.

    source
    theorem Analytic.specialize_monic {K : Type u_1} [RCLike K] {m : β„•} {W : Polynomial β†₯(Conv K m)} (hW : W.Monic) (x : Fin m β†’ K) :
    (specialize W x).Monic

    The specialization of a monic polynomial is monic.

    source
    theorem Analytic.natDegree_specialize_of_monic {K : Type u_1} [RCLike K] {m : β„•} {W : Polynomial β†₯(Conv K m)} (hW : W.Monic) (x : Fin m β†’ K) :
    (specialize W x).natDegree = W.natDegree

    The specialization of a monic polynomial has the same degree.