MaskMoment.lean`

92 declarations, 0 contain sorry, 0 declared as axioms

Averaging the actual sparse clean experiment

The explicit seed has an independent singleton coin and uniform single-column advice at each position. Additional independent data supply the intercept and both full-block columns. Unused columns are sampled and discarded, allowing a fixed finite product sample space. A local strategy may depend on the fixed seed; the bound consequently also covers the original, less informed players.

The only mathematical rate input below is the stated bound on the actual ordinary repeated game. No conditional distribution, local reconstruction, mask distribution, or averaging assertion is assumed.

def OAI.MaxCutGames.Clean.bernoulli line 14

Source documentation

true is the singleton branch.

def bernoulli (p : ℝ) (hp₀ : 0 ≤ p) (hp₁ : p ≤ 1) :
    FiniteDistribution Bool where
…

def OAI.MaxCutGames.Clean.maskCount line 21
Source documentation
The exact mask, including the empty mask at k = 0.
```
def maskCount {k : ℕ} (mask : Fin k → Bool) : ℕ :=
…
```
theorem OAI.MaxCutGames.Clean.product_mask line 24

theorem OAI.MaxCutGames.Clean.iid_product_moment line 30

Source documentation

The finite product identity underlying the binomial generating function.

theorem iid_product_moment {Ω : Type*} [Fintype Ω]
    (μ : FiniteDistribution Ω) (f : Ω → ℝ) (k : ℕ) :
    (μ.iid k).expectation (fun x => ∏ i, f (x i)) = μ.expectation f ^ k := by
…

theorem OAI.MaxCutGames.Clean.bernoulli_mask_moment line 40
def OAI.MaxCutGames.Clean.cleanProbability line 57
theorem OAI.MaxCutGames.Clean.cleanProbability_nonneg line 61
theorem OAI.MaxCutGames.Clean.cleanProbability_le_one line 65
def OAI.MaxCutGames.Clean.singletonSlopeLaw line 73
Source documentation
Independent singleton choice and uniform advice slope.
```
def singletonSlopeLaw (β : ℝ) (hβ₀ : 0 ≤ β) (hβ₁ : β ≤ 1) :
    FiniteDistribution (Bool × E) :=
…
```
def OAI.MaxCutGames.Clean.cleanBit line 79
Source documentation
origin is instantiated by the zero advice slope. Keeping it explicit also shows that every specified slope has exactly the same chance.
```
def cleanBit (origin : E) (sample : Bool × E) : Bool := by
…
```
theorem OAI.MaxCutGames.Clean.clean_pushforward line 83
theorem OAI.MaxCutGames.Clean.clean_mask_law line 104
Source documentation
In particular, the whole mask has the independent Bernoulli law.
```
theorem clean_mask_law (β : ℝ) (hβ₀ : 0 ≤ β) (hβ₁ : β ≤ 1)
    (origin : E) (k : ℕ) :
    ((singletonSlopeLaw (E := E) β hβ₀ hβ₁).iid k).pushforward
…
```
Mentions: OAI.MaxCutGames.Clean.singletonSlopeLaw
theorem OAI.MaxCutGames.Clean.clean_mask_moment line 112
theorem OAI.MaxCutGames.Clean.cleanProbability_ge_of_card_le line 122
theorem OAI.MaxCutGames.Clean.cleanProbability_ge_dimension line 128

theorem OAI.MaxCutGames.Clean.mask_rate_antitone line 136

Source documentation

Larger clean probability decreases the moment for a rate in [0,1].

theorem mask_rate_antitone {p q ρ : ℝ} (hp₀ : 0 ≤ p) (hp₁ : p ≤ 1)
    (hqp : q ≤ p) (hρ₀ : 0 ≤ ρ) (hρ₁ : ρ ≤ 1) (k : ℕ) :
    (1 - p * (1 - ρ)) ^ k ≤ (1 - q * (1 - ρ)) ^ k := by
…

theorem OAI.MaxCutGames.Clean.clean_mask_moment_le line 146
Source documentation
Section 5's numerical specialization. A bound on the number of possible advice slopes gives a uniform bound over every fixed advice map.
```
theorem clean_mask_moment_le (β : ℝ) (hβ₀ : 0 ≤ β) (hβ₁ : β ≤ 1)
    (origin : E) (k : ℕ) {N : ℝ} (hcard : (Fintype.card E : ℝ) ≤ N) :
    ((singletonSlopeLaw (E := E) β hβ₀ hβ₁).iid k).expectation
