FormZeroCount.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Actual repeated-tuple zero events

The finite sample is a family of vectors. Currying identifies it with the scalar assignments of the literal tuple polynomial. No injectivity or nonzero-coordinate assumption is made on the sampled vectors or tuple indices.

theorem OAI.MetricEntropyDuality.tupleEvent_form_zero_card line 23
Source documentation
The original vector-sample event has exactly the polynomial zero count.
```
theorem tupleEvent_form_zero_card (F : SymmetricForm (ZMod p) r h)
    (a : Fin h → Fin u) :
    (tupleEvent (fun v => SymmetricForm.eval F v = 0) a).card =
      (polynomialZeros (tuplePolynomial F a)).card := by
…
```
Mentions: OAI.MetricEntropyDuality.SymmetricForm, OAI.MetricEntropyDuality.tupleEvent, OAI.MetricEntropyDuality.SymmetricForm.eval, OAI.MetricEntropyDuality.polynomialZeros, OAI.MetricEntropyDuality.tuplePolynomial
theorem OAI.MetricEntropyDuality.card_direction_samples line 36
Source documentation
The literal number of samples is the number of scalar assignments.
```
theorem card_direction_samples :
    Fintype.card (Fin u → Fin r → ZMod p) =
      p ^ Fintype.card (Fin u × Fin r) := by
…
```
theorem OAI.MetricEntropyDuality.tupleEvent_form_zero_card_mul_le line 44
Source documentation
Cross-multiplied finite zero count, including every repeated-index tuple.
```
theorem tupleEvent_form_zero_card_mul_le (hp : h < p)
    (F : SymmetricForm (ZMod p) r h) (hF : F ≠ 0)
    (a : Fin h → Fin u) :
    p * (tupleEvent (fun v => SymmetricForm.eval F v = 0) a).card ≤
      h * Fintype.card (Fin u → Fin r → ZMod p) := by
…
```
Mentions: OAI.MetricEntropyDuality.SymmetricForm, OAI.MetricEntropyDuality.tupleEvent, OAI.MetricEntropyDuality.SymmetricForm.eval

theorem OAI.MetricEntropyDuality.tupleEvent_form_zero_card_real_le line 54

Source documentation

Real zero count for the actual vector sample.

theorem tupleEvent_form_zero_card_real_le (hp : h < p)
    (F : SymmetricForm (ZMod p) r h) (hF : F ≠ 0)
    (a : Fin h → Fin u) :
    ((tupleEvent (fun v => SymmetricForm.eval F v = 0) a).card : ℝ) ≤
      (h : ℝ) / p * (Fintype.card (Fin u → Fin r → ZMod p) : ℝ) := by
…

Mentions: OAI.MetricEntropyDuality.SymmetricForm, OAI.MetricEntropyDuality.tupleEvent, OAI.MetricEntropyDuality.SymmetricForm.eval

theorem OAI.MetricEntropyDuality.tupleEvent_form_zero_proportion_le line 65
Source documentation
Uniform probability of a zero evaluation is at most h/p, with repetitions allowed in a. The denominator is the full finite vector-sample cardinality.
```
theorem tupleEvent_form_zero_proportion_le (hp : h < p)
    (F : SymmetricForm (ZMod p) r h) (hF : F ≠ 0)
    (a : Fin h → Fin u) :
    ((tupleEvent (fun v => SymmetricForm.eval F v = 0) a).card : ℝ) /
      (Fintype.card (Fin u → Fin r → ZMod p) : ℝ) ≤ (h : ℝ) / p := by
…
```
Mentions: OAI.MetricEntropyDuality.SymmetricForm, OAI.MetricEntropyDuality.tupleEvent, OAI.MetricEntropyDuality.SymmetricForm.eval