KernelIteration.lean`

39 declarations, 0 contain sorry, 0 declared as axioms

Independent repetitions of the actual conditional projection kernel. The resulting game has precisely the original game's product question law. A successor tuple is a reindexed independent product, so collision bounds on the product apply to unrestricted strategies on whole tuples.

def OAI.MaxCutGames.Repetition.ProjectionKernel.repetition line 24
theorem OAI.MaxCutGames.Repetition.ProjectionKernel.repetition_accepts_iff line 37
theorem OAI.MaxCutGames.Repetition.ProjectionKernel.toGame_repetition line 44
theorem OAI.MaxCutGames.Repetition.ProjectionKernel.eq_of_data_eq line 62

theorem OAI.MaxCutGames.Repetition.ProjectionKernel.repetition_succ line 74

Source documentation

Separate the first coordinate without restricting answer dependence on any coordinate of the complete local question tuple.

theorem repetition_succ (K : ProjectionKernel Q₁ Q₂ A₁ A₂) (n : Nat) :
    K.repetition (n + 1) =
      (K.product (K.repetition n)).reindex
        (Fin.consEquiv (fun _ : Fin (n + 1) => Q₁))
        (Fin.consEquiv (fun _ : Fin (n + 1) => Q₂))
        (Fin.consEquiv (fun _ : Fin (n + 1) => A₁))
        (Fin.consEquiv (fun _ : Fin (n + 1) => A₂)) := by
…

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

theorem OAI.MaxCutGames.Repetition.ProjectionKernel.collisionValue_repetition_succ line 107
theorem OAI.MaxCutGames.Repetition.ProjectionKernel.collisionValue_repetition_zero_le_one line 113

def OAI.MaxCutGames.Foundations.Repetition.revealedProductWeight line 140

Source documentation

mask i = false reveals the first question, and true the second.

def revealedProductWeight (weight : ι → α → β → ℝ) (mask : ι → Bool)
    (fixedLeft : ι → α) (fixedRight : ι → β) (x : ι → α) (y : ι → β) : ℝ :=
…

def OAI.MaxCutGames.Foundations.Repetition.revealedLeftWeight line 146
def OAI.MaxCutGames.Foundations.Repetition.revealedRightWeight line 151
theorem OAI.MaxCutGames.Foundations.Repetition.revealedProductWeight_factorizes line 159
Source documentation
Exact factorization after fixing the selected endpoint at every position. No assumption on coordinate alphabets or probabilities is needed for this identity, so it applies separately at every fixed outside question tuple.
```
theorem revealedProductWeight_factorizes (weight : ι → α → β → ℝ) (mask : ι → Bool)
    (fixedLeft : ι → α) (fixedRight : ι → β) (x : ι → α) (y : ι → β) :
    revealedProductWeight weight mask fixedLeft fixedRight x y =
      revealedLeftWeight weight mask fixedLeft fixedRight x *
        revealedRightWeight weight mask fixedLeft fixedRight y := by
…
```
Mentions: OAI.MaxCutGames.Foundations.Repetition.revealedProductWeight, OAI.MaxCutGames.Foundations.Repetition.revealedLeftWeight, OAI.MaxCutGames.Foundations.Repetition.revealedRightWeight

theorem OAI.MaxCutGames.Foundations.Repetition.revealedProductWeight_local_restrictions line 174

Source documentation

Local answer tests are separate functions of the complete local question vectors. Multiplying by both tests leaves a product of two local weights.

theorem revealedProductWeight_local_restrictions
    (weight : ι → α → β → ℝ) (mask : ι → Bool)
    (fixedLeft : ι → α) (fixedRight : ι → β)
    (leftTest : (ι → α) → ℝ) (rightTest : (ι → β) → ℝ)
    (x : ι → α) (y : ι → β) :
    revealedProductWeight weight mask fixedLeft fixedRight x y * leftTest x * rightTest y =
      (revealedLeftWeight weight mask fixedLeft fixedRight x * leftTest x) *
      (revealedRightWeight weight mask fixedLeft fixedRight y * rightTest y) := by
…

Mentions: OAI.MaxCutGames.Foundations.Repetition.revealedProductWeight, OAI.MaxCutGames.Foundations.Repetition.revealedLeftWeight, OAI.MaxCutGames.Foundations.Repetition.revealedRightWeight

theorem OAI.MaxCutGames.Foundations.Repetition.productWeight_mass line 187
def OAI.MaxCutGames.Foundations.Repetition.normalizedWeight line 193
theorem OAI.MaxCutGames.Foundations.Repetition.normalizedWeight_isProbability line 196
theorem OAI.MaxCutGames.Foundations.Repetition.normalized_productWeight line 206
Source documentation
Normalizing an actual product weight gives the product of its separately normalized marginals. This is the finite conditional-independence identity.
```
theorem normalized_productWeight (left : X → ℝ) (right : Y → ℝ)
    (hleft : 0 < ∑ x, left x) (hright : 0 < ∑ y, right y) (xy : X × Y) :
    normalizedWeight (fun z : X × Y => left z.1 * right z.2) xy =
      normalizedWeight left xy.1 * normalizedWeight right xy.2 := by