…
```
Mentions: OAI.MaxCutGames.Clean.singletonSlopeLaw

theorem OAI.MaxCutGames.Clean.clean_mask_moment_le_dimension line 160

Source documentation

2^(dim W + r_s) is chosen before the particular advice-map rank.

theorem clean_mask_moment_le_dimension (β : ℝ) (hβ₀ : 0 ≤ β) (hβ₁ : β ≤ 1)
    (origin : E) (k dimW rs : ℕ) (hcard : Fintype.card E ≤ 2 ^ (dimW + rs)) :
    ((singletonSlopeLaw (E := E) β hβ₀ hβ₁).iid k).expectation
…

Mentions: OAI.MaxCutGames.Clean.singletonSlopeLaw

theorem OAI.MaxCutGames.Clean.mask_rate_le_exp line 171
Source documentation
The exponential estimate uses nonnegativity of 1 - x before raising to a natural power. It also covers the empty mask.
```
theorem mask_rate_le_exp {x : ℝ} (hx : x ≤ 1) (k : ℕ) :
    (1 - x) ^ k ≤ Real.exp (-(k : ℝ) * x) := by
…
```
theorem OAI.MaxCutGames.Clean.clean_mask_moment_le_exp line 181
theorem OAI.MaxCutGames.Clean.cube_singleton_probability_nonneg line 197
theorem OAI.MaxCutGames.Clean.cube_singleton_probability_le_one line 200

theorem OAI.MaxCutGames.Clean.cube_mask_rate_le_exp line 210

Source documentation

On cubes, k = n^3 and beta = n^(-2), so k * beta = n. The advice-space size bound N is fixed independently of n.

theorem cube_mask_rate_le_exp {n : ℕ} (hn : 1 ≤ n) {N : ℝ} (hN : 1 ≤ N) :
    (1 - ((1 / (n : ℝ)) ^ 2 / N) / 3600) ^ (n ^ 3) ≤
      Real.exp (-(n : ℝ) / (3600 * N)) := by
…

theorem OAI.MaxCutGames.Clean.exists_cube_exponential_lt line 234
Source documentation
A repetition cube can be selected after fixing only the advice-space size bound and the required error. This is a scalar fact, not a game-value theorem.
```
theorem exists_cube_exponential_lt {N error : ℝ} (hN : 0 < N) (herror : 0 < error) :
    ∃ n : ℕ, 1 ≤ n ∧ Real.exp (-(n : ℝ) / (3600 * N)) < error := by
…
```
theorem OAI.MaxCutGames.Clean.exists_cube_mask_rate_lt line 253
abbrev OAI.MaxCutGames.Clean.Experiment.Coefficient line 289
abbrev OAI.MaxCutGames.Clean.Experiment.Additional line 290
abbrev OAI.MaxCutGames.Clean.Experiment.SparseSeed line 291
def OAI.MaxCutGames.Clean.Experiment.singletonSet line 293
def OAI.MaxCutGames.Clean.Experiment.coefficients line 296
theorem OAI.MaxCutGames.Clean.Experiment.zeroSet_eq_cleanMask line 306
Source documentation
The actual zero coefficient set is exactly the clean mask counted by the Bernoulli law. The homogeneous intercept and full columns never enter it.
```
theorem zeroSet_eq_cleanMask {k : ℕ} (extra : Additional k R) (seed : SparseSeed k R) :
    zeroSet (singletonSet seed) (coefficients extra seed) =
      Finset.univ.filter (fun i => cleanBit (ZeroInformation.zero : Coefficient R) (seed i) = true) := by
