Cancellation of opposite shears on strict weighted coefficient jets
ProvedOAI.PiExponent.AdmissibleFormalInterpolation.weightedShear_neg_leftInversenumber-theoryopenai-pi-exponent-017
For positive weights and positive strict cutoff, suppose D_i vanishes below degree N_i and u_i ≤ N_i v0. The finite coefficient operators for translation by D and then -D compose to the identity linear map. Both translations preserve weight, so intermediate truncation is harmless. Equality in the weight bound is allowed, and weight exactly H is excluded. When m = 0 the operator is the identity; N_i = 0 is incompatible with the hypotheses.
Preamble
import Definitions.Def_OAI_PiExponent_WeightedJetShear open OAI.PiExponent OAI.PiExponent.AdmissibleFormalInterpolation
Formal statement
theorem OAI.PiExponent.AdmissibleFormalInterpolation.weightedShear_neg_leftInverse
{m : ℕ} (v0 : ℝ) (u : Fin m → ℝ) (H : ℝ)
(N : Fin m → ℕ) (D : 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) :
(weightedShear (m := m) v0 u H (fun i : Fin m => -D i)) ∘ₗ
(weightedShear (m := m) v0 u H D) =
(LinearMap.id :
((↥(strictWeightedSimplex (Fin.cases v0 u) H)) → ℂ) →ₗ[ℂ]
((↥(strictWeightedSimplex (Fin.cases v0 u) H)) → ℂ)) := by sorrySource