FormalConjectures/Mathoverflow/339137.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

3 declarations, 2 contain sorry, 0 declared as axioms

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

Imports (2)
  1. def Mathoverflow339137.IsZeroOne The predicate that all coefficients of a polynomial are either zero or one line 43 source

    Source documentation

    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.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Polynomial, Real

    Proof uses: LE.le, Finset, Polynomial.coeffs, Singleton.singleton, OfNat.ofNat

    8 instances, coercions and auxiliary constants left out.

    def IsZeroOne (P : ℝ[X]) := P.coeffs ⊆ {1}
…
  2. theorem Mathoverflow339137.mathoverflow_339137 Let $P(x), Q(x) ∈ ℝ[x]$ be two monic polynomials with non-negative coefficients sorry line 53 source

    Source documentation

    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.

    depends on sorry what this means

    Statement uses: Polynomial, Real, Polynomial.Monic, Membership.mem, Finset, Polynomial.coeffs, LE.le, OfNat.ofNat, Eq, HMul.hMul, Mathoverflow339137.IsZeroOne, And

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Nat

    17 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

    theorem 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 := by
…

    Mentions: c, Mathoverflow339137.IsZeroOne

  3. theorem Mathoverflow339137.mathoverflow_339137_probabilistic Green's Open Problem 28 is the probabilistic reformulation of Mathoverflow 339137 sorry line 70 source

    Source documentation

    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.

    depends on sorry what this means

    Statement uses: Iff, Polynomial, Real, Polynomial.Monic, Membership.mem, Finset, Polynomial.coeffs, LE.le, OfNat.ofNat, Eq, HMul.hMul, Mathoverflow339137.IsZeroOne, And, True, PMF, Int, Set.Finite, PMF.support, Green28.IsUniformOnSupport, Green28.indepSum

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Nat

    17 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

    theorem mathoverflow_339137_probabilistic :
    type_of% Mathoverflow339137.mathoverflow_339137 ↔ type_of% Green28.green_28 := by
…

    Mentions: Mathoverflow339137.mathoverflow_339137, Green28.green_28