RoundingThresholdLemmas.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

Exact finite threshold expansion for unit vectors. A shared seed chooses one coordinate and one atom of the common threshold partition. Squared amplitudes are acceptance probabilities, and joint acceptance has the coordinatewise minimum law. The construction permits arbitrary vertex-dependent labels and arbitrary relations between their labels.

def OAI.UniqueGamesTheorem.Repetition.thresholdLevels line 28
Source documentation
All squared amplitudes, including repetitions, determine a single shared finite threshold partition.
```
def thresholdLevels (f : V → Ω → ℝ) : List ℝ := by
…
```
theorem OAI.UniqueGamesTheorem.Repetition.square_mem_thresholdLevels line 32
abbrev OAI.UniqueGamesTheorem.Repetition.ThresholdSeed line 39
Source documentation
The seed is a coordinate and a finite threshold interval.
```
abbrev ThresholdSeed (f : V → Ω → ℝ) := RectangleSeed (thresholdLevels f) Ω
```
Mentions: OAI.UniqueGamesTheorem.Repetition.thresholdLevels
def OAI.UniqueGamesTheorem.Repetition.thresholdDistribution line 41
theorem OAI.UniqueGamesTheorem.Repetition.thresholdSeed_nonempty line 44
def OAI.UniqueGamesTheorem.Repetition.thresholdAccept line 52
def OAI.UniqueGamesTheorem.Repetition.thresholdLabel line 56
Source documentation
Labels use only the local vertex and the shared coordinate.
```
def thresholdLabel (f : V → Ω → ℝ) (a : V → Ω → A) (x : V)
    (seed : ThresholdSeed f) : A := a x seed.1
```
Mentions: OAI.UniqueGamesTheorem.Repetition.ThresholdSeed
def OAI.UniqueGamesTheorem.Repetition.thresholdRate line 59
theorem OAI.UniqueGamesTheorem.Repetition.thresholdRate_positive line 61
theorem OAI.UniqueGamesTheorem.Repetition.square_le_one_of_row_norm line 66
theorem OAI.UniqueGamesTheorem.Repetition.threshold_acceptance_mass line 75
Source documentation
Every vertex accepts with the same positive mass, independently of its unit vector. Nonnegativity of the amplitudes is unnecessary for this lemma.
```
theorem threshold_acceptance_mass [Nonempty Ω] (f : V → Ω → ℝ)
    (hnorm : ∀ x, ∑ ω, f x ω ^ 2 = 1) (x : V) :
    (thresholdDistribution f).probability (thresholdAccept f x) = thresholdRate Ω := by
…
```
Mentions: OAI.UniqueGamesTheorem.Repetition.thresholdDistribution, OAI.UniqueGamesTheorem.Repetition.thresholdAccept, OAI.UniqueGamesTheorem.Repetition.thresholdRate

theorem OAI.UniqueGamesTheorem.Repetition.threshold_good_pair_mass line 87

Source documentation

Joint acceptance with any relation on the two local labels has exactly the minimum-overlap mass. Both vertices use the same coordinate and threshold.

theorem threshold_good_pair_mass [Nonempty Ω] (f : V → Ω → ℝ)
    (hnorm : ∀ x, ∑ ω, f x ω ^ 2 = 1) (a : V → Ω → A)
    (x y : V) (R : A → A → Prop) [DecidableRel R] :
    (thresholdDistribution f).probability (fun seed =>
      (thresholdAccept f x seed && thresholdAccept f y seed) &&
        decide (R (thresholdLabel f a x seed) (thresholdLabel f a y seed))) =
      thresholdRate Ω * ∑ ω,
        if R (a x ω) (a y ω) then min (f x ω ^ 2) (f y ω ^ 2) else 0 := by
…

Mentions: OAI.UniqueGamesTheorem.Repetition.thresholdDistribution, OAI.UniqueGamesTheorem.Repetition.thresholdAccept, OAI.UniqueGamesTheorem.Repetition.thresholdLabel, OAI.UniqueGamesTheorem.Repetition.thresholdRate

