CollisionLemmas.lean`

61 declarations, 0 contain sorry, 0 declared as axioms

Finite conditional projection kernels for the Dinur--Steurer argument. The outer distribution samples the right question and the inner distribution samples the left question conditional on it. These are genuine normalized finite distributions; no norm inequality or repetition claim is a field.

structure OAI.UniqueGamesTheorem.Repetition.ProjectionKernel line 27
def OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.toGame line 39
theorem OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.toGame_isProjection line 49
def OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.apply line 53
Source documentation
Apply the projection operator to an arbitrary real assignment table.
```
def apply (K : ProjectionKernel Q₁ Q₂ A₁ A₂)
    (f : Q₁ → A₁ → ℝ) (y : Q₂) (b : A₂) : ℝ :=
…
```
Mentions: OAI.UniqueGamesTheorem.Repetition.ProjectionKernel
def OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.energy line 58
Source documentation
Squared Hilbert norm, with the actual right-question marginal.
```
def energy (K : ProjectionKernel Q₁ Q₂ A₁ A₂) (f : Q₁ → A₁ → ℝ) : ℝ :=
…
```
Mentions: OAI.UniqueGamesTheorem.Repetition.ProjectionKernel
def OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.assignment line 61
def OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.assignmentEnergy line 65
def OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.collisionValue line 69
Source documentation
Maximum squared collision norm of an ordinary deterministic left strategy.
```
def collisionValue [Nonempty A₁] (K : ProjectionKernel Q₁ Q₂ A₁ A₂) : ℝ := by
…
```
Mentions: OAI.UniqueGamesTheorem.Repetition.ProjectionKernel
def OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.vectorEnergy line 73
def OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.vectorMass line 76
theorem OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.energy_nonneg line 79
theorem OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.assignmentEnergy_le_collisionValue line 84
theorem OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.collisionValue_le_iff line 90
theorem OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.exists_optimal_assignment line 96
theorem OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.collisionValue_nonneg line 104
theorem OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.apply_assignment line 110
def OAI.UniqueGamesTheorem.Repetition.leftQuestionMarginal line 159
def OAI.UniqueGamesTheorem.Repetition.rightQuestionMarginal line 166
def OAI.UniqueGamesTheorem.Repetition.leftGivenRight line 175
Source documentation
The fallback exists even when the question types were not supplied with Nonempty instances: it is a marginal of the game's actual probability law.
```
def leftGivenRight (G : Game Q₁ Q₂ A₁ A₂) (y : Q₂) : FiniteDistribution Q₁ :=
…
```
theorem OAI.UniqueGamesTheorem.Repetition.rightQuestionMarginal_mul_leftGivenRight line 182
Source documentation
Exact disintegration, including right questions of marginal probability zero. The conditional law is never assumed to reconstruct the question law.
```
theorem rightQuestionMarginal_mul_leftGivenRight
    (G : Game Q₁ Q₂ A₁ A₂) (x : Q₁) (y : Q₂) :
    (rightQuestionMarginal G).weight y * (leftGivenRight G y).weight x =
      G.questions.weight (x, y) :=
…
```
Mentions: OAI.UniqueGamesTheorem.Repetition.rightQuestionMarginal, OAI.UniqueGamesTheorem.Repetition.leftGivenRight
def OAI.UniqueGamesTheorem.Repetition.kernelOfGame line 192
Source documentation
A projection game's predicate and actual question distribution determine the conditional kernel used by the collision argument.
```
def kernelOfGame (G : Game Q₁ Q₂ A₁ A₂) (hG : IsProjection G) :
    ProjectionKernel Q₁ Q₂ A₁ A₂ where
…
```
Mentions: OAI.UniqueGamesTheorem.Repetition.IsProjection, OAI.UniqueGamesTheorem.Repetition.ProjectionKernel
theorem OAI.UniqueGamesTheorem.Repetition.kernelOfGame_question_weight line 199
theorem OAI.UniqueGamesTheorem.Repetition.toGame_kernelOfGame line 204
theorem OAI.UniqueGamesTheorem.Repetition.kernelOfGame_success line 216
theorem OAI.UniqueGamesTheorem.Repetition.kernelOfGame_value line 222
def OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.reindex line 253
Source documentation
Transport both normalized question laws and the projection predicate.
```
def reindex (K : ProjectionKernel Q₁ Q₂ A₁ A₂)
    (eQ₁ : Q₁ ≃ R₁) (eQ₂ : Q₂ ≃ R₂)
    (eA₁ : A₁ ≃ B₁) (eA₂ : A₂ ≃ B₂) : ProjectionKernel R₁ R₂ B₁ B₂ where
