Weighted series jets on the empty strict simplex
ProvedOAI.PiExponent.AdmissibleFormalInterpolation.weighted_series_jet_equiv_of_coeff_agreement_nonposnumber-theoryopenai-pi-exponent-017
When H is nonpositive, positivity of the coordinate weights makes the strict weighted simplex empty. The resulting coefficient-function space is trivial, so the requested equivalence and jet identity hold.
Preamble
import Definitions.Def_OAI_PiExponent_WeightedSeriesJets open OAI.PiExponent OAI.PiExponent.AdmissibleFormalInterpolation
Formal statement
theorem OAI.PiExponent.AdmissibleFormalInterpolation.weighted_series_jet_equiv_of_coeff_agreement_nonpos
{m : ℕ} (v0 : ℝ) (u : Fin m → ℝ) (H : ℝ)
(N : Fin m → ℕ) (F G : Fin m → PowerSeries ℂ)
(hv0 : 0 < v0) (hu : ∀ i, 0 < u i)
(hN : ∀ i, u i ≤ (N i : ℝ) * v0)
(hFG : ∀ i n, n < N i → PowerSeries.coeff n (F i) = PowerSeries.coeff n (G i))
(hH : H ≤ 0) :
∃ E : ((↥(strictWeightedSimplex (Fin.cases v0 u) H)) → ℂ) ≃ₗ[ℂ]
((↥(strictWeightedSimplex (Fin.cases v0 u) H)) → ℂ),
∀ (c : Fin m → ℂ) (P : MvPolynomial (Fin (m + 1)) ℂ),
E (weightedSeriesJet v0 u H c G P) = weightedSeriesJet v0 u H c F P := by sorrySource