OAI/Computability/UniqueGames/Games/Overlap.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Direct diagonal-overlap comparison for the finite correlated sampler. All quantities are finite weight arrays; no reference sampler or embedding claim is assumed. The final theorem consumes the per-label lower bound that is proved for the actual finite threshold sampler in CorrelatedSampling.

  1. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.min_half_formula line 20
  2. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.sum_min_one_sub_tv line 28
  3. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.discount_le_self line 37
  4. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.discount_loss_le_mul line 42
  5. def OAI.UniqueGamesTheorem.Foundations.Repetition.discountedCommonMass line 52
  6. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.discounted_common_mass_bounds line 57

    Source documentation

    The direct common-mass argument, with its exact finite-array premises.

    theorem discounted_common_mass_bounds {X S : Type*} [Fintype X] [Fintype S]
    (p a b : X × S → ℝ) (μ t : X → ℝ)
    (hp : IsProbability p) (ha : IsProbability a) (hb : IsProbability b)
    (ht : ∀ x, 0 ≤ t x)
    (hrow : ∀ x, (∑ s, a (x, s)) = μ x)
    (htv : (∑ x, μ x * t x) = totalVariation a b) :
    1 - 2 * totalVariation p a - 2 * totalVariation p b ≤ discountedCommonMass p a b t ∧
      discountedCommonMass p a b t ≤ 1 := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Repetition.discountedCommonMass

  7. def OAI.UniqueGamesTheorem.Foundations.Repetition.diagonalWeights line 117
  8. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.diagonalWeights_isProbability line 122
  9. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.diagonal_overlap_identity line 133
  10. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.diagonal_sampler_totalVariation_le line 160

    Source documentation

    The per-label diagonal guarantee implies direct TV control even when the target's question marginal differs from the simulator's question marginal.

    theorem diagonal_sampler_totalVariation_le {X S : Type*} [Fintype X] [Fintype S]
    (p : X × S → ℝ) (μ : X → ℝ) (L R : X → S → ℝ)
    (sim : X × S × S → ℝ) (hp : IsProbability p) (hμ : IsProbability μ)
    (hL : ∀ x, IsProbability (L x)) (hR : ∀ x, IsProbability (R x))
    (hsim : IsProbability sim) {τ : ℝ} (hτ0 : 0 ≤ τ) (hτ1 : τ ≤ 1)
    (hdiag : ∀ x s, μ x * min (L x s) (R x s) /
      (1 + totalVariation (L x) (R x)) * (1 - τ) ≤ sim (x, s, s)) :
    totalVariation sim (diagonalWeights p) ≤
      2 * totalVariation p (fun z => μ z.1 * L z.1 z.2) +
      2 * totalVariation p (fun z => μ z.1 * R z.1 z.2) + τ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Repetition.diagonalWeights