…
```
Mentions: OAI.MaxCutGames.Clean.Experiment.Additional, OAI.MaxCutGames.Clean.Experiment.SparseSeed, OAI.MaxCutGames.Clean.Experiment.singletonSet, OAI.MaxCutGames.Clean.Experiment.coefficients, OAI.MaxCutGames.Clean.cleanBit, OAI.MaxCutGames.Clean.Experiment.Coefficient
theorem OAI.MaxCutGames.Clean.Experiment.zeroSet_card line 317
abbrev OAI.MaxCutGames.Clean.Experiment.LocalStrategies line 323

def OAI.MaxCutGames.Clean.Experiment.success line 327

Source documentation

Exact nested finite expectation of the advice-agreement experiment.

def success (k : ℕ) (μ : FiniteDistribution (O × Fin 3))
    (g : IncidenceExtraction.Incidence O N)
    (extraLaw : FiniteDistribution (Additional k R))
    (β : ℝ) (hβ₀ : 0 ≤ β) (hβ₁ : β ≤ 1)
    (strategy : Additional k R → SparseSeed k R → LocalStrategies k R O N) : ℝ :=
…

Mentions: OAI.MaxCutGames.Clean.Experiment.Additional, OAI.MaxCutGames.Clean.Experiment.SparseSeed, OAI.MaxCutGames.Clean.Experiment.LocalStrategies

theorem OAI.MaxCutGames.Clean.Experiment.expectation_mono_inline_Experiment line 337
theorem OAI.MaxCutGames.Clean.Experiment.expectation_const_inline_Experiment line 343

theorem OAI.MaxCutGames.Clean.Experiment.success_le_of_repetition line 350

Source documentation

Exact clean-coordinate upper bound for arbitrary weighted occurrences. The sole external theorem input rate concerns the genuine classical repeated game, so its alphabet dependence cannot be concealed in this interface.

theorem success_le_of_repetition (k : ℕ) (μ : FiniteDistribution (O × Fin 3))
    (g : IncidenceExtraction.Incidence O N)
    (extraLaw : FiniteDistribution (Additional k R))
    (β : ℝ) (hβ₀ : 0 ≤ β) (hβ₁ : β ≤ 1)
    (strategy : Additional k R → SparseSeed k R → LocalStrategies k R O N)
    (distinct : ∀ o i j, g.name o i = g.name o j → i = j)
    (ρ : ℝ)
    (rate : ∀ n, ((incidenceGame g (μ.pushforward (incidence g.name))).repetition n).value ≤ ρ ^ n) :
    success k μ g extraLaw β hβ₀ hβ₁ strategy ≤
      (1 - (β / (Fintype.card (Coefficient R) : ℝ)) * (1 - ρ)) ^ k := by
…

Mentions: OAI.MaxCutGames.Clean.Experiment.Additional, OAI.MaxCutGames.Clean.Experiment.SparseSeed, OAI.MaxCutGames.Clean.Experiment.LocalStrategies, OAI.MaxCutGames.Clean.Experiment.success, OAI.MaxCutGames.Clean.Experiment.Coefficient

theorem OAI.MaxCutGames.Clean.Experiment.randomized_success_le_of_repetition line 379

Source documentation

Uniform finite private/shared strategy seeds are also covered by the same constant bound; the seed is sampled before the questions.

theorem randomized_success_le_of_repetition {Seed : Type*} [Fintype Seed]
    (k : ℕ) (μ : FiniteDistribution (O × Fin 3))
    (g : IncidenceExtraction.Incidence O N)
    (extraLaw : FiniteDistribution (Additional k R))
    (β : ℝ) (hβ₀ : 0 ≤ β) (hβ₁ : β ≤ 1)
    (seedLaw : FiniteDistribution Seed)
    (strategy : Seed → Additional k R → SparseSeed k R → LocalStrategies k R O N)
    (distinct : ∀ o i j, g.name o i = g.name o j → i = j)
    (ρ : ℝ)
    (rate : ∀ n, ((incidenceGame g (μ.pushforward (incidence g.name))).repetition n).value ≤ ρ ^ n) :
    seedLaw.expectation (fun seed => success k μ g extraLaw β hβ₀ hβ₁ (strategy seed)) ≤
      (1 - (β / (Fintype.card (Coefficient R) : ℝ)) * (1 - ρ)) ^ k := by
…

def OAI.MaxCutGames.Soundness.SubsetIntersection.subsets line 415
Source documentation
The actual finite sample space of all t-subsets of Fin k.
```
def subsets (k t : ℕ) : Finset (Finset (Fin k)) :=
…
```
def OAI.MaxCutGames.Soundness.SubsetIntersection.uniformMean line 419
Source documentation
Uniform expectation, implemented by its normalized finite sum.
```
def uniformMean (k t : ℕ) (f : Finset (Fin k) → ℚ) : ℚ :=
…
```
def OAI.MaxCutGames.Soundness.SubsetIntersection.independentMean line 423
Source documentation
Independent draws use the product of the two uniform laws.
```
def independentMean (k t : ℕ) (f : Finset (Fin k) → Finset (Fin k) → ℚ) : ℚ :=
…
```
def OAI.MaxCutGames.Soundness.SubsetIntersection.memberIndicator line 426
def OAI.MaxCutGames.Soundness.SubsetIntersection.overlapProbability line 429
theorem OAI.MaxCutGames.Soundness.SubsetIntersection.independentMean_eq_double_sum line 434
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.MaxCutGames.Soundness.SubsetIntersection.independentMean, OAI.MaxCutGames.Soundness.SubsetIntersection.subsets
theorem OAI.MaxCutGames.Soundness.SubsetIntersection.uniformMean_mul_left line 442
theorem OAI.MaxCutGames.Soundness.SubsetIntersection.uniformMean_mul_right line 448
theorem OAI.MaxCutGames.Soundness.SubsetIntersection.independentMean_product line 455
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.MaxCutGames.Soundness.SubsetIntersection.independentMean, OAI.MaxCutGames.Soundness.SubsetIntersection.uniformMean
theorem OAI.MaxCutGames.Soundness.SubsetIntersection.subsets_card line 459
theorem OAI.MaxCutGames.Soundness.SubsetIntersection.subsets_nonempty line 462
theorem OAI.MaxCutGames.Soundness.SubsetIntersection.subsets_card_ne_zero line 466
theorem OAI.MaxCutGames.Soundness.SubsetIntersection.count_containing line 471
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.MaxCutGames.Soundness.SubsetIntersection.subsets
theorem OAI.MaxCutGames.Soundness.SubsetIntersection.choose_predecessor_ratio line 478
theorem OAI.MaxCutGames.Soundness.SubsetIntersection.inclusion_probability line 490
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.MaxCutGames.Soundness.SubsetIntersection.uniformMean, OAI.MaxCutGames.Soundness.SubsetIntersection.memberIndicator
theorem OAI.MaxCutGames.Soundness.SubsetIntersection.independent_inclusion_probability line 501
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.MaxCutGames.Soundness.SubsetIntersection.independentMean, OAI.MaxCutGames.Soundness.SubsetIntersection.memberIndicator
theorem OAI.MaxCutGames.Soundness.SubsetIntersection.uniformMean_congr line 507
theorem OAI.MaxCutGames.Soundness.SubsetIntersection.uniformMean_const line 512
theorem OAI.MaxCutGames.Soundness.SubsetIntersection.uniformMean_finset_sum line 518
theorem OAI.MaxCutGames.Soundness.SubsetIntersection.uniformMean_mono line 526
theorem OAI.MaxCutGames.Soundness.SubsetIntersection.independentMean_mono line 531
theorem OAI.MaxCutGames.Soundness.SubsetIntersection.intersection_card_indicator line 539
theorem OAI.MaxCutGames.Soundness.SubsetIntersection.expected_intersection_fixed line 545
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.MaxCutGames.Soundness.SubsetIntersection.uniformMean
theorem OAI.MaxCutGames.Soundness.SubsetIntersection.expected_intersection line 553
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.MaxCutGames.Soundness.SubsetIntersection.independentMean
theorem OAI.MaxCutGames.Soundness.SubsetIntersection.nonempty_indicator_le_card line 568
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
…
```
theorem OAI.MaxCutGames.Soundness.SubsetIntersection.overlap_probability_le line 575
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.MaxCutGames.Soundness.SubsetIntersection.overlapProbability
abbrev OAI.MaxCutGames.Soundness.PartnerSampling.ActiveSet line 590
Source documentation
The literal support of the uniform active-set sample.
```
abbrev ActiveSet (k t : ℕ) := ↥(subsets k t)
```
abbrev OAI.MaxCutGames.Soundness.PartnerSampling.Partner line 593
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.MaxCutGames.Soundness.PartnerSampling.ActiveSet
theorem OAI.MaxCutGames.Soundness.PartnerSampling.activeSet_card line 595
theorem OAI.MaxCutGames.Soundness.PartnerSampling.slotTuples_card line 598
theorem OAI.MaxCutGames.Soundness.PartnerSampling.partner_card line 603
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.MaxCutGames.Soundness.PartnerSampling.Partner
theorem OAI.MaxCutGames.Soundness.PartnerSampling.partner_nonempty line 609
theorem OAI.MaxCutGames.Soundness.PartnerSampling.uniformMean_real_cast line 613
theorem OAI.MaxCutGames.Soundness.PartnerSampling.independentMean_real_cast line 619

