FormalConjectures.Mathoverflow.«339137»

/-
Copyright 2025 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/

import FormalConjecturesUtil
import FormalConjectures.GreensOpenProblems.«28»

Mathoverflow 339137

Why do polynomials with coefficients 0,1 like to have only factors with 0,1 coefficients?

Reference: mathoverflow/339137 asked by user Sil

open scoped Polynomialnamespace Mathoverflow339137

The predicate that all coefficients of a polynomial are either zero or one. P.coeffs is the finite set of all nonzero coefficients of the polynomial P. So IsZeroOne P means that every nonzero coefficient of P is equal to 1. Note that zero coefficients are not included in P.coeffs.

def IsZeroOne (P : ℝ[X]) := P.coeffs ⊆ {1}

Let $P(x), Q(x) ∈ ℝ[x]$ be two monic polynomials with non-negative coefficients. If $R(x) = P(x)Q(x)$ is a $0,1$ polynomial (coefficients only from ${0,1}$), then $P(x)$ and $Q(x)$ are also $0, 1$ polynomials.

@[category research open, AMS 12]
theorem declaration uses 'sorry'mathoverflow_339137 (P Q R : ℝ[X]) (hP: P.Monic) (hQ : Q.Monic)
    (hp : ∀ c ∈ P.coeffs, 0 ≤ c) (hq : ∀ c ∈ Q.coeffs, 0 ≤ c)
    (h : R = P * Q) (hR : IsZeroOne R) :
    IsZeroOne P ∧ IsZeroOne Q := byP:ℝ[X]Q:ℝ[X]R:ℝ[X]hP:P.MonichQ:Q.Monichp:∀ c ∈ P.coeffs, 0 ≤ chq:∀ c ∈ Q.coeffs, 0 ≤ ch:R = P * QhR:IsZeroOne R⊢ IsZeroOne P ∧ IsZeroOne Q
  sorryAll goals completed! 🐙

Green's Open Problem 28 is the probabilistic reformulation of Mathoverflow 339137.

Suppose that $X, Y$ are two finitely-supported independent random variables taking integer values, and such that $X + Y$ is uniformly distributed on its range. Are $X$ and $Y$ themselves uniformly distributed on their ranges?

Mathematically, this equivalence is established via Probability Generating Functions (PGFs), shifting the support to $\mathbb{N}$, and appropriately scaling the coefficients.

@[category textbook, AMS 60]
theorem declaration uses 'sorry'mathoverflow_339137_probabilistic :
    type_of% Mathoverflow339137.mathoverflow_339137 ↔ type_of% Green28.green_28 := by⊢ (∀ (P Q R : ℝ[X]),
    P.Monic →
      Q.Monic →
        (∀ c ∈ P.coeffs, 0 ≤ c) → (∀ c ∈ Q.coeffs, 0 ≤ c) → R = P * Q → IsZeroOne R → IsZeroOne P ∧ IsZeroOne Q) ↔
  (sorry ↔
    ∀ (X Y : PMF ℤ),
      X.support.Finite ∧ Y.support.Finite ∧ Green28.IsUniformOnSupport (Green28.indepSum X Y) →
        Green28.IsUniformOnSupport X ∧ Green28.IsUniformOnSupport Y)
  sorryAll goals completed! 🐙


end Mathoverflow339137