OAI/Computability/MaxCut/PCP/ProductCollisionBounds.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

Comparison of the actual classical game value with the squared collision norm. Both directions are proved for the normalized conditional kernel, including partial projection constraints and zero-weight questions.

  1. theorem OAI.MaxCutGames.Repetition.ProjectionKernel.sq_expectation_le_expectation_sq line 22
  2. theorem OAI.MaxCutGames.Repetition.ProjectionKernel.apply_assignment_nonneg line 34
  3. theorem OAI.MaxCutGames.Repetition.ProjectionKernel.sum_apply_assignment_le_one line 42

    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.MaxCutGames.Repetition.ProjectionKernel, OAI.MaxCutGames.Repetition.ProjectionKernel.assignment

  4. theorem OAI.MaxCutGames.Repetition.ProjectionKernel.success_eq_outer_apply line 66
  5. theorem OAI.MaxCutGames.Repetition.ProjectionKernel.success_sq_le_assignmentEnergy line 81
  6. theorem OAI.MaxCutGames.Repetition.ProjectionKernel.value_sq_le_collisionValue line 95
  7. theorem OAI.MaxCutGames.Repetition.ProjectionKernel.exists_best_response line 103

    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.MaxCutGames.Repetition.ProjectionKernel, OAI.MaxCutGames.Repetition.ProjectionKernel.assignment

  8. theorem OAI.MaxCutGames.Repetition.ProjectionKernel.assignmentEnergy_le_value line 119
  9. theorem OAI.MaxCutGames.Repetition.ProjectionKernel.collisionValue_le_value line 145
  10. theorem OAI.MaxCutGames.Repetition.ProjectionKernel.collisionValue_le_one line 150
  11. theorem OAI.MaxCutGames.Repetition.ProjectionKernel.distribution_nonempty_inline_RoundingKernel line 158
  12. theorem OAI.MaxCutGames.Repetition.ProjectionKernel.vectorEnergy_le_gap_rate line 167

    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.MaxCutGames.Repetition.ProjectionKernel, OAI.MaxCutGames.Repetition.ProjectionKernel.vectorMass

  13. def OAI.MaxCutGames.Repetition.kernelApply line 230

    Source documentation

    Apply a finite real kernel. Output indices need no finiteness assumption.

    def kernelApply (K : Y → B → X → A → ℝ) (f : X → A → ℝ) (y : Y) (b : B) : ℝ :=
…
  14. def OAI.MaxCutGames.Repetition.tensorKernel line 234

    Source documentation

    Independent tensor of two kernels.

    def tensorKernel (K : Y → B → X → A → ℝ) (L : Z → C → U → D → ℝ)
    (yz : Y × Z) (bc : B × C) (xu : X × U) (ad : A × D) : ℝ :=
…
  15. theorem OAI.MaxCutGames.Repetition.kernelApply_tensor line 240

    Source documentation

    Applying the tensor first applies L separately for every fixed input of K, and then applies K. This is valid for arbitrary coupled inputs.

    theorem kernelApply_tensor
    (K : Y → B → X → A → ℝ) (L : Z → C → U → D → ℝ)
    (f : (X × U) → (A × D) → ℝ) (y : Y) (z : Z) (b : B) (c : C) :
    kernelApply (tensorKernel K L) f (y,z) (b,c) =
      kernelApply K (fun x a => kernelApply L (fun u d => f (x,u) (a,d)) z c) y b := by
…

    Mentions: OAI.MaxCutGames.Repetition.kernelApply, OAI.MaxCutGames.Repetition.tensorKernel

  16. theorem OAI.MaxCutGames.Repetition.kernelApply_nonnegative line 254
  17. theorem OAI.MaxCutGames.Repetition.kernelApply_sum line 265

    Source documentation

    Summing a family of input functions commutes with the finite operator.

    theorem kernelApply_sum
    (K : Y → B → X → A → ℝ) (f : I → X → A → ℝ) (y : Y) (b : B) :
    kernelApply K (fun x a => ∑ i, f i x a) y b =
      ∑ i, kernelApply K (f i) y b := by
…

    Mentions: OAI.MaxCutGames.Repetition.kernelApply

  18. theorem OAI.MaxCutGames.Repetition.kernelApply_smul line 279
  19. theorem OAI.MaxCutGames.Repetition.kernelApply_slice_mass line 292

    Source documentation

    Marginalizing the first answer of a joint input strategy after applying the second kernel is the same as applying the kernel to the answer marginal.

    theorem kernelApply_slice_mass
    (L : Z → C → U → D → ℝ) (f : (X × U) → (A × D) → ℝ)
    (x : X) (z : Z) (c : C) :
    (∑ a, kernelApply L (fun u d => f (x,u) (a,d)) z c) =
      kernelApply L (fun u d => ∑ a, f (x,u) (a,d)) z c := by
