OAI/Computability/MaxCut/PCP/Overlap.lean

GitHub source file

50 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.MaxCutGames.Foundations.Repetition.min_half_formula_inline_Overlap line 24
  2. theorem OAI.MaxCutGames.Foundations.Repetition.sum_min_one_sub_tv line 32
  3. theorem OAI.MaxCutGames.Foundations.Repetition.discount_le_self_inline_Overlap line 41
  4. theorem OAI.MaxCutGames.Foundations.Repetition.discount_loss_le_mul_inline_Overlap line 46
  5. def OAI.MaxCutGames.Foundations.Repetition.discountedCommonMass line 56
  6. theorem OAI.MaxCutGames.Foundations.Repetition.discounted_common_mass_bounds line 61

    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.MaxCutGames.Foundations.Repetition.discountedCommonMass

  7. def OAI.MaxCutGames.Foundations.Repetition.diagonalWeights line 121
  8. theorem OAI.MaxCutGames.Foundations.Repetition.diagonalWeights_isProbability line 126
  9. theorem OAI.MaxCutGames.Foundations.Repetition.diagonal_overlap_identity line 137
  10. theorem OAI.MaxCutGames.Foundations.Repetition.diagonal_sampler_totalVariation_le line 164

    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.MaxCutGames.Foundations.Repetition.diagonalWeights

  11. def OAI.MaxCutGames.Foundations.Repetition.TraceSeed line 232
  12. instance OAI.MaxCutGames.Foundations.Repetition.traceSeedFintype line 236
  13. instance OAI.MaxCutGames.Foundations.Repetition.traceSeedUniqueZero line 241
  14. def OAI.MaxCutGames.Foundations.Repetition.traceList line 244
  15. def OAI.MaxCutGames.Foundations.Repetition.traceSeedLaw line 248
  16. theorem OAI.MaxCutGames.Foundations.Repetition.traceSeedLaw_expectation line 254
  17. def OAI.MaxCutGames.Foundations.Repetition.sharedOutputLaw line 273

    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) :=
…
  18. theorem OAI.MaxCutGames.Foundations.Repetition.sharedOutputLaw_weight line 281
  19. def OAI.MaxCutGames.Foundations.Repetition.samplerLocal line 299
  20. def OAI.MaxCutGames.Foundations.Repetition.samplerOutputLaw line 305
  21. theorem OAI.MaxCutGames.Foundations.Repetition.probability_weight_le_one line 312
  22. theorem OAI.MaxCutGames.Foundations.Repetition.samplerOutputLaw_diagonal line 320

    Source documentation

    The published per-label estimate now 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.MaxCutGames.Foundations.Information.totalVariation, OAI.MaxCutGames.Foundations.Repetition.samplerOutputLaw

  23. theorem OAI.MaxCutGames.Foundations.Repetition.samplerOutputLaw_uniform_diagonal line 351
  24. theorem OAI.MaxCutGames.Foundations.Repetition.samplerOutputLaw_totalVariation line 374

    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.MaxCutGames.Foundations.Information.totalVariation, OAI.MaxCutGames.Foundations.Repetition.samplerOutputLaw, OAI.MaxCutGames.Foundations.Repetition.diagonalWeights

  25. theorem OAI.MaxCutGames.Foundations.Repetition.samplerOutputLaw_arbitrarily_close line 396
  26. def OAI.MaxCutGames.Repetition.partialPairMass line 431
  27. def OAI.MaxCutGames.Repetition.partialEdgeMass line 435
  28. def OAI.MaxCutGames.Repetition.partialLabelScore line 440
  29. def OAI.MaxCutGames.Repetition.partialSample line 444
  30. theorem OAI.MaxCutGames.Repetition.expectation_mono_inline_RoundingSampling' line 448
  31. theorem OAI.MaxCutGames.Repetition.expectation_const_inline_RoundingSampling' line 455
  32. theorem OAI.MaxCutGames.Repetition.first_good_relation_le_inline_RoundingSampling line 460
  33. theorem OAI.MaxCutGames.Repetition.partial_mass_bounds_inline_RoundingSampling line 483
  34. theorem OAI.MaxCutGames.Repetition.partial_ratio_bound_inline_RoundingSampling line 512
  35. theorem OAI.MaxCutGames.Repetition.partialSample_pair_lower line 536

    Source documentation

    Pointwise success bound for the actual shared finite first-accept sampler. The relation may depend on the ordered pair and need not be symmetric.

    theorem partialSample_pair_lower (μ : FiniteDistribution S)
    (accept : V → S → Bool) (label : V → S → A)
    (R : V → V → A → A → Bool) (fallback : A) (density : ℝ)
    (hdensity₀ : 0 < density) (hdensity : ∀ v, μ.probability (accept v) = density)
    (x y : V) (n : Nat) :
    2 * (partialPairMass μ accept label R x y / density) - 1 - (1 - density) ^ n ≤
      traceAverage μ.weight n (fun proposals =>
        if R x y (partialSample accept label fallback proposals x)
          (partialSample accept label fallback proposals y) then 1 else 0) := by