…
```
Mentions: OAI.UniqueGamesTheorem.Repetition.ProjectionKernel

theorem OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.apply_reindex line 264

Source documentation

Reindexing the operator equals pulling back its assignment table.

theorem apply_reindex (K : ProjectionKernel Q₁ Q₂ A₁ A₂)
    (eQ₁ : Q₁ ≃ R₁) (eQ₂ : Q₂ ≃ R₂)
    (eA₁ : A₁ ≃ B₁) (eA₂ : A₂ ≃ B₂)
    (f : R₁ → B₁ → ℝ) (y : R₂) (b : B₂) :
    (K.reindex eQ₁ eQ₂ eA₁ eA₂).apply f y b =
      K.apply (fun x a => f (eQ₁ x) (eA₁ a)) (eQ₂.symm y) (eA₂.symm b) := by
…

Mentions: OAI.UniqueGamesTheorem.Repetition.ProjectionKernel, OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.apply

theorem OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.energy_reindex line 283
theorem OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.assignmentEnergy_reindex line 298

theorem OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.collisionValue_reindex line 321

Source documentation

No strategy is lost under bijective question and answer encodings.

theorem collisionValue_reindex [Nonempty A₁] [Nonempty B₁]
    (K : ProjectionKernel Q₁ Q₂ A₁ A₂)
    (eQ₁ : Q₁ ≃ R₁) (eQ₂ : Q₂ ≃ R₂)
    (eA₁ : A₁ ≃ B₁) (eA₂ : A₂ ≃ B₂) :
    (K.reindex eQ₁ eQ₂ eA₁ eA₂).collisionValue = K.collisionValue := by
…

Mentions: OAI.UniqueGamesTheorem.Repetition.ProjectionKernel, OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.collisionValue

theorem OAI.UniqueGamesTheorem.Repetition.FiniteLaw.probability_product_eq_left_expectation line 360
theorem OAI.UniqueGamesTheorem.Repetition.FiniteLaw.probability_product_eq_right_expectation line 372
theorem OAI.UniqueGamesTheorem.Repetition.FiniteLaw.expectation_mono line 385
def OAI.UniqueGamesTheorem.Repetition.leftFactorStrategy line 397
def OAI.UniqueGamesTheorem.Repetition.rightFactorStrategy line 402
theorem OAI.UniqueGamesTheorem.Repetition.success_product_le_left line 407
theorem OAI.UniqueGamesTheorem.Repetition.success_product_le_right line 423
theorem OAI.UniqueGamesTheorem.Repetition.product_value_le_min line 439
theorem OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.sq_expectation_le_expectation_sq line 468
theorem OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.apply_assignment_nonneg line 480
theorem OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.sum_apply_assignment_le_one line 488
Source documentation
The projected distribution has total mass at most one; missing mass is the possibility that a partial projection rejects the chosen left answer.
```
theorem sum_apply_assignment_le_one (K : ProjectionKernel Q₁ Q₂ A₁ A₂)
    (labels : Q₁ → A₁) (y : Q₂) :
    (∑ b, K.apply (assignment labels) y b) ≤ 1 := by
…
```
Mentions: OAI.UniqueGamesTheorem.Repetition.ProjectionKernel, OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.assignment
theorem OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.success_eq_outer_apply line 512
theorem OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.success_sq_le_assignmentEnergy line 527
theorem OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.value_sq_le_collisionValue line 541
theorem OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.exists_best_response line 549
Source documentation
Choose the actual best right answer separately at each right question.
```
theorem exists_best_response [Nonempty A₂]
    (K : ProjectionKernel Q₁ Q₂ A₁ A₂) (labels : Q₁ → A₁) :
    ∃ answers : Q₂ → A₂, ∀ y b,
      K.apply (assignment labels) y b ≤ K.apply (assignment labels) y (answers y) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Repetition.ProjectionKernel, OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.assignment