theorem OAI.UniqueGamesTheorem.Repetition.threshold_good_pair_mass_bool line 129

Source documentation

Boolean-predicate form used by finite games and the shared sampler.

theorem threshold_good_pair_mass_bool [Nonempty Ω] (f : V → Ω → ℝ)
    (hnorm : ∀ x, ∑ ω, f x ω ^ 2 = 1) (a : V → Ω → A)
    (x y : V) (R : A → A → Bool) :
    (thresholdDistribution f).probability (fun seed =>
      (thresholdAccept f x seed && thresholdAccept f y seed) &&
        R (thresholdLabel f a x seed) (thresholdLabel f a y seed)) =
      thresholdRate Ω * ∑ ω,
        if R (a x ω) (a y ω) then min (f x ω ^ 2) (f y ω ^ 2) else 0 := by
…

theorem OAI.UniqueGamesTheorem.Repetition.threshold_average_good_mass line 164
theorem OAI.UniqueGamesTheorem.Repetition.exists_labeling_high_value line 181
Source documentation
Unit squared row mass converts a large collision energy into a genuinely local deterministic labeling. All randomness used by the proof is independent of the sampled constraint, and the final answer has no random seed.
```
theorem exists_labeling_high_value (ν : FiniteDistribution E)
    (left right : E → V) (R : E → A → A → Bool)
    (a : V → Ω → A) (f : V → Ω → ℝ)
    (hf : ∀ v ω, 0 ≤ f v ω) (hrow : ∀ v, rowSquareMass f v = 1) :
    ∃ labels : V → A,
      1 - 2 * Real.sqrt (2 * (1 - pairEnergy ν left right R a f)) ≤
        partialLabelScore ν left right R labels := by
…
```
Mentions: OAI.UniqueGamesTheorem.Repetition.rowSquareMass, OAI.UniqueGamesTheorem.Repetition.pairEnergy, OAI.UniqueGamesTheorem.Repetition.partialLabelScore

theorem OAI.UniqueGamesTheorem.Repetition.exists_labeling_high_value_of_rows_le_one line 201

Source documentation

Rows of mass at most one are completed by private vertex coordinates. Their nonnegative contribution only improves the collision energy.

theorem exists_labeling_high_value_of_rows_le_one (ν : FiniteDistribution E)
    (left right : E → V) (R : E → A → A → Bool)
    (a : V → Ω → A) (f : V → Ω → ℝ)
    (hf : ∀ v ω, 0 ≤ f v ω) (hrow : ∀ v, rowSquareMass f v ≤ 1) :
    ∃ labels : V → A,
      1 - 2 * Real.sqrt (2 * (1 - pairEnergy ν left right R a f)) ≤
        partialLabelScore ν left right R labels := by
…

Mentions: OAI.UniqueGamesTheorem.Repetition.rowSquareMass, OAI.UniqueGamesTheorem.Repetition.pairEnergy, OAI.UniqueGamesTheorem.Repetition.partialLabelScore

theorem OAI.UniqueGamesTheorem.Repetition.pairEnergy_le_of_labeling_gap line 226

Source documentation

A genuine gap for every deterministic labeling bounds the vector energy by an alphabet-independent quadratic gap.

theorem pairEnergy_le_of_labeling_gap (ν : FiniteDistribution E)
    (left right : E → V) (R : E → A → A → Bool)
    (a : V → Ω → A) (f : V → Ω → ℝ)
    (hf : ∀ v ω, 0 ≤ f v ω) (hrow : ∀ v, rowSquareMass f v ≤ 1)
    {g : ℝ} (hg : 0 < g)
    (hgap : ∀ labels : V → A, partialLabelScore ν left right R labels ≤ 1 - g) :
    pairEnergy ν left right R a f ≤ 1 - g ^ 2 / 8 := by
…

Mentions: OAI.UniqueGamesTheorem.Repetition.rowSquareMass, OAI.UniqueGamesTheorem.Repetition.partialLabelScore, OAI.UniqueGamesTheorem.Repetition.pairEnergy