RobustDirections.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Actual directions surviving deletion

The sample is the full finite product of indexed vectors over ZMod p. The actual symmetric-form count and the zero bound for every repeated-index tuple feed the disjoint-witness union bound. A finite maximum disjoint family then produces the surviving set separately for each nonzero form.

theorem OAI.MetricEntropyDuality.exists_robust_directions_of_budget line 26

Source documentation

The actual finite-field direction construction with an explicit deletion budget. One sample works for every nonzero form; its surviving subset may depend on that form. All ordered tuples, including repetitions, are retained.

theorem exists_robust_directions_of_budget
    {p r h u : ℕ} [Fact p.Prime]
    (hr : 0 < r) (hh : 0 < h) (hu : 0 < u)
    {θ : ℝ} (hθ : θ < 1)
    (hdel : (h : ℝ) * (2 * (formDimension r h : ℝ)) ≤ θ * (u : ℝ))
    (hp_h : h < p) (hp_size : h ^ 2 * u ^ (2 * h) < p) :
    ∃ t : Fin u → Fin r → ZMod p,
      ∀ F : SymmetricForm (ZMod p) r h, F ≠ 0 →
        ∃ T : Finset (Fin u),
          ((Finset.univ \ T).card : ℝ) ≤ θ * (u : ℝ) ∧ T.Nonempty ∧
          ∀ a : Fin h → Fin u, (∀ j, a j ∈ T) →
            SymmetricForm.eval F (fun j => t (a j)) ≠ 0 := by
…

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

theorem OAI.MetricEntropyDuality.exists_robust_directions line 99

Source documentation

The ceiling-defined direction count satisfies the deletion budget. The field size is chosen after r, h, and θ.

theorem exists_robust_directions
    {p r h : ℕ} [Fact p.Prime] (hr : 0 < r) (hh : 0 < h)
    {θ : ℝ} (hθ0 : 0 < θ) (hθ1 : θ < 1)
    (hp_h : h < p)
    (hp_size : h ^ 2 * (directionCount r h θ) ^ (2 * h) < p) :
    ∃ t : Fin (directionCount r h θ) → Fin r → ZMod p,
      ∀ F : SymmetricForm (ZMod p) r h, F ≠ 0 →
        ∃ T : Finset (Fin (directionCount r h θ)),
          ((Finset.univ \ T).card : ℝ) ≤ θ * (directionCount r h θ : ℝ) ∧
            T.Nonempty ∧
          ∀ a : Fin h → Fin (directionCount r h θ), (∀ j, a j ∈ T) →
            SymmetricForm.eval F (fun j => t (a j)) ≠ 0 :=
…

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