…

    Mentions: OAI.MaxCutGames.Repetition.partialPairMass, OAI.MaxCutGames.Repetition.partialSample

  36. theorem OAI.MaxCutGames.Repetition.expectation_partial_lower_inline_RoundingSampling line 575
  37. theorem OAI.MaxCutGames.Repetition.exists_labeling_ge_partial line 592

    Source documentation

    Finite partial-assignment correlated rounding. Every vertex has acceptance probability density. The normalized accepted good-pair mass T gives an actual deterministic labeling with success at least 2*T - 1.

    theorem exists_labeling_ge_partial {E : Type*} [Fintype E] [Nonempty V] [Nonempty A]
    (μ : FiniteDistribution S) (ν : FiniteDistribution E)
    (accept : V → S → Bool) (label : V → S → A)
    (left right : E → V) (R : E → A → A → Bool) (density : ℝ) (hdensity₀ : 0 < density)
    (hdensity : ∀ v, μ.probability (accept v) = density) :
    ∃ f : V → A,
      2 * (ν.expectation (partialEdgeMass μ accept label left right R) / density) - 1 ≤
        partialLabelScore ν left right R f := by
…

    Mentions: OAI.MaxCutGames.Repetition.partialEdgeMass, OAI.MaxCutGames.Repetition.partialLabelScore

  38. def OAI.MaxCutGames.Repetition.thresholdLevels line 666

    Source documentation

    All squared amplitudes, including repetitions, determine a single shared finite threshold partition.

    def thresholdLevels (f : V → Ω → ℝ) : List ℝ := by
…
  39. theorem OAI.MaxCutGames.Repetition.square_mem_thresholdLevels line 670
  40. abbrev OAI.MaxCutGames.Repetition.ThresholdSeed line 677

    Source documentation

    The seed is a coordinate and a finite threshold interval.

    abbrev ThresholdSeed (f : V → Ω → ℝ) := RectangleSeed (thresholdLevels f) Ω

    Mentions: OAI.MaxCutGames.Repetition.thresholdLevels

  41. def OAI.MaxCutGames.Repetition.thresholdDistribution line 679
  42. theorem OAI.MaxCutGames.Repetition.thresholdSeed_nonempty line 682
  43. def OAI.MaxCutGames.Repetition.thresholdAccept line 690
  44. def OAI.MaxCutGames.Repetition.thresholdLabel line 694

    Source documentation

    Labels use only the local vertex and the shared coordinate.

    def thresholdLabel (f : V → Ω → ℝ) (a : V → Ω → A) (x : V)
    (seed : ThresholdSeed f) : A := a x seed.1

    Mentions: OAI.MaxCutGames.Repetition.ThresholdSeed

  45. def OAI.MaxCutGames.Repetition.thresholdRate line 697
  46. theorem OAI.MaxCutGames.Repetition.thresholdRate_positive line 699
  47. theorem OAI.MaxCutGames.Repetition.square_le_one_of_row_norm line 704
  48. theorem OAI.MaxCutGames.Repetition.threshold_acceptance_mass line 713

    Source documentation

    Every vertex accepts with the same positive mass, independently of its unit vector. Nonnegativity of the amplitudes is unnecessary for this lemma.

    theorem threshold_acceptance_mass [Nonempty Ω] (f : V → Ω → ℝ)
    (hnorm : ∀ x, ∑ ω, f x ω ^ 2 = 1) (x : V) :
    (thresholdDistribution f).probability (thresholdAccept f x) = thresholdRate Ω := by
…

    Mentions: OAI.MaxCutGames.Repetition.thresholdDistribution, OAI.MaxCutGames.Repetition.thresholdAccept, OAI.MaxCutGames.Repetition.thresholdRate

  49. theorem OAI.MaxCutGames.Repetition.threshold_good_pair_mass line 725

    Source documentation

    Joint acceptance with any relation on the two local labels has exactly the minimum-overlap mass. Both vertices use the same coordinate and threshold.

    theorem threshold_good_pair_mass [Nonempty Ω] (f : V → Ω → ℝ)
    (hnorm : ∀ x, ∑ ω, f x ω ^ 2 = 1) (a : V → Ω → A)
    (x y : V) (R : A → A → Prop) [DecidableRel R] :
    (thresholdDistribution f).probability (fun seed =>
      (thresholdAccept f x seed && thresholdAccept f y seed) &&
        decide (R (thresholdLabel f a x seed) (thresholdLabel f a y seed))) =
      thresholdRate Ω * ∑ ω,
        if R (a x ω) (a y ω) then min (f x ω ^ 2) (f y ω ^ 2) else 0 := by
…

    Mentions: OAI.MaxCutGames.Repetition.thresholdDistribution, OAI.MaxCutGames.Repetition.thresholdAccept, OAI.MaxCutGames.Repetition.thresholdLabel, OAI.MaxCutGames.Repetition.thresholdRate

  50. theorem OAI.MaxCutGames.Repetition.threshold_good_pair_mass_bool line 767

    Source documentation

    Boolean-predicate form used by finite games and the shared sampler.

    theorem threshold_good_pair_mass_bool [Nonempty Ω] (f : V → Ω → ℝ)
    (hnorm : ∀ x, ∑ ω, f x ω ^ 2 = 1) (a : V → Ω → A)
    (x y : V) (R : A → A → Bool) :
    (thresholdDistribution f).probability (fun seed =>
      (thresholdAccept f x seed && thresholdAccept f y seed) &&
        R (thresholdLabel f a x seed) (thresholdLabel f a y seed)) =
      thresholdRate Ω * ∑ ω,
        if R (a x ω) (a y ω) then min (f x ω ^ 2) (f y ω ^ 2) else 0 := by
…

    Mentions: OAI.MaxCutGames.Repetition.thresholdDistribution, OAI.MaxCutGames.Repetition.thresholdAccept, OAI.MaxCutGames.Repetition.thresholdLabel, OAI.MaxCutGames.Repetition.thresholdRate