…
```
Mentions: OAI.MaxCutGames.Foundations.Repetition.normalizedWeight

theorem OAI.MaxCutGames.Foundations.Repetition.normalized_rectangle_restriction line 216

Source documentation

Conditioning a product law on separate local events keeps the two factors independent, with each conditioned on its own event.

theorem normalized_rectangle_restriction
    (left : X → ℝ) (right : Y → ℝ) (leftTest : X → ℝ) (rightTest : Y → ℝ)
    (hleft : 0 < ∑ x, left x * leftTest x)
    (hright : 0 < ∑ y, right y * rightTest y) (xy : X × Y) :
    normalizedWeight
      (fun z : X × Y => left z.1 * right z.2 * leftTest z.1 * rightTest z.2) xy =
      normalizedWeight (fun x => left x * leftTest x) xy.1 *
      normalizedWeight (fun y => right y * rightTest y) xy.2 := by
…

Mentions: OAI.MaxCutGames.Foundations.Repetition.normalizedWeight

def OAI.MaxCutGames.Foundations.Repetition.normalizeOr line 247
theorem OAI.MaxCutGames.Foundations.Repetition.sum_mul_normalizeOr line 255

theorem OAI.MaxCutGames.Foundations.Repetition.local_completion_recombination line 272

Source documentation

Exact reconstruction from two separately normalized local completion laws, valid even when either unnormalized row has mass zero.

theorem local_completion_recombination
    (left : X → ℝ) (right : Y → ℝ)
    (hl : ∀ x, 0 ≤ left x) (hr : ∀ y, 0 ≤ right y)
    (defaultLeft : FiniteDistribution X) (defaultRight : FiniteDistribution Y)
    (c : ℝ) (x : X) (y : Y) :
    (c * (∑ z, left z) * (∑ z, right z)) *
      ((normalizeOr left hl defaultLeft).weight x *
        (normalizeOr right hr defaultRight).weight y) = c * left x * right y := by
…

Mentions: OAI.MaxCutGames.Foundations.Repetition.normalizeOr

theorem OAI.MaxCutGames.Foundations.Repetition.factorized_completion_row line 287

Source documentation

The row mass appearing in reconstruction is the actual sum of product weights, not an assumed marginal identity.

theorem factorized_completion_row
    (left : X → ℝ) (right : Y → ℝ)
    (hl : ∀ x, 0 ≤ left x) (hr : ∀ y, 0 ≤ right y)
    (defaultLeft : FiniteDistribution X) (defaultRight : FiniteDistribution Y)
    (c : ℝ) (xy : X × Y) :
    (∑ z : X × Y, c * left z.1 * right z.2) *
      ((normalizeOr left hl defaultLeft).product
        (normalizeOr right hr defaultRight)).weight xy = c * left xy.1 * right xy.2 := by
…

Mentions: OAI.MaxCutGames.Foundations.Repetition.normalizeOr

def OAI.MaxCutGames.Repetition.leftQuestionMarginal line 323
def OAI.MaxCutGames.Repetition.rightQuestionMarginal line 330
def OAI.MaxCutGames.Repetition.leftGivenRight line 339
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.MaxCutGames.Repetition.rightQuestionMarginal_mul_leftGivenRight line 346
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.MaxCutGames.Repetition.rightQuestionMarginal, OAI.MaxCutGames.Repetition.leftGivenRight
def OAI.MaxCutGames.Repetition.kernelOfGame line 356
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.MaxCutGames.Repetition.IsProjection, OAI.MaxCutGames.Repetition.ProjectionKernel
theorem OAI.MaxCutGames.Repetition.kernelOfGame_question_weight line 363
theorem OAI.MaxCutGames.Repetition.toGame_kernelOfGame line 368
theorem OAI.MaxCutGames.Repetition.kernelOfGame_success line 380
theorem OAI.MaxCutGames.Repetition.kernelOfGame_value line 386
theorem OAI.MaxCutGames.Repetition.sequence_le_power line 396
theorem OAI.MaxCutGames.Repetition.squared_rate_le_dsRate_sq line 408
theorem OAI.MaxCutGames.Repetition.rate_of_squared_collision_recurrence line 414
theorem OAI.MaxCutGames.Repetition.ProjectionKernel.collisionValue_product_le_gap_rate line 459
theorem OAI.MaxCutGames.Repetition.ProjectionKernel.repetition_value_le_dsRate line 473
theorem OAI.MaxCutGames.Repetition.projection_repetition_value line 498
Source documentation
The v2 projection-repetition estimate, including the empty product. The repetition exponent is independent of all question and answer cardinalities.
```
theorem projection_repetition_value
    (G : Game Q₁ Q₂ A₁ A₂) (hG : IsProjection G) (n : ℕ)
    {gap : ℝ} (hgap₀ : 0 < gap) (hgap₁ : gap < 1)
    (hvalue : G.value ≤ 1 - gap) :
    (G.repetition n).value ≤ (1 - gap ^ 2 / 16) ^ n := by
…
```
Mentions: OAI.MaxCutGames.Repetition.IsProjection
theorem OAI.MaxCutGames.Repetition.projection_repetition_success line 507
theorem OAI.MaxCutGames.Repetition.clean_repetition_value line 516
theorem OAI.MaxCutGames.Repetition.final_repetition_value line 526