UpperBound.lean`

24 declarations, 0 contain sorry, 0 declared as axioms

Exact sampling of two conditional kernels from one finite weighted shared seed. The seed consists of independent full response tables and is independent of the questions. Supported-coordinate repairs preserve the sampled laws and enforce the designated coordinate even on seeds of weight zero. The seed is not claimed to be uniform: the kernel weights may be arbitrary real numbers.

def OAI.MaxCutGames.Clean.UpperBound.fixedAdviceSuccess line 22

Source documentation

The true weighted occurrence/position experiment at fixed visible advice.

def fixedAdviceSuccess (μ : FiniteDistribution (O × Fin 3)) (J : Finset P)
    (g : IncidenceExtraction.Incidence O N)
    (gamma : RawCoefficients J (ZeroInformation.Bits R))
    (strategy : OuterStrategy (P := P) (R := R) (O := O) (N := N)) : ℝ :=
…

theorem OAI.MaxCutGames.Clean.UpperBound.reference_of_positive_inline_UpperBound line 30

theorem OAI.MaxCutGames.Clean.UpperBound.conditioned_success_le_repeated_value_with_reference line 51

Source documentation

On each positive public observation fibre, the full agreement event is bounded by ordinary repetition. The reference draw is fixed public padding, not an extra input depending on the still hidden question pair.

theorem conditioned_success_le_repeated_value_with_reference
    (μ : FiniteDistribution (O × Fin 3)) (J : Finset P)
    (g : IncidenceExtraction.Incidence O N)
    (gamma : RawCoefficients J (ZeroInformation.Bits R))
    (observed : PositionOutside (zeroSet J gamma) → O × N)
    (positive : 0 < (FiniteDistribution.table (fun _ : P => μ)).probability
      (fun draw => decide (outsideRecord (zeroSet J gamma) g.name draw = observed)))
    (reference : RawObservationFibre J g.name gamma observed)
    (e : Fin (zeroSet J gamma).card ≃ PositionInside (zeroSet J gamma))
    (strategy : OuterStrategy (P := P) (R := R) (O := O) (N := N))
…

theorem OAI.MaxCutGames.Clean.UpperBound.conditioned_success_le_repeated_value line 109
theorem OAI.MaxCutGames.Clean.UpperBound.fixed_advice_success_le_repeated_value line 133
Source documentation
All outside observations are genuinely averaged with their actual weights. The result permits arbitrary repeated occurrence IDs and correlated local answers across the entire clean tuple.
```
theorem fixed_advice_success_le_repeated_value
    (μ : FiniteDistribution (O × Fin 3)) (J : Finset P)
    (g : IncidenceExtraction.Incidence O N)
    (gamma : RawCoefficients J (ZeroInformation.Bits R))
    (strategy : OuterStrategy (P := P) (R := R) (O := O) (N := N))
…
```
theorem OAI.MaxCutGames.Foundations.Games.FiniteDistribution.pushforward_eq_of_agree_on_support line 166
theorem OAI.MaxCutGames.Foundations.Games.FiniteDistribution.product_pushforward line 182
Source documentation
Applying separate maps to independent samples preserves their independence.
```
theorem product_pushforward
    {Ω Γ A B : Type*} [Fintype Ω] [Fintype Γ] [Fintype A] [Fintype B]
    (μ : FiniteDistribution Ω) (ν : FiniteDistribution Γ)
    (f : Ω → A) (g : Γ → B) :
    (μ.product ν).pushforward (fun z => (f z.1, g z.2)) =
      (μ.pushforward f).product (ν.pushforward g) := by
