Shear coordinates have no terms below their assigned weights
ProvedOAI.PiExponent.LogarithmicJetIdeals.weighted_shear_coordinate_coefficientsnumber-theoryopenai-pi-exponent-017
The coefficient cutoff on each correction series ensures that every nonzero coefficient of each inverse shear coordinate has weight at least its assigned coordinate weight, including equality at the boundary.
Preamble
import Definitions.Def_OAI_PiExponent_AdmissibleFormalInterpolation import Definitions.Def_OAI_PiExponent_LogarithmicJetIdeals_LocalCoordinatePolynomial open OAI.PiExponent open OAI.PiExponent.AdmissibleFormalInterpolation open scoped BigOperators
Formal statement
theorem OAI.PiExponent.LogarithmicJetIdeals.weighted_shear_coordinate_coefficients
{m : ℕ} (q : Fin (m + 1) → ℝ) (hq : ∀ j, 0 < q j)
(D : Fin m → PowerSeries ℂ)
(hD : ∀ i : Fin m, ∀ n : ℕ,
(n : ℝ) * q 0 < q i.succ → PowerSeries.coeff n (D i) = 0) :
∀ i : Fin (m + 1), ∀ b : Fin (m + 1) →₀ ℕ,
MvPowerSeries.coeff b
(Fin.cases (MvPowerSeries.X 0)
(fun i => MvPowerSeries.X i.succ - liftLogSeries m (D i)) i) ≠ 0 →
q i ≤ ∑ j, q j * (b j : ℝ) := by sorrySource