Addition law for weighted shears with a weight-preserving outer substitution
ProvedOAI.PiExponent.AdmissibleFormalInterpolation.weightedShear_comp_of_weightedOrdernumber-theoryopenai-pi-exponent-017
For positive coordinate weights, suppose E_i vanishes below degree N_i and u_i ≤ N_i v0. For any family D of power series and any real strict cutoff H, applying the finite shear by D and then by E equals the finite shear by D+E. Only the outer substitution needs the weighted-order condition, since it prevents omitted intermediate coefficients from returning below the cutoff.
Preamble
import Definitions.Def_OAI_PiExponent_WeightedJetShear open OAI.PiExponent OAI.PiExponent.AdmissibleFormalInterpolation
Formal statement
theorem OAI.PiExponent.AdmissibleFormalInterpolation.weightedShear_comp_of_weightedOrder
{m : ℕ} (v0 : ℝ) (u : Fin m → ℝ) (H : ℝ)
(N : Fin m → ℕ) (D E : Fin m → PowerSeries ℂ)
(hv0 : 0 < v0) (hu : ∀ i, 0 < u i)
(hN : ∀ i, u i ≤ (N i : ℝ) * v0)
(hE : ∀ i n, n < N i → PowerSeries.coeff n (E i) = 0) :
(weightedShear (m := m) v0 u H E) ∘ₗ
(weightedShear (m := m) v0 u H D) =
weightedShear (m := m) v0 u H (fun i : Fin m => D i + E i) := by sorrySource