Row coefficients of the truncated formal jet as a finite matrix sum

Proved

OAI.PiExponent.AdmissibleFormalInterpolation.truncatedFormalJet_row_sum

by Eyal1990 · Oct 16, 2026 · Mathlib 0df444a (Lean v4.33.1)

number-theoryopenai-pi-exponent-017

For a fixed strict row, the coefficient of the truncated formal jet equals the finite sum over admissible polynomial columns of the truncated logarithmic matrix entry times the polynomial’s column coefficient.

Preamble

import Definitions.Def_OAI_PiExponent_ApproximationDefinitions
import Definitions.Def_OAI_NumberTheory_PiExponent_Approximation_DeterminantContradiction_CoreData
import Definitions.Def_OAI_PiExponent_AdmissibleFormalInterpolation
import Definitions.Def_OAI_PiExponent_FormalJetShear
import Definitions.Def_OAI_PiExponent_AdmissibleFormalInterpolation_TruncatedJet

open OAI.PiExponent OAI.PiExponent.DeterminantContradiction
open OAI.PiExponent.AdmissibleFormalInterpolation

Formal statement

theorem OAI.PiExponent.AdmissibleFormalInterpolation.truncatedFormalJet_row_sum
    {m : ℕ} (K : ℕ) (w0 v0 theta : ℝ)
    (w : Fin m → ℝ) (H : ℝ) (r : Fin m → ℂ) (T : Fin m → ℕ)
    (hw0 : 0 < w0) (hv0 : 0 < v0) (htheta : 0 < theta)
    (hw : ∀ i, 0 < w i)
    (hT : ∀ i, w i / theta ≤ (T i : ℝ) * v0)
    (P : WeightedPolynomial w0 w H)
    (rho : InterpolationMatrix.Row K v0 theta w H) :
    MvPowerSeries.coeff (InterpolationMatrix.exponentVector rho.2.1)
        (truncatedFormalJet T (fun i => (rho.1.val : ℂ) * r i) P.val) =
      ∑ c : InterpolationMatrix.Column w0 w H,
        InterpolationMatrix.truncatedLogMatrix K w0 v0 theta w H r T rho c *
          MvPolynomial.coeff (InterpolationMatrix.exponentVector c.1) P.val := by sorry

Source

https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/NumberTheory/PiExponent/Approximation/AdmissibleMatrixGeometry.lean#L41-L44

View graph