Represent formal packets by the truncated logarithmic matrix
DisprovedOAI.PiExponent.AdmissibleFormalInterpolation.packet_matrix_representationnumber-theoryopenai-pi-exponent-017
Every admissible weighted polynomial's formal packet function is represented by the truncated logarithmic matrix applied to some column vector, under the stated positivity and truncation bounds.
Preamble
import Definitions.Def_OAI_PiExponent_ApproximationDefinitions import Definitions.Def_OAI_NumberTheory_PiExponent_Approximation_DeterminantContradiction_CoreData import Definitions.Def_OAI_PiExponent_AdmissibleFormalInterpolation open OAI.PiExponent OAI.PiExponent.DeterminantContradiction open OAI.PiExponent.AdmissibleFormalInterpolation
Formal statement
theorem OAI.PiExponent.AdmissibleFormalInterpolation.packet_matrix_representation {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) :
∃ x : InterpolationMatrix.Column w0 w H → ℂ,
packetMap K w0 v0 theta w H r P =
(InterpolationMatrix.truncatedLogMatrix K w0 v0 theta w H r T).mulVecLin x := by sorrySource