theorem OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.assignmentEnergy_le_value line 565
theorem OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.collisionValue_le_value line 591
theorem OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.collisionValue_le_one line 596
def OAI.UniqueGamesTheorem.Repetition.rowMass line 626
Source documentation
The mass at each vertex, before or after determinization.
```
def rowMass (h : V → A → ℝ) (v : V) : ℝ := ∑ a, h v a
```
def OAI.UniqueGamesTheorem.Repetition.deterministicVector line 629
Source documentation
Move the full mass of each row to its selected label.
```
def deterministicVector [DecidableEq A] (h : V → A → ℝ) (labels : V → A)
    (v : V) (a : A) : ℝ :=
…
```
theorem OAI.UniqueGamesTheorem.Repetition.deterministicVector_rowMass line 634
theorem OAI.UniqueGamesTheorem.Repetition.rowMass_nonnegative line 640
theorem OAI.UniqueGamesTheorem.Repetition.deterministicVector_nonnegative line 645
theorem OAI.UniqueGamesTheorem.Repetition.deterministicVector_linear_image line 653
theorem OAI.UniqueGamesTheorem.Repetition.entry_eq_zero_of_rowMass_eq_zero line 660
def OAI.UniqueGamesTheorem.Repetition.rowLaw line 668
Source documentation
A zero row is harmless and uses a fixed fallback label.
```
def rowLaw [Nonempty A] (h : V → A → ℝ) (hh : ∀ v a, 0 ≤ h v a)
    (v : V) : FiniteDistribution A := by
…
```
theorem OAI.UniqueGamesTheorem.Repetition.rowLaw_expectation_mul_mass line 684

theorem OAI.UniqueGamesTheorem.Repetition.square_expectation_le line 698

Source documentation

Finite Jensen for the square, proved by expanding nonnegative variance.

theorem square_expectation_le {Ω : Type*} [Fintype Ω]
    (law : FiniteDistribution Ω) (f : Ω → ℝ) :
    law.expectation f ^ 2 ≤ law.expectation (fun x => f x ^ 2) := by
…

theorem OAI.UniqueGamesTheorem.Repetition.exists_expectation_le line 725
theorem OAI.UniqueGamesTheorem.Repetition.exists_deterministic_preserving_mass line 746
Source documentation
One label per vertex preserves every row's mass and can only improve the nonnegative weighted squared image under any fixed linear map. In particular, the same theorem applies separately at each coordinate of a vector-valued assignment; no product or independence property of those coordinates is used.
```
theorem exists_deterministic_preserving_mass [Nonempty A]
    (h : V → A → ℝ) (hh : ∀ v a, 0 ≤ h v a)
    (w : T → ℝ) (hw : ∀ t, 0 ≤ w t) (c : T → V → A → ℝ) :
    ∃ labels : V → A,
      (∑ t, w t * (∑ v, ∑ a, c t v a * h v a) ^ 2) ≤
        ∑ t, w t * (∑ v, c t v (labels v) * rowMass h v) ^ 2 := by
…
```
Mentions: OAI.UniqueGamesTheorem.Repetition.rowMass

theorem OAI.UniqueGamesTheorem.Repetition.exists_deterministic_vector line 794

Source documentation

The same conclusion stated directly as a deterministic nonnegative vector. Its row masses are exactly those of the original vector.

theorem exists_deterministic_vector [Nonempty A] [DecidableEq A]
    (h : V → A → ℝ) (hh : ∀ v a, 0 ≤ h v a)
    (w : T → ℝ) (hw : ∀ t, 0 ≤ w t) (c : T → V → A → ℝ) :
    ∃ labels : V → A,
      (∀ v a, 0 ≤ deterministicVector h labels v a) ∧
      (∀ v, rowMass (deterministicVector h labels) v = rowMass h v) ∧
      (∑ t, w t * (∑ v, ∑ a, c t v a * h v a) ^ 2) ≤
        ∑ t, w t * (∑ v, ∑ a, c t v a * deterministicVector h labels v a) ^ 2 := by
…

Mentions: OAI.UniqueGamesTheorem.Repetition.deterministicVector, OAI.UniqueGamesTheorem.Repetition.rowMass