OAI/Computability/UniqueGames/Soundness/SubsetIntersectionLemmas.lean

GitHub source file

85 declarations, 0 contain sorry, 0 declared as axioms

Exact overlap bound for independently sampled uniform fixed-size subsets

All expectations below are explicit rational sums over Finset.powersetCard. The marginal inclusion probability is derived from the exact binomial count of subsets containing a prescribed singleton. No probabilistic estimate is an assumption. This is the active-set overlap bound used in Lemma 6.3.

  1. def OAI.UniqueGamesTheorem.Soundness.SubsetIntersection.subsets line 38

    Source documentation

    The actual finite sample space of all t-subsets of Fin k.

    def subsets (k t : ℕ) : Finset (Finset (Fin k)) :=
…
  2. def OAI.UniqueGamesTheorem.Soundness.SubsetIntersection.uniformMean line 42

    Source documentation

    Uniform expectation, implemented by its normalized finite sum.

    def uniformMean (k t : ℕ) (f : Finset (Fin k) → ℚ) : ℚ :=
…
  3. def OAI.UniqueGamesTheorem.Soundness.SubsetIntersection.independentMean line 46

    Source documentation

    Independent draws use the product of the two uniform laws.

    def independentMean (k t : ℕ) (f : Finset (Fin k) → Finset (Fin k) → ℚ) : ℚ :=
…
  4. def OAI.UniqueGamesTheorem.Soundness.SubsetIntersection.memberIndicator line 49
  5. def OAI.UniqueGamesTheorem.Soundness.SubsetIntersection.overlapProbability line 52
  6. theorem OAI.UniqueGamesTheorem.Soundness.SubsetIntersection.independentMean_eq_double_sum line 57

    Source documentation

    The nested expectations are exactly the normalized sum on the product sample space, whose cardinality is the square of the single-draw cardinality.

    theorem independentMean_eq_double_sum (k t : ℕ)
    (f : Finset (Fin k) → Finset (Fin k) → ℚ) :
    independentMean k t f =
      (∑ a ∈ subsets k t, ∑ b ∈ subsets k t, f a b) / ((subsets k t).card : ℚ)^2 := by
…

    Mentions: OAI.UniqueGamesTheorem.Soundness.SubsetIntersection.independentMean, OAI.UniqueGamesTheorem.Soundness.SubsetIntersection.subsets

  7. theorem OAI.UniqueGamesTheorem.Soundness.SubsetIntersection.uniformMean_mul_left line 65
  8. theorem OAI.UniqueGamesTheorem.Soundness.SubsetIntersection.uniformMean_mul_right line 71
  9. theorem OAI.UniqueGamesTheorem.Soundness.SubsetIntersection.independentMean_product line 78

    Source documentation

    Independence is proved from the actual two normalized finite sums.

    theorem independentMean_product (k t : ℕ) (f g : Finset (Fin k) → ℚ) :
    independentMean k t (fun a b => f a * g b) = uniformMean k t f * uniformMean k t g := by
…

    Mentions: OAI.UniqueGamesTheorem.Soundness.SubsetIntersection.independentMean, OAI.UniqueGamesTheorem.Soundness.SubsetIntersection.uniformMean

  10. theorem OAI.UniqueGamesTheorem.Soundness.SubsetIntersection.subsets_card line 82
  11. theorem OAI.UniqueGamesTheorem.Soundness.SubsetIntersection.subsets_nonempty line 85
  12. theorem OAI.UniqueGamesTheorem.Soundness.SubsetIntersection.subsets_card_ne_zero line 89
  13. theorem OAI.UniqueGamesTheorem.Soundness.SubsetIntersection.count_containing line 94

    Source documentation

    Count the sampled subsets containing one specified coordinate.

    theorem count_containing {k t : ℕ} (ht : 0 < t) (i : Fin k) :
    ((subsets k t).filter (fun a => i ∈ a)).card =
      (k - 1).choose (t - 1) := by
…

    Mentions: OAI.UniqueGamesTheorem.Soundness.SubsetIntersection.subsets

  14. theorem OAI.UniqueGamesTheorem.Soundness.SubsetIntersection.choose_predecessor_ratio line 101
  15. theorem OAI.UniqueGamesTheorem.Soundness.SubsetIntersection.inclusion_probability line 113

    Source documentation

    Exact marginal probability: a coordinate belongs to a uniform t-subset with probability t / k. This also includes t = 0.

    theorem inclusion_probability {k t : ℕ} (hk : 0 < k) (htk : t ≤ k) (i : Fin k) :
    uniformMean k t (memberIndicator i) = (t : ℚ) / k := by
