Coefficient of a product of finite single-coordinate monomial sums

Proved

OAI.PiExponent.FinitePeriodCollision.coeff_prod_single_coordinate_monomial_sum

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

irrationality-measurenumber-theoryopenai-pi-exponent-017

The coefficient of a product of finite single-coordinate monomial sums is the product of the requested coefficients, with zero whenever a requested exponent is absent.

Preamble

import Mathlib.Algebra.MvPolynomial.Basic
open scoped BigOperators

Formal statement

theorem OAI.PiExponent.FinitePeriodCollision.coeff_prod_single_coordinate_monomial_sum
    {σ : Type} [Fintype σ] [DecidableEq σ] {R : Type} [CommSemiring R]
    (S : σ → Finset ℕ) (c : σ → ℕ → R) (A : σ → ℕ) :
    (∏ i, ∑ n ∈ S i,
      MvPolynomial.monomial (Finsupp.single i n) (c i n)).coeff
        (Finsupp.equivFunOnFinite.symm A) =
      ∏ i, if A i ∈ S i then c i (A i) else 0 := by sorry

Source

https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/NumberTheory/PiExponent/Analysis/Collision.lean, formal_period_collision_bound; https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/NumberTheory/PiExponent/Analysis/DeterminantAnalyticBound.lean, translated_summand_bound and log_norm_sum_le; https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/NumberTheory/PiExponent/Analysis/TranslationCountLimit.lean, translationTermCount. Synthesized explicit actual-matrix bridge obligation for Approximation/DeterminantContradiction.lean, AnalyticAggregateStatement; not claimed to be proved by those source lemmas.

View graph