…
```
Mentions: OAI.MaxCutGames.Foundations.Games.FiniteDistribution, OAI.MaxCutGames.Foundations.Games.FiniteDistribution.pushforward, OAI.MaxCutGames.Foundations.Games.FiniteDistribution.product
theorem OAI.MaxCutGames.Foundations.Games.FiniteDistribution.table_row_weight_ne_zero line 200
Source documentation
A full response table of nonzero weight uses a supported answer in every row.
```
theorem table_row_weight_ne_zero
    {Q A : Type*} [Fintype Q] [Fintype A] [DecidableEq Q]
    (responses : Q → FiniteDistribution A) (answers : Q → A)
    (h : (table responses).weight answers ≠ 0) (q : Q) :
    (responses q).weight (answers q) ≠ 0 := by
…
```
Mentions: OAI.MaxCutGames.Foundations.Games.FiniteDistribution, OAI.MaxCutGames.Foundations.Games.FiniteDistribution.table
theorem OAI.MaxCutGames.Foundations.Games.FiniteDistribution.table_repair_pushforward line 211
Source documentation
Repairing table entries only off each row's support leaves its exact law intact.
```
theorem table_repair_pushforward
    {Q A : Type*} [Fintype Q] [Fintype A] [DecidableEq Q]
    (responses : Q → FiniteDistribution A) (repair : Q → A → A)
    (hrepair : ∀ q a, (responses q).weight a ≠ 0 → repair q a = a) (q : Q) :
    (table responses).pushforward (fun answers => repair q (answers q)) =
      responses q := by
…
```
Mentions: OAI.MaxCutGames.Foundations.Games.FiniteDistribution, OAI.MaxCutGames.Foundations.Games.FiniteDistribution.table, OAI.MaxCutGames.Foundations.Games.FiniteDistribution.pushforward
abbrev OAI.MaxCutGames.Foundations.Games.KernelSampling.Seed line 229
Source documentation
A single seed supplies a full local table to each side.
```
abbrev Seed (Q₁ Q₂ A B : Type*) := (Q₁ → A) × (Q₂ → B)
```
def OAI.MaxCutGames.Foundations.Games.KernelSampling.readLeft line 231
def OAI.MaxCutGames.Foundations.Games.KernelSampling.readRight line 232
def OAI.MaxCutGames.Foundations.Games.KernelSampling.seedLaw line 235
Source documentation
The fixed weighted seed law; it does not depend on the sampled questions.
```
def seedLaw {Q₁ Q₂ A B : Type*}
    [Fintype Q₁] [Fintype Q₂] [Fintype A] [Fintype B]
    [DecidableEq Q₁] [DecidableEq Q₂]
    (left : Q₁ → FiniteDistribution A) (right : Q₂ → FiniteDistribution B) :
    FiniteDistribution (Seed Q₁ Q₂ A B) :=
…
```
Mentions: OAI.MaxCutGames.Foundations.Games.FiniteDistribution, OAI.MaxCutGames.Foundations.Games.KernelSampling.Seed
theorem OAI.MaxCutGames.Foundations.Games.KernelSampling.read_joint_pushforward line 243
Source documentation
The two reads have exactly the product of the requested conditional laws.
```
theorem read_joint_pushforward {Q₁ Q₂ A B : Type*}
    [Fintype Q₁] [Fintype Q₂] [Fintype A] [Fintype B]
    [DecidableEq Q₁] [DecidableEq Q₂]
    (left : Q₁ → FiniteDistribution A) (right : Q₂ → FiniteDistribution B)
    (x : Q₁) (y : Q₂) :
    (seedLaw left right).pushforward (fun seed => (readLeft seed x, readRight seed y)) =
      (left x).product (right y) := by
…
```
Mentions: OAI.MaxCutGames.Foundations.Games.FiniteDistribution, OAI.MaxCutGames.Foundations.Games.KernelSampling.seedLaw, OAI.MaxCutGames.Foundations.Games.KernelSampling.readLeft, OAI.MaxCutGames.Foundations.Games.KernelSampling.readRight

theorem OAI.MaxCutGames.Foundations.Games.KernelSampling.repaired_joint_pushforward line 257

Source documentation

Separate supported repairs retain the exact joint product law.

theorem repaired_joint_pushforward {Q₁ Q₂ A B : Type*}
    [Fintype Q₁] [Fintype Q₂] [Fintype A] [Fintype B]
    [DecidableEq Q₁] [DecidableEq Q₂]
    (left : Q₁ → FiniteDistribution A) (right : Q₂ → FiniteDistribution B)
    (repairLeft : Q₁ → A → A) (repairRight : Q₂ → B → B)
    (hleft : ∀ x a, (left x).weight a ≠ 0 → repairLeft x a = a)
    (hright : ∀ y b, (right y).weight b ≠ 0 → repairRight y b = b)
    (x : Q₁) (y : Q₂) :
    (seedLaw left right).pushforward (fun seed =>
      (repairLeft x (readLeft seed x), repairRight y (readRight seed y))) =
      (left x).product (right y) := by
…

Mentions: OAI.MaxCutGames.Foundations.Games.FiniteDistribution, OAI.MaxCutGames.Foundations.Games.KernelSampling.seedLaw, OAI.MaxCutGames.Foundations.Games.KernelSampling.readLeft, OAI.MaxCutGames.Foundations.Games.KernelSampling.readRight

def OAI.MaxCutGames.Foundations.Games.KernelSampling.completedLeft line 278
Source documentation
Restore the designated coordinate on every left table read.
```
def completedLeft (j : I)
    (seed : Seed (A × S) (B × S) (I → A) (I → B)) (q : A × S) : I → A :=
…
```
Mentions: OAI.MaxCutGames.Foundations.Games.KernelSampling.Seed
def OAI.MaxCutGames.Foundations.Games.KernelSampling.completedRight line 283
Source documentation
Restore the designated coordinate on every right table read.
```
def completedRight (j : I)
    (seed : Seed (A × S) (B × S) (I → A) (I → B)) (q : B × S) : I → B :=
…
```
Mentions: OAI.MaxCutGames.Foundations.Games.KernelSampling.Seed
theorem OAI.MaxCutGames.Foundations.Games.KernelSampling.completedLeft_coordinate line 287
theorem OAI.MaxCutGames.Foundations.Games.KernelSampling.completedRight_coordinate line 291
theorem OAI.MaxCutGames.Foundations.Games.KernelSampling.update_eq_of_coordinate_inline_KernelSampling line 295
theorem OAI.MaxCutGames.Foundations.Games.KernelSampling.completed_joint_pushforward line 303
Source documentation
Exact conditional completion from a finite weighted shared seed. The reads always restore the specified coordinates, including on seeds of weight zero; the support hypotheses ensure that this repair preserves the requested laws.
```
theorem completed_joint_pushforward
    [Fintype I] [Fintype A] [Fintype B] [Fintype S]
    [DecidableEq A] [DecidableEq B] [DecidableEq S]
    (left : (A × S) → FiniteDistribution (I → A))
    (right : (B × S) → FiniteDistribution (I → B)) (j : I)
    (hleft : ∀ q xs, (left q).weight xs ≠ 0 → xs j = q.1)
    (hright : ∀ q ys, (right q).weight ys ≠ 0 → ys j = q.1)
    (x : A × S) (y : B × S) :
    (seedLaw left right).pushforward
        (fun seed => (completedLeft j seed x, completedRight j seed y)) =
      (left x).product (right y) := by
…
```
Mentions: OAI.MaxCutGames.Foundations.Games.FiniteDistribution, OAI.MaxCutGames.Foundations.Games.KernelSampling.seedLaw, OAI.MaxCutGames.Foundations.Games.KernelSampling.completedLeft, OAI.MaxCutGames.Foundations.Games.KernelSampling.completedRight
def OAI.MaxCutGames.Foundations.Games.FiniteDistribution.mixture line 334
theorem OAI.MaxCutGames.Foundations.Games.FiniteDistribution.probability_mixture line 344
theorem OAI.MaxCutGames.Foundations.Games.FiniteDistribution.probability_mixture_le line 361