…

    Mentions: OAI.MaxCutGames.Repetition.kernelApply

  20. def OAI.MaxCutGames.Repetition.ProjectionKernel.coefficients line 312

    Source documentation

    The coefficient form of the conditional projection operator.

    def coefficients (K : ProjectionKernel Q₁ Q₂ A₁ A₂)
    (y : Q₂) (b : A₂) (x : Q₁) (a : A₁) : ℝ :=
…

    Mentions: OAI.MaxCutGames.Repetition.ProjectionKernel

  21. theorem OAI.MaxCutGames.Repetition.ProjectionKernel.apply_eq_kernelApply line 316
  22. theorem OAI.MaxCutGames.Repetition.ProjectionKernel.apply_nonnegative line 328
  23. theorem OAI.MaxCutGames.Repetition.ProjectionKernel.apply_sum line 340
  24. theorem OAI.MaxCutGames.Repetition.ProjectionKernel.apply_smul line 346
  25. def OAI.MaxCutGames.Repetition.ProjectionKernel.product line 353

    Source documentation

    Independent product of the outer and conditional laws.

    def product (K : ProjectionKernel Q₁ Q₂ A₁ A₂)
    (H : ProjectionKernel R₁ R₂ B₁ B₂) :
    ProjectionKernel (Q₁ × R₁) (Q₂ × R₂) (A₁ × B₁) (A₂ × B₂) where
…

    Mentions: OAI.MaxCutGames.Repetition.ProjectionKernel

  26. theorem OAI.MaxCutGames.Repetition.ProjectionKernel.coefficients_product line 365
  27. theorem OAI.MaxCutGames.Repetition.ProjectionKernel.apply_product line 374

    Source documentation

    Arbitrary product inputs factor through the second game operator.

    theorem apply_product (K : ProjectionKernel Q₁ Q₂ A₁ A₂)
    (H : ProjectionKernel R₁ R₂ B₁ B₂)
    (f : (Q₁ × R₁) → (A₁ × B₁) → ℝ)
    (y : Q₂) (z : R₂) (b : A₂) (c : B₂) :
    (K.product H).apply f (y,z) (b,c) =
      K.apply (fun x a => H.apply (fun u d => f (x,u) (a,d)) z c) y b := by
…

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

  28. theorem OAI.MaxCutGames.Repetition.ProjectionKernel.toGame_product line 385

    Source documentation

    The kernel tensor realizes the ordinary independent conjunction game.

    theorem toGame_product (K : ProjectionKernel Q₁ Q₂ A₁ A₂)
    (H : ProjectionKernel R₁ R₂ B₁ B₂) :
    (K.product H).toGame = MaxCutGames.Repetition.product K.toGame H.toGame := by
…

    Mentions: OAI.MaxCutGames.Repetition.ProjectionKernel, OAI.MaxCutGames.Repetition.ProjectionKernel.toGame, OAI.MaxCutGames.Repetition.product

  29. def OAI.MaxCutGames.Repetition.ProjectionKernel.tensorSlice line 413

    Source documentation

    Apply the second game to a fixed first question and first answer. The square-root factor changes its weighted output space into counting measure.

    def tensorSlice (H : ProjectionKernel R₁ R₂ B₁ B₂)
    (labels : (Q₁ × R₁) → (A₁ × B₁))
    (ω : R₂ × B₂) (x : Q₁) (a : A₁) : ℝ :=
…

    Mentions: OAI.MaxCutGames.Repetition.ProjectionKernel

  30. theorem OAI.MaxCutGames.Repetition.ProjectionKernel.tensorSlice_nonnegative line 420
  31. theorem OAI.MaxCutGames.Repetition.ProjectionKernel.sum_assignment_product line 434

    Source documentation

    Marginalizing the first label of a deterministic product strategy leaves the deterministic second-label strategy.

    theorem sum_assignment_product (labels : (Q₁ × R₁) → (A₁ × B₁))
    (x : Q₁) (u : R₁) (d : B₁) :
    (∑ a, assignment labels (x,u) (a,d)) =
      assignment (fun r => (labels (x,r)).2) u d := by