theorem OAI.MaxCutGames.Soundness.PartnerSampling.subset_overlap_probability_le line 626

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
…

theorem OAI.MaxCutGames.Soundness.PartnerSampling.activeSet_expect line 636
theorem OAI.MaxCutGames.Soundness.PartnerSampling.partner_expect_activeSet line 642
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.MaxCutGames.Soundness.PartnerSampling.ActiveSet, OAI.MaxCutGames.Soundness.PartnerSampling.Partner
theorem OAI.MaxCutGames.Soundness.PartnerSampling.partner_expect_active line 655
theorem OAI.MaxCutGames.Soundness.PartnerSampling.partner_pair_expect_active line 659
theorem OAI.MaxCutGames.Soundness.PartnerSampling.partner_active_overlap_probability_le line 671
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.MaxCutGames.Soundness.PartnerSampling.Partner
def OAI.MaxCutGames.Soundness.PartnerSampling.active line 677
def OAI.MaxCutGames.Soundness.PartnerSampling.decodeSlot line 680
def OAI.MaxCutGames.Soundness.PartnerSampling.slots line 683
def OAI.MaxCutGames.Soundness.PartnerSampling.kernel line 686
def OAI.MaxCutGames.Soundness.PartnerSampling.activeSubtypeEquiv line 690
theorem OAI.MaxCutGames.Soundness.PartnerSampling.kernel_finrank line 694
theorem OAI.MaxCutGames.Soundness.PartnerSampling.kernel_inf_finrank_le line 702
theorem OAI.MaxCutGames.Soundness.PartnerSampling.kernel_inf_eq_bot_of_no_overlap line 709
def OAI.MaxCutGames.Soundness.PartnerSampling.activeOverlap line 722
def OAI.MaxCutGames.Soundness.PartnerSampling.kernelCollision line 725
theorem OAI.MaxCutGames.Soundness.PartnerSampling.kernelCollision_le_activeOverlap line 730
theorem OAI.MaxCutGames.Soundness.PartnerSampling.kernel_collision_probability_le line 740
theorem OAI.MaxCutGames.Soundness.PartnerSampling.kernel_overlap_weight_pointwise line 754
theorem OAI.MaxCutGames.Soundness.PartnerSampling.kernel_overlap_weight_le line 770