…

    Mentions: OAI.UniqueGamesTheorem.Soundness.SubsetIntersection.uniformMean, OAI.UniqueGamesTheorem.Soundness.SubsetIntersection.memberIndicator

  16. theorem OAI.UniqueGamesTheorem.Soundness.SubsetIntersection.independent_inclusion_probability line 124

    Source documentation

    A coordinate belongs to both independent draws with the product probability.

    theorem independent_inclusion_probability {k t : ℕ} (hk : 0 < k) (htk : t ≤ k) (i : Fin k) :
    independentMean k t (fun a b => memberIndicator i a * memberIndicator i b) =
      ((t : ℚ) / k)^2 := by
…

    Mentions: OAI.UniqueGamesTheorem.Soundness.SubsetIntersection.independentMean, OAI.UniqueGamesTheorem.Soundness.SubsetIntersection.memberIndicator

  17. theorem OAI.UniqueGamesTheorem.Soundness.SubsetIntersection.uniformMean_congr line 130
  18. theorem OAI.UniqueGamesTheorem.Soundness.SubsetIntersection.uniformMean_const line 135
  19. theorem OAI.UniqueGamesTheorem.Soundness.SubsetIntersection.uniformMean_finset_sum line 141
  20. theorem OAI.UniqueGamesTheorem.Soundness.SubsetIntersection.uniformMean_mono line 149
  21. theorem OAI.UniqueGamesTheorem.Soundness.SubsetIntersection.independentMean_mono line 154
  22. theorem OAI.UniqueGamesTheorem.Soundness.SubsetIntersection.intersection_card_indicator line 162
  23. theorem OAI.UniqueGamesTheorem.Soundness.SubsetIntersection.expected_intersection_fixed line 168

    Source documentation

    Conditional expectation against any fixed first set, directly from the proved marginal inclusion probability of the independent second draw.

    theorem expected_intersection_fixed {k t : ℕ} (hk : 0 < k) (htk : t ≤ k)
    (a : Finset (Fin k)) :
    uniformMean k t (fun b => ((a ∩ b).card : ℚ)) = a.card * ((t : ℚ) / k) := by
…

    Mentions: OAI.UniqueGamesTheorem.Soundness.SubsetIntersection.uniformMean

  24. theorem OAI.UniqueGamesTheorem.Soundness.SubsetIntersection.expected_intersection line 176

    Source documentation

    Exact expected intersection size for independent uniform t-subsets.

    theorem expected_intersection {k t : ℕ} (hk : 0 < k) (htk : t ≤ k) :
    independentMean k t (fun a b => ((a ∩ b).card : ℚ)) = (t : ℚ)^2 / k := by
…

    Mentions: OAI.UniqueGamesTheorem.Soundness.SubsetIntersection.independentMean

  25. theorem OAI.UniqueGamesTheorem.Soundness.SubsetIntersection.nonempty_indicator_le_card line 191

    Source documentation

    The pointwise first-moment bound for a nonempty intersection.

    theorem nonempty_indicator_le_card {k : ℕ} (a b : Finset (Fin k)) :
    (if (a ∩ b).Nonempty then (1 : ℚ) else 0) ≤ (a ∩ b).card := by
…
  26. theorem OAI.UniqueGamesTheorem.Soundness.SubsetIntersection.overlap_probability_le line 198

    Source documentation

    The uniform-subset overlap bound used in the map-law comparison.

    theorem overlap_probability_le {k t : ℕ} (hk : 0 < k) (htk : t ≤ k) :
    overlapProbability k t ≤ (t : ℚ)^2 / k := by
…

    Mentions: OAI.UniqueGamesTheorem.Soundness.SubsetIntersection.overlapProbability

  27. abbrev OAI.UniqueGamesTheorem.Soundness.PartnerSampling.ActiveSet line 217

    Source documentation

    The literal support of the uniform active-set sample.

    abbrev ActiveSet (k t : ℕ) := ↥(subsets k t)
  28. abbrev OAI.UniqueGamesTheorem.Soundness.PartnerSampling.Partner line 220

    Source documentation

    Each retained coordinate receives an independent slot in Fin 3.

    abbrev Partner (k t : ℕ) := Σ a : ActiveSet k t, (↥a.val → Fin 3)

    Mentions: OAI.UniqueGamesTheorem.Soundness.PartnerSampling.ActiveSet

  29. theorem OAI.UniqueGamesTheorem.Soundness.PartnerSampling.activeSet_card line 222
  30. theorem OAI.UniqueGamesTheorem.Soundness.PartnerSampling.slotTuples_card line 225
  31. theorem OAI.UniqueGamesTheorem.Soundness.PartnerSampling.partner_card line 230

    Source documentation

    Equal-size fibers prove that slot sampling does not change subset weights.

    theorem partner_card (k t : ℕ) :
    Fintype.card (Partner k t) = (subsets k t).card * 3 ^ t := by
