RoundingKernel.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The alphabet-independent high-value bound for the actual projection operator. Positive vectors are determinized, padded, and rounded using proved finite constructions. No rounding or repetition hypothesis is exposed.

theorem OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.distribution_nonempty line 23
theorem OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.vectorEnergy_le_gap_rate line 32
Source documentation
Unit mass form of the Dinur--Steurer positive-vector approximation bound. The loss is independent of both alphabets and of the auxiliary dimension.
```
theorem vectorEnergy_le_gap_rate [Nonempty A₁] [Nonempty A₂]
    (K : ProjectionKernel Q₁ Q₂ A₁ A₂) (f : Ω → Q₁ → A₁ → ℝ)
    (hf : ∀ ω x a, 0 ≤ f ω x a) (hmass : ∀ x, vectorMass f x ≤ 1)
    {g : ℝ} (hg0 : 0 ≤ g) (hg1 : g ≤ 1)
    (hvalue : K.toGame.value ≤ 1 - g) :
    K.vectorEnergy f ≤ 1 - g ^ 2 / 8 := by
…
```
Mentions: OAI.UniqueGamesTheorem.Repetition.ProjectionKernel, OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.vectorMass