…

    Mentions: OAI.MaxCutGames.Repetition.ProjectionKernel.assignment

  32. theorem OAI.MaxCutGames.Repetition.ProjectionKernel.tensorSlice_label_mass line 442
  33. theorem OAI.MaxCutGames.Repetition.ProjectionKernel.vectorMass_tensorSlice line 454

    Source documentation

    The fiber mass is an actual collision energy of the second game, not a free normalization assumption.

    theorem vectorMass_tensorSlice (H : ProjectionKernel R₁ R₂ B₁ B₂)
    (labels : (Q₁ × R₁) → (A₁ × B₁)) (x : Q₁) :
    vectorMass (H.tensorSlice labels) x =
      H.assignmentEnergy (fun r => (labels (x,r)).2) := by
…

    Mentions: OAI.MaxCutGames.Repetition.ProjectionKernel, OAI.MaxCutGames.Repetition.ProjectionKernel.vectorMass

  34. theorem OAI.MaxCutGames.Repetition.ProjectionKernel.vectorMass_tensorSlice_le line 467
  35. theorem OAI.MaxCutGames.Repetition.ProjectionKernel.vectorEnergy_tensorSlice line 475

    Source documentation

    Exact Hilbert-norm factorization, with every marginal weight retained.

    theorem vectorEnergy_tensorSlice (K : ProjectionKernel Q₁ Q₂ A₁ A₂)
    (H : ProjectionKernel R₁ R₂ B₁ B₂)
    (labels : (Q₁ × R₁) → (A₁ × B₁)) :
    K.vectorEnergy (H.tensorSlice labels) = (K.product H).assignmentEnergy labels := by
…

    Mentions: OAI.MaxCutGames.Repetition.ProjectionKernel, OAI.MaxCutGames.Repetition.ProjectionKernel.assignmentEnergy

  36. theorem OAI.MaxCutGames.Repetition.ProjectionKernel.vectorMass_smul line 530
  37. theorem OAI.MaxCutGames.Repetition.ProjectionKernel.energy_smul line 536
  38. theorem OAI.MaxCutGames.Repetition.ProjectionKernel.vectorEnergy_smul line 547
  39. theorem OAI.MaxCutGames.Repetition.ProjectionKernel.entry_eq_zero_of_vectorMass_nonpositive line 555
  40. theorem OAI.MaxCutGames.Repetition.ProjectionKernel.vectorEnergy_eq_zero_of_mass_nonpositive line 569
  41. theorem OAI.MaxCutGames.Repetition.ProjectionKernel.vectorEnergy_le_of_unit_bound line 582

    Source documentation

    A unit-mass estimate extends to any nonnegative mass bound, including zero. The hypothesis is precisely the unit-mass analytic estimate being normalized; the normalization itself assumes no repetition bound.

    theorem vectorEnergy_le_of_unit_bound
    (K : ProjectionKernel Q₁ Q₂ A₁ A₂) (ρ C : ℝ)
    (unit_bound : ∀ f : Ω → Q₁ → A₁ → ℝ,
      (∀ ω x a, 0 ≤ f ω x a) → (∀ x, vectorMass f x ≤ 1) → K.vectorEnergy f ≤ ρ)
    (hC : 0 ≤ C) (f : Ω → Q₁ → A₁ → ℝ)
    (hf : ∀ ω x a, 0 ≤ f ω x a) (hmass : ∀ x, vectorMass f x ≤ C) :
    K.vectorEnergy f ≤ ρ * C := by
…

    Mentions: OAI.MaxCutGames.Repetition.ProjectionKernel, OAI.MaxCutGames.Repetition.ProjectionKernel.vectorMass

  42. def OAI.MaxCutGames.Repetition.ProjectionKernel.reindex line 615

    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.MaxCutGames.Repetition.ProjectionKernel

  43. theorem OAI.MaxCutGames.Repetition.ProjectionKernel.apply_reindex line 626

    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.MaxCutGames.Repetition.ProjectionKernel, OAI.MaxCutGames.Repetition.ProjectionKernel.apply

  44. theorem OAI.MaxCutGames.Repetition.ProjectionKernel.energy_reindex line 645
  45. theorem OAI.MaxCutGames.Repetition.ProjectionKernel.assignmentEnergy_reindex line 660
  46. theorem OAI.MaxCutGames.Repetition.ProjectionKernel.collisionValue_reindex line 683

    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.MaxCutGames.Repetition.ProjectionKernel, OAI.MaxCutGames.Repetition.ProjectionKernel.collisionValue