…

    Mentions: OAI.UniqueGamesTheorem.Soundness.PartnerSampling.Partner

  32. theorem OAI.UniqueGamesTheorem.Soundness.PartnerSampling.partner_nonempty line 236
  33. theorem OAI.UniqueGamesTheorem.Soundness.PartnerSampling.uniformMean_real_cast line 240
  34. theorem OAI.UniqueGamesTheorem.Soundness.PartnerSampling.independentMean_real_cast line 246
  35. theorem OAI.UniqueGamesTheorem.Soundness.PartnerSampling.subset_overlap_probability_le line 253

    Source documentation

    Real Finset.expect form of the already-proved rational subset bound.

    theorem subset_overlap_probability_le {k t : ℕ} (hk : 0 < k) (htk : t ≤ k) :
    (𝔼 a ∈ subsets k t, 𝔼 b ∈ subsets k t,
      if (a ∩ b).Nonempty then (1 : ℝ) else 0) ≤ (t : ℝ)^2 / k := by
…
  36. theorem OAI.UniqueGamesTheorem.Soundness.PartnerSampling.activeSet_expect line 263
  37. theorem OAI.UniqueGamesTheorem.Soundness.PartnerSampling.partner_expect_activeSet line 269

    Source documentation

    The uniform full-partner law projects to the uniform active-subset law.

    theorem partner_expect_activeSet (k t : ℕ) (f : ActiveSet k t → ℝ) :
    (𝔼 p : Partner k t, f p.1) = (𝔼 a : ActiveSet k t, f a) := by
…

    Mentions: OAI.UniqueGamesTheorem.Soundness.PartnerSampling.ActiveSet, OAI.UniqueGamesTheorem.Soundness.PartnerSampling.Partner

  38. theorem OAI.UniqueGamesTheorem.Soundness.PartnerSampling.partner_expect_active line 282
  39. theorem OAI.UniqueGamesTheorem.Soundness.PartnerSampling.partner_pair_expect_active line 286
  40. theorem OAI.UniqueGamesTheorem.Soundness.PartnerSampling.partner_active_overlap_probability_le line 298

    Source documentation

    The independently drawn full partners obey the same active-overlap bound.

    theorem partner_active_overlap_probability_le {k t : ℕ} (hk : 0 < k) (htk : t ≤ k) :
    (𝔼 p : Partner k t, 𝔼 q : Partner k t,
      if (p.1.val ∩ q.1.val).Nonempty then (1 : ℝ) else 0) ≤ (t : ℝ)^2 / k := by
