SelectedCommonMarginalLemmas.lean`

54 declarations, 0 contain sorry, 0 declared as axioms

The common-data law has exactly the actual selected-event question marginal. Removing the fair endpoint reveal and regrouping the outside data preserve the embedded question pair.

theorem OAI.UniqueGamesTheorem.Foundations.Repetition.pushforward_snd_weight_eq_secondMarginal line 23
def OAI.UniqueGamesTheorem.Foundations.Repetition.revealDataSplitEquiv line 33
theorem OAI.UniqueGamesTheorem.Foundations.Repetition.partialRevealMarginal_secondMarginal line 50
def OAI.UniqueGamesTheorem.Foundations.Repetition.selectedObservationDataEquiv line 70
theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selectedFullReveal_secondMarginal line 79
theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selectedRawMarginal_secondMarginal line 93

theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selectedCommonLaw_secondMarginal line 117

Source documentation

The exact marginal identification needed to use the conditioned-question information bound in the two local common-data profile errors.

theorem selectedCommonLaw_secondMarginal (G : Game Q₁ Q₂ A₁ A₂)
    (strategy : Strategy (Fin n → Q₁) (Fin n → Q₂) (Fin n → A₁) (Fin n → A₂))
    (selected : Finset (Fin n)) (positive : 0 < G.selectedSuccess strategy selected)
    (j : {i : Fin n // i ∉ selected}) :
    secondMarginal (selectedCommonLaw G strategy selected positive j).weight =
      (selectedQuestionMarginal G strategy selected positive j.1).weight := by
…

Mentions: OAI.UniqueGamesTheorem.Foundations.Repetition.selectedCommonLaw, OAI.UniqueGamesTheorem.Foundations.Repetition.selectedQuestionMarginal

theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selectedCommonLaw_questions_pushforward line 128
def OAI.UniqueGamesTheorem.Foundations.Repetition.completionTupleEquiv line 167
def OAI.UniqueGamesTheorem.Foundations.Repetition.updatedTableFallback line 173
theorem OAI.UniqueGamesTheorem.Foundations.Repetition.updatedTableFallback_zero line 178
theorem OAI.UniqueGamesTheorem.Foundations.Repetition.normalizeOr_weight_eq_zero_of_zero line 190
def OAI.UniqueGamesTheorem.Foundations.Repetition.selectedLeftRaw line 207
def OAI.UniqueGamesTheorem.Foundations.Repetition.selectedRightRaw line 215
theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selectedLeftRaw_nonnegative line 224
theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selectedRightRaw_nonnegative line 237
def OAI.UniqueGamesTheorem.Foundations.Repetition.selectedLeftCompletion line 249
def OAI.UniqueGamesTheorem.Foundations.Repetition.selectedRightCompletion line 258
theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selectedLeftCompletion_zero line 268
theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selectedRightCompletion_zero line 279
theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selectedLeftCompletion_support line 290
theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selectedRightCompletion_support line 300
def OAI.UniqueGamesTheorem.Foundations.Repetition.selectedCompletionScale line 309

theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selected_completion_factorization line 319

Source documentation

Pointwise factorization of the actual selected common-data row.

theorem selected_completion_factorization (G : Game Q₁ Q₂ A₁ A₂)
    (strategy : Strategy (Fin n → Q₁) (Fin n → Q₂) (Fin n → A₁) (Fin n → A₂))
    (selected : Finset (Fin n)) (j : {i : Fin n // i ∉ selected})
    (s : SelectedCommonData (Q₁ := Q₁) (Q₂ := Q₂) (A₁ := A₁) (A₂ := A₂) selected j)
…

Mentions: OAI.UniqueGamesTheorem.Foundations.Repetition.SelectedCommonData

theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selectedCommonLaw_completion_row_mass line 344

theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selected_completion_row_recombine line 368

Source documentation

Actual common-row mass times the two local completion probabilities is the selected partial-reveal weight with its actual coordinate indicator.

theorem selected_completion_row_recombine (G : Game Q₁ Q₂ A₁ A₂)
    (strategy : Strategy (Fin n → Q₁) (Fin n → Q₂) (Fin n → A₁) (Fin n → A₂))
    (selected : Finset (Fin n)) (positive : 0 < G.selectedSuccess strategy selected)
    (j : {i : Fin n // i ∉ selected})
    (s : SelectedCommonData (Q₁ := Q₁) (Q₂ := Q₂) (A₁ := A₁) (A₂ := A₂) selected j)
…

Mentions: OAI.UniqueGamesTheorem.Foundations.Repetition.SelectedCommonData

theorem OAI.UniqueGamesTheorem.Foundations.Repetition.partialRevealWeight_forget line 414
theorem OAI.UniqueGamesTheorem.Foundations.Repetition.partialReveal_event_forget line 426
theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selectedOutsideLikelihood_event_sum line 443
theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selected_partial_event_total line 506
def OAI.UniqueGamesTheorem.Foundations.Repetition.selectedFullLeftCompletion line 527
def OAI.UniqueGamesTheorem.Foundations.Repetition.selectedFullRightCompletion line 535
theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selectedFullLeftCompletion_support line 544
theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selectedFullRightCompletion_support line 566
theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selected_full_completion_probability line 587
theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selected_completion_event_row line 613
def OAI.UniqueGamesTheorem.Foundations.Repetition.selectedFullCompletionMixture line 657
theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selectedFullCompletionMixture_probability line 666

theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selectedFullCompletionMixture_eq_conditionedQuestions line 690

Source documentation

Exact equality with the actual repeated-game question law conditioned on the selected wins, derived by summing the local completion rows.

theorem selectedFullCompletionMixture_eq_conditionedQuestions (G : Game Q₁ Q₂ A₁ A₂)
    (strategy : Strategy (Fin n → Q₁) (Fin n → Q₂) (Fin n → A₁) (Fin n → A₂))
    (selected : Finset (Fin n)) (positive : 0 < G.selectedSuccess strategy selected)
    (j : {i : Fin n // i ∉ selected}) :
    selectedFullCompletionMixture G strategy selected positive j =
      (G.repetition n).questions.condition (G.selectedWins strategy selected) positive := by
…

Mentions: OAI.UniqueGamesTheorem.Foundations.Repetition.selectedFullCompletionMixture

def OAI.UniqueGamesTheorem.Foundations.Repetition.TraceSeed line 720
instance OAI.UniqueGamesTheorem.Foundations.Repetition.traceSeedFintype line 724
instance OAI.UniqueGamesTheorem.Foundations.Repetition.traceSeedUniqueZero line 729
def OAI.UniqueGamesTheorem.Foundations.Repetition.traceList line 732
def OAI.UniqueGamesTheorem.Foundations.Repetition.traceSeedLaw line 736
theorem OAI.UniqueGamesTheorem.Foundations.Repetition.traceSeedLaw_expectation line 742

def OAI.UniqueGamesTheorem.Foundations.Repetition.sharedOutputLaw line 761

Source documentation

The law of the two local outputs, driven by a seed chosen independently of the question pair. Local maps receive only their own question.

def sharedOutputLaw {X Y S Seed : Type*}
    [Fintype X] [Fintype Y] [Fintype S] [Fintype Seed] [DecidableEq S]
    (μ : FiniteDistribution (X × Y)) (seedLaw : FiniteDistribution Seed)
    (left : Seed → X → S) (right : Seed → Y → S) :
    FiniteDistribution ((X × Y) × S × S) :=
…

theorem OAI.UniqueGamesTheorem.Foundations.Repetition.sharedOutputLaw_weight line 769
def OAI.UniqueGamesTheorem.Foundations.Repetition.samplerLocal line 789
def OAI.UniqueGamesTheorem.Foundations.Repetition.samplerOutputLaw line 795
theorem OAI.UniqueGamesTheorem.Foundations.Repetition.probability_weight_le_one line 802

theorem OAI.UniqueGamesTheorem.Foundations.Repetition.samplerOutputLaw_diagonal line 810

Source documentation

The per-label estimate concerns the actual finite game-law sampler with a shared seed independent of the input questions.

theorem samplerOutputLaw_diagonal (thresholds : List ℝ)
    (μ : FiniteDistribution (X × Y))
    (L : X → FiniteDistribution S) (R : Y → FiniteDistribution S)
    (hL : ∀ x s, (L x).weight s ∈ thresholds)
    (hR : ∀ y s, (R y).weight s ∈ thresholds)
    (fallback : S) (n : Nat) (x : X) (y : Y) (a : S) :
    μ.weight (x,y) * min ((L x).weight a) ((R y).weight a) /
        (1 + Information.totalVariation (L x).weight (R y).weight) *
        (1 - eventMass (rectangleWeight thresholds)
          (fun s => !(rectangleAccept thresholds (L x).weight s ||
            rectangleAccept thresholds (R y).weight s)) ^ n) ≤
      (samplerOutputLaw thresholds μ L R fallback n).weight ((x,y),a,a) := by
…

Mentions: OAI.UniqueGamesTheorem.Foundations.Information.totalVariation, OAI.UniqueGamesTheorem.Foundations.Repetition.samplerOutputLaw

theorem OAI.UniqueGamesTheorem.Foundations.Repetition.samplerOutputLaw_uniform_diagonal line 841

theorem OAI.UniqueGamesTheorem.Foundations.Repetition.samplerOutputLaw_totalVariation line 864

Source documentation

Actual finite shared sampler approximates any prescribed diagonal law. Its error is derived from the two actual conditional profiles and its uniform finite exhaustion probability.

theorem samplerOutputLaw_totalVariation
    (p : FiniteDistribution ((X × Y) × S)) (μ : FiniteDistribution (X × Y))
    (L : X → FiniteDistribution S) (R : Y → FiniteDistribution S)
    (fallback : S) (n : Nat) :
    Information.totalVariation
      (samplerOutputLaw (sharedProfileThresholds L R) μ L R fallback n).weight
      (diagonalWeights p.weight) ≤
      2 * Information.totalVariation p.weight (fun z => μ.weight z.1 * (L z.1.1).weight z.2) +
      2 * Information.totalVariation p.weight (fun z => μ.weight z.1 * (R z.1.2).weight z.2) +
      uniformRejectionRate S ^ n := by
…

Mentions: OAI.UniqueGamesTheorem.Foundations.Information.totalVariation, OAI.UniqueGamesTheorem.Foundations.Repetition.samplerOutputLaw, OAI.UniqueGamesTheorem.Foundations.Repetition.diagonalWeights

theorem OAI.UniqueGamesTheorem.Foundations.Repetition.samplerOutputLaw_arbitrarily_close line 886