PolynomialZeroBound.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Polynomial zero counts over a finite prime field

The sample space contains every assignment of the finite variable set. In particular, using a product variable type imposes no restriction on repeated vector indices. The exact counting bound is obtained from the Schwartz–Zippel theorem by renaming variables and clearing positive denominators.

def OAI.MetricEntropyDuality.polynomialZeros line 28
Source documentation
The literal zero set in the full finite assignment space.
```
def polynomialZeros {V : Type uV} [Fintype V] (P : MvPolynomial V (ZMod p)) :
    Finset (V → ZMod p) := by
…
```
theorem OAI.MetricEntropyDuality.mem_polynomialZeros line 33
theorem OAI.MetricEntropyDuality.polynomial_zero_card_mul_le_fin line 39
theorem OAI.MetricEntropyDuality.polynomial_zero_card_mul_le line 63
Source documentation
Schwartz–Zippel as a natural-number inequality, for any finite variable type, including the empty variable type.
```
theorem polynomial_zero_card_mul_le {V : Type uV} [Fintype V]
    (P : MvPolynomial V (ZMod p)) (hP : P ≠ 0) :
    p * (polynomialZeros P).card ≤ P.totalDegree * p ^ Fintype.card V := by
…
```
Mentions: OAI.MetricEntropyDuality.polynomialZeros

theorem OAI.MetricEntropyDuality.polynomial_zero_card_mul_le_of_totalDegree_le line 96

Source documentation

A supplied upper bound for total degree gives the same exact zero count.

theorem polynomial_zero_card_mul_le_of_totalDegree_le {V : Type uV} [Fintype V]
    (P : MvPolynomial V (ZMod p)) (hP : P ≠ 0) {d : ℕ}
    (hdeg : P.totalDegree ≤ d) :
    p * (polynomialZeros P).card ≤ d * p ^ Fintype.card V :=
…

Mentions: OAI.MetricEntropyDuality.polynomialZeros

theorem OAI.MetricEntropyDuality.polynomial_zero_card_real_le line 103

Source documentation

The number of zeros is at most d/p times the number of assignments.

theorem polynomial_zero_card_real_le {V : Type uV} [Fintype V]
    (P : MvPolynomial V (ZMod p)) (hP : P ≠ 0) {d : ℕ}
    (hdeg : P.totalDegree ≤ d) :
    ((polynomialZeros P).card : ℝ) ≤
      (d : ℝ) / p * ((p ^ Fintype.card V : ℕ) : ℝ) := by
…

Mentions: OAI.MetricEntropyDuality.polynomialZeros

theorem OAI.MetricEntropyDuality.polynomial_zero_proportion_le line 120
Source documentation
The exact fraction of assignments on which the polynomial vanishes is at most d/p; this is the uniform-product probability formulation.
```
theorem polynomial_zero_proportion_le {V : Type uV} [Fintype V]
    (P : MvPolynomial V (ZMod p)) (hP : P ≠ 0) {d : ℕ}
    (hdeg : P.totalDegree ≤ d) :
    ((polynomialZeros P).card : ℝ) / ((p ^ Fintype.card V : ℕ) : ℝ) ≤
      (d : ℝ) / p := by
…
```
Mentions: OAI.MetricEntropyDuality.polynomialZeros