…

    Mentions: OAI.UniqueGamesTheorem.Soundness.PartnerSampling.Partner

  41. def OAI.UniqueGamesTheorem.Soundness.PartnerSampling.active line 304
  42. def OAI.UniqueGamesTheorem.Soundness.PartnerSampling.decodeSlot line 307
  43. def OAI.UniqueGamesTheorem.Soundness.PartnerSampling.slots line 310
  44. def OAI.UniqueGamesTheorem.Soundness.PartnerSampling.kernel line 313
  45. def OAI.UniqueGamesTheorem.Soundness.PartnerSampling.activeSubtypeEquiv line 317
  46. theorem OAI.UniqueGamesTheorem.Soundness.PartnerSampling.kernel_finrank line 321
  47. theorem OAI.UniqueGamesTheorem.Soundness.PartnerSampling.kernel_inf_finrank_le line 329
  48. theorem OAI.UniqueGamesTheorem.Soundness.PartnerSampling.kernel_inf_eq_bot_of_no_overlap line 336
  49. def OAI.UniqueGamesTheorem.Soundness.PartnerSampling.activeOverlap line 349
  50. def OAI.UniqueGamesTheorem.Soundness.PartnerSampling.kernelCollision line 352
  51. theorem OAI.UniqueGamesTheorem.Soundness.PartnerSampling.kernelCollision_le_activeOverlap line 357
  52. theorem OAI.UniqueGamesTheorem.Soundness.PartnerSampling.kernel_collision_probability_le line 367
  53. theorem OAI.UniqueGamesTheorem.Soundness.PartnerSampling.kernel_overlap_weight_pointwise line 381
  54. theorem OAI.UniqueGamesTheorem.Soundness.PartnerSampling.kernel_overlap_weight_le line 397
  55. theorem OAI.UniqueGamesTheorem.Soundness.ActualMapComparison.actual_partner_expectation_comparison line 438
  56. theorem OAI.UniqueGamesTheorem.Soundness.ActualMapComparison.actual_partner_expectation_comparison_dimension line 467
  57. theorem OAI.UniqueGamesTheorem.Soundness.ActualMapComparison.actual_partner_expectation_quarter line 486
  58. def OAI.UniqueGamesTheorem.Soundness.PartnerFullSampling.restrictIndices line 525
  59. def OAI.UniqueGamesTheorem.Soundness.PartnerFullSampling.restrictionProductEquiv line 529

    Source documentation

    The values inside and outside a finite set reconstruct the full tuple.

    def restrictionProductEquiv {P X : Type*} [DecidableEq P] (J : Finset P) :
    (P → X) ≃ ((↥J → X) × ({j : P // j ∉ J} → X)) where
…
  60. theorem OAI.UniqueGamesTheorem.Soundness.PartnerFullSampling.expect_restrictIndices line 546

    Source documentation

    Marginalizing the nonempty complement tuple gives the exact uniform law on the active coordinates. This includes an empty active set or complement.

    theorem expect_restrictIndices {P X : Type*} [Fintype P] [DecidableEq P]
    [Fintype X] [Nonempty X] (J : Finset P) (h : (↥J → X) → ℝ) :
    (𝔼 indices : P → X, h (restrictIndices J indices)) =
      𝔼 activeIndices : ↥J → X, h activeIndices := by
…

    Mentions: OAI.UniqueGamesTheorem.Soundness.PartnerFullSampling.restrictIndices

  61. def OAI.UniqueGamesTheorem.Soundness.PartnerFullSampling.fromFullIndices line 560
  62. theorem OAI.UniqueGamesTheorem.Soundness.PartnerFullSampling.fixed_active_expect_fullIndices line 564

    Source documentation

    Fixed-active-set form of the actual three-way slot sampling identity.

    theorem fixed_active_expect_fullIndices {k t : ℕ} (a : ActiveSet k t)
    (h : (↥a.val → Fin 3) → ℝ) :
    (𝔼 indices : Fin k → Fin 3, h (restrictIndices a.val indices)) =
      𝔼 activeIndices : ↥a.val → Fin 3, h activeIndices :=
…

    Mentions: OAI.UniqueGamesTheorem.Soundness.PartnerFullSampling.restrictIndices

  63. theorem OAI.UniqueGamesTheorem.Soundness.PartnerFullSampling.partner_expect_active_slots line 572

    Source documentation

    All active-set fibers have 3^t elements, so the uniform dependent-pair average is the active-set average of the uniform slot average.

    theorem partner_expect_active_slots (k t : ℕ) (f : Partner k t → ℝ) :
    (𝔼 p : Partner k t, f p) =
      𝔼 a : ActiveSet k t, 𝔼 indices : ↥a.val → Fin 3, f ⟨a, indices⟩ := by
…
  64. theorem OAI.UniqueGamesTheorem.Soundness.PartnerFullSampling.partner_expect_fullIndices line 584

    Source documentation

    The full-index experiment has exactly the existing Partner law. No independence or equality of probability laws is assumed.

    theorem partner_expect_fullIndices (k t : ℕ) (f : Partner k t → ℝ) :
    (𝔼 p : Partner k t, f p) =
      𝔼 a : ActiveSet k t, 𝔼 indices : Fin k → Fin 3,
        f (fromFullIndices a indices) := by
…

    Mentions: OAI.UniqueGamesTheorem.Soundness.PartnerFullSampling.fromFullIndices

  65. theorem OAI.UniqueGamesTheorem.Soundness.PartnerFullSampling.projection_eq_of_slots_eq_on_active line 594

    Source documentation

    Slots outside active positions have no effect on the genuine projection.

    theorem projection_eq_of_slots_eq_on_active {P : Type}
    (rhs active : P → Bool) (slot slot' : P → PartnerProjection.Slot)
    (hslot : ∀ j, active j = true → slot j = slot' j) :
    PartnerLinear.projection rhs active slot =
      PartnerLinear.projection rhs active slot' := by
…

    Mentions: OAI.UniqueGamesTheorem.Soundness.PartnerProjection.Slot, OAI.UniqueGamesTheorem.Soundness.PartnerLinear.projection

  66. theorem OAI.UniqueGamesTheorem.Soundness.PartnerFullSampling.projection_fromFullIndices line 613

    Source documentation

    Defaulting inactive slots to .first gives the same map as retaining all the independently sampled full indices.

    theorem projection_fromFullIndices {k t : ℕ} (rhs : Fin k → Bool)
    (a : ActiveSet k t) (indices : Fin k → Fin 3) :
    PartnerLinear.projection rhs (active (fromFullIndices a indices))
        (slots (fromFullIndices a indices)) =
      PartnerLinear.projection rhs (active (fromFullIndices a indices))
        (fun j => decodeSlot (indices j)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Soundness.PartnerLinear.projection, OAI.UniqueGamesTheorem.Soundness.PartnerFullSampling.fromFullIndices

  67. def OAI.UniqueGamesTheorem.Soundness.PartnerFullSampling.drawProductEquiv line 628

    Source documentation

    Drawing an occurrence and a slot at each position is the same finite sample space as drawing the occurrence tuple and the slot tuple separately.

    def drawProductEquiv {P Id : Type*} :
    (P → Id × Fin 3) ≃ ((P → Id) × (P → Fin 3)) where
…
  68. theorem OAI.UniqueGamesTheorem.Soundness.PartnerFullSampling.fixed_active_rawDraw_expect line 638

    Source documentation

    The raw occurrence/slot draw induces independent uniform occurrences and uniform active slots, with all unused slot choices marginalized exactly.

    theorem fixed_active_rawDraw_expect {k t : ℕ} {Id : Type*} [Fintype Id]
    (a : ActiveSet k t)
    (f : (Fin k → Id) → (↥a.val → Fin 3) → ℝ) :
    (𝔼 draw : Fin k → Id × Fin 3,
      f (fun j => (draw j).1)
        (restrictIndices a.val (fun j => (draw j).2))) =
      𝔼 occurrence : Fin k → Id, 𝔼 indices : ↥a.val → Fin 3,
        f occurrence indices := by
…

    Mentions: OAI.UniqueGamesTheorem.Soundness.PartnerFullSampling.restrictIndices

  69. theorem OAI.UniqueGamesTheorem.Soundness.PartnerFullSampling.occurrence_partner_expect_eq_rawDraw line 667

    Source documentation

    The actual raw draw, including indices outside the active set, agrees with the occurrence-then-partner experiment for every real test function.

    theorem occurrence_partner_expect_eq_rawDraw (k t : ℕ)
    {Id : Type*} [Fintype Id] (f : (Fin k → Id) → Partner k t → ℝ) :
    (𝔼 occurrence : Fin k → Id, 𝔼 p : Partner k t, f occurrence p) =
      𝔼 a : ActiveSet k t, 𝔼 draw : Fin k → Id × Fin 3,
        f (fun j => (draw j).1) (fromFullIndices a (fun j => (draw j).2)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Soundness.PartnerFullSampling.fromFullIndices

  70. def OAI.UniqueGamesTheorem.Soundness.ActualMapComparison.sourcePrecomposeEquiv line 699
  71. theorem OAI.UniqueGamesTheorem.Soundness.ActualMapComparison.uniformMean_sourcePrecompose line 716
  72. theorem OAI.UniqueGamesTheorem.Soundness.ActualMapComparison.actual_partner_expectation_quarter_equiv line 727
  73. def OAI.UniqueGamesTheorem.Soundness.UniformPartition.mean line 766
  74. theorem OAI.UniqueGamesTheorem.Soundness.UniformPartition.mean_equiv line 769
  75. def OAI.UniqueGamesTheorem.Soundness.UniformPartition.fiberSum line 774
  76. def OAI.UniqueGamesTheorem.Soundness.UniformPartition.fiberSize line 778
  77. theorem OAI.UniqueGamesTheorem.Soundness.UniformPartition.fiberSize_eq_card line 781
  78. theorem OAI.UniqueGamesTheorem.Soundness.UniformPartition.sum_fiberSum line 789
  79. theorem OAI.UniqueGamesTheorem.Soundness.UniformPartition.fiberSize_mul line 798
  80. theorem OAI.UniqueGamesTheorem.Soundness.UniformPartition.fiberSize_pos line 807
  81. theorem OAI.UniqueGamesTheorem.Soundness.UniformPartition.fiberSize_mul_conditional line 816
  82. theorem OAI.UniqueGamesTheorem.Soundness.UniformPartition.total_mean line 826
  83. theorem OAI.UniqueGamesTheorem.Soundness.UniformPartition.mean_mono line 845
  84. theorem OAI.UniqueGamesTheorem.Soundness.UniformPartition.mean_le_partition_bound line 849
  85. theorem OAI.UniqueGamesTheorem.Soundness.UniformPartition.fiber_conditional_eq_subtype_mean line 859