Extend the monomial identity to polynomials
ProvedOAI.PiExponent.AdmissibleFormalInterpolation.weightedShear_seriesJet_linearExtensionnumber-theoryopenai-pi-exponent-017
If the shear identity holds for every unit-coefficient monomial, complex linearity extends it to every polynomial through its finite monomial expansion.
Preamble
import Definitions.Def_OAI_PiExponent_WeightedJetShear open OAI.PiExponent OAI.PiExponent.AdmissibleFormalInterpolation
Formal statement
theorem OAI.PiExponent.AdmissibleFormalInterpolation.weightedShear_seriesJet_linearExtension
{m : ℕ} (v0 : ℝ) (u : Fin m → ℝ) (H : ℝ)
(N : Fin m → ℕ) (D F : Fin m → PowerSeries ℂ)
(hv0 : 0 < v0) (hu : ∀ i, 0 < u i)
(hN : ∀ i, u i ≤ (N i : ℝ) * v0)
(hD : ∀ i n, n < N i → PowerSeries.coeff n (D i) = 0)
(hH : 0 < H)
(c : Fin m → ℂ) (P : MvPolynomial (Fin (m + 1)) ℂ)
(hmono : ∀ e : Fin (m + 1) →₀ ℕ,
(weightedShear (m := m) v0 u H D).toFun
(weightedSeriesJet (m := m) v0 u H c F
(MvPolynomial.monomial e 1)) =
weightedSeriesJet (m := m) v0 u H c (fun i => F i + D i)
(MvPolynomial.monomial e 1)) :
(weightedShear (m := m) v0 u H D).toFun
(weightedSeriesJet (m := m) v0 u H c F P) =
weightedSeriesJet (m := m) v0 u H c (fun i => F i + D i) P := by sorrySource