AdviceFibersLemmas.lean`

86 declarations, 0 contain sorry, 0 declared as axioms

Exact visible row advice and private matrix coordinates

Every nonempty fiber of M ↦ A ∘ M is an affine copy of Hom(E, ker A), whether or not A is surjective. Choosing one base matrix for each attainable row gives a product decomposition of the complete matrix space. Uniform sampling therefore makes visible row advice and the hidden kernel-valued matrix independent.

abbrev OAI.UniqueGamesTheorem.Decoder.AdviceFibers.RowFiber line 37
Source documentation
Actual matrices with the specified observed row advice.
```
abbrev RowFiber (A : K →ₗ[F2] R) (S : E →ₗ[F2] R) :=
…
```
def OAI.UniqueGamesTheorem.Decoder.AdviceFibers.kernelDifference line 41
Source documentation
Hidden coordinates relative to one base matrix in the same row fiber.
```
def kernelDifference (A : K →ₗ[F2] R) (S : E →ₗ[F2] R)
    (M₀ : E →ₗ[F2] K) (h₀ : A.comp M₀ = S) (M : RowFiber A S) :
    E →ₗ[F2] A.ker :=
…
```
Mentions: OAI.UniqueGamesTheorem.Decoder.AdviceFibers.RowFiber
theorem OAI.UniqueGamesTheorem.Decoder.AdviceFibers.kernelDifference_apply line 54
def OAI.UniqueGamesTheorem.Decoder.AdviceFibers.assemble line 59
Source documentation
Reassemble an actual matrix from its fixed visible base and private part.
```
def assemble (A : K →ₗ[F2] R) (M₀ : E →ₗ[F2] K)
    (N : E →ₗ[F2] A.ker) : E →ₗ[F2] K :=
…
```
theorem OAI.UniqueGamesTheorem.Decoder.AdviceFibers.assemble_apply line 63
theorem OAI.UniqueGamesTheorem.Decoder.AdviceFibers.observed_assemble line 68
Source documentation
Observed advice is completely unchanged by the private coordinates.
```
theorem observed_assemble (A : K →ₗ[F2] R) (M₀ : E →ₗ[F2] K)
    (N : E →ₗ[F2] A.ker) : A.comp (assemble A M₀ N) = A.comp M₀ := by
…
```
Mentions: OAI.UniqueGamesTheorem.Decoder.AdviceFibers.assemble
def OAI.UniqueGamesTheorem.Decoder.AdviceFibers.rowFiberEquiv line 75
Source documentation
The exact row-fiber bijection; no rank or surjectivity premise is needed.
```
def rowFiberEquiv (A : K →ₗ[F2] R) (S : E →ₗ[F2] R)
    (M₀ : E →ₗ[F2] K) (h₀ : A.comp M₀ = S) :
    (E →ₗ[F2] A.ker) ≃ RowFiber A S where
…
```
Mentions: OAI.UniqueGamesTheorem.Decoder.AdviceFibers.RowFiber
theorem OAI.UniqueGamesTheorem.Decoder.AdviceFibers.rowFiberEquiv_coe line 92
theorem OAI.UniqueGamesTheorem.Decoder.AdviceFibers.rowFiberEquiv_symm line 96
theorem OAI.UniqueGamesTheorem.Decoder.AdviceFibers.assemble_affine_target line 101
Source documentation
Affine target intercepts are retained in the private coordinates.
```
theorem assemble_affine_target (A : K →ₗ[F2] R) (M₀ : E →ₗ[F2] K)
    (N : E →ₗ[F2] A.ker) (z : E) (u : K) :
    assemble A M₀ N z + u = (N z : K) + (M₀ z + u) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Decoder.AdviceFibers.assemble
theorem OAI.UniqueGamesTheorem.Decoder.AdviceFibers.rowFiber_card line 112
theorem OAI.UniqueGamesTheorem.Decoder.AdviceFibers.rowFiber_expect line 117
Source documentation
Uniform private matrices push forward to uniform matrices in the fiber.
```
theorem rowFiber_expect (M₀ : E →ₗ[F2] K) (h₀ : A.comp M₀ = S)
    [Fintype (RowFiber A S)] (f : (E →ₗ[F2] K) → ℝ) :
    (𝔼 M : RowFiber A S, f M.val) =
      𝔼 N : E →ₗ[F2] A.ker, f (assemble A M₀ N) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Decoder.AdviceFibers.RowFiber, OAI.UniqueGamesTheorem.Decoder.AdviceFibers.assemble
abbrev OAI.UniqueGamesTheorem.Decoder.AdviceFibers.ObservedRow line 127
Source documentation
Only attainable rows are observation values.
```
abbrev ObservedRow (A : K →ₗ[F2] R) :=
…
```
def OAI.UniqueGamesTheorem.Decoder.AdviceFibers.observe line 130
def OAI.UniqueGamesTheorem.Decoder.AdviceFibers.observedBase line 134
Source documentation
A canonical base depends only on observed advice, never on the hidden matrix.
```
def observedBase (A : K →ₗ[F2] R) (S : ObservedRow (E := E) A) : E →ₗ[F2] K :=
…
```
Mentions: OAI.UniqueGamesTheorem.Decoder.AdviceFibers.ObservedRow
theorem OAI.UniqueGamesTheorem.Decoder.AdviceFibers.observedBase_property line 137
def OAI.UniqueGamesTheorem.Decoder.AdviceFibers.hiddenCoordinate line 140
theorem OAI.UniqueGamesTheorem.Decoder.AdviceFibers.observe_assemble_base line 145
def OAI.UniqueGamesTheorem.Decoder.AdviceFibers.observationEquiv line 152
Source documentation
Full matrix space is a product of attainable visible rows and private kernel-valued maps. A section of A is not required.
```
def observationEquiv (A : K →ₗ[F2] R) :
    (E →ₗ[F2] K) ≃ ObservedRow (E := E) A × (E →ₗ[F2] A.ker) where
…
```
Mentions: OAI.UniqueGamesTheorem.Decoder.AdviceFibers.ObservedRow
theorem OAI.UniqueGamesTheorem.Decoder.AdviceFibers.observationEquiv_apply line 172
theorem OAI.UniqueGamesTheorem.Decoder.AdviceFibers.observation_expect line 181
Source documentation
The joint law is exactly the uniform product law.
```
theorem observation_expect (f : ObservedRow (E := E) A → (E →ₗ[F2] A.ker) → ℝ) :
…
```
Mentions: OAI.UniqueGamesTheorem.Decoder.AdviceFibers.ObservedRow
theorem OAI.UniqueGamesTheorem.Decoder.AdviceFibers.observed_hidden_independent line 190
Source documentation
Exact factorization of every product of visible and private observables.
```
theorem observed_hidden_independent (f : ObservedRow (E := E) A → ℝ)
…
```
Mentions: OAI.UniqueGamesTheorem.Decoder.AdviceFibers.ObservedRow
def OAI.UniqueGamesTheorem.Decoder.NoiseSampler.samplerLaw line 228
Source documentation
The real pushforward of the uniform law on sampler outcomes.
```
def samplerLaw (noise : Noise → V) (v : V) : ℝ := by
…
```
theorem OAI.UniqueGamesTheorem.Decoder.NoiseSampler.samplerLaw_nonneg line 233
theorem OAI.UniqueGamesTheorem.Decoder.NoiseSampler.samplerLaw_eq_count line 244
Source documentation
Literal counting formula; multiple sampler outcomes mapping to the same vector retain their multiplicity.
```
theorem samplerLaw_eq_count (noise : Noise → V) (v : V) :
    samplerLaw noise v =
      ((Finset.univ.filter fun n => noise n = v).card : ℝ) / Fintype.card Noise := by
…
```
Mentions: OAI.UniqueGamesTheorem.Decoder.NoiseSampler.samplerLaw
theorem OAI.UniqueGamesTheorem.Decoder.NoiseSampler.samplerLaw_sum line 252
theorem OAI.UniqueGamesTheorem.Decoder.NoiseSampler.sample_expect_eq line 263
Source documentation
Exact pushforward expectation, with the uniform normalization explicit.
```
theorem sample_expect_eq (noise : Noise → V) (f : V → ℝ) :
    (𝔼 n, f (noise n)) = ∑ v, samplerLaw noise v * f v := by
…
```
Mentions: OAI.UniqueGamesTheorem.Decoder.NoiseSampler.samplerLaw
theorem OAI.UniqueGamesTheorem.Decoder.NoiseSampler.samplerLaw_normalized line 267
theorem OAI.UniqueGamesTheorem.Decoder.NoiseSampler.rat_expect_cast line 272
theorem OAI.UniqueGamesTheorem.Decoder.NoiseSampler.samplerLaw_eq_rat_count line 277
theorem OAI.UniqueGamesTheorem.Decoder.NoiseSampler.sample_kernel_eq_eigenvalue line 293
Source documentation
The actual matrix multiplier is precisely the sampler's kernel event.
```
theorem sample_kernel_eq_eigenvalue (noise : Noise → V) (S : V →ₗ[F2] E) :
    (𝔼 n, if S (noise n) = 0 then (1 : ℝ) else 0) =
      linearNoiseEigenvalue (samplerLaw noise) S := by
…
```
Mentions: OAI.UniqueGamesTheorem.Decoder.NoiseSampler.samplerLaw
theorem OAI.UniqueGamesTheorem.Decoder.NoiseSampler.detection_add_eigenvalue line 300
Source documentation
Detection plus annihilation is one for the same unconditional sampler.
```
theorem detection_add_eigenvalue [Nonempty Noise]
    (noise : Noise → V) (S : V →ₗ[F2] E) :
    (𝔼 n, if S (noise n) ≠ 0 then (1 : ℝ) else 0) +
      linearNoiseEigenvalue (samplerLaw noise) S = 1 := by
…
```
Mentions: OAI.UniqueGamesTheorem.Decoder.NoiseSampler.samplerLaw

theorem OAI.UniqueGamesTheorem.Decoder.NoiseSampler.detection_eigenvalue_le line 314

Source documentation

The constant-detection input becomes the 7/8 multiplier bound.

theorem detection_eigenvalue_le [Nonempty Noise]
    (noise : Noise → V) (S : V →ₗ[F2] E)
    (hdetect : (1 : ℝ) / 8 ≤ 𝔼 n, if S (noise n) ≠ 0 then (1 : ℝ) else 0) :
    linearNoiseEigenvalue (samplerLaw noise) S ≤ 7 / 8 := by
…

Mentions: OAI.UniqueGamesTheorem.Decoder.NoiseSampler.samplerLaw

theorem OAI.UniqueGamesTheorem.Decoder.NoiseSampler.detection_eigenvalue_le_complement line 322

Source documentation

A generic detection level bounds the annihilation multiplier.

theorem detection_eigenvalue_le_complement [Nonempty Noise]
    (noise : Noise → V) (S : V →ₗ[F2] E) (d : ℝ)
    (hdetect : d ≤ 𝔼 n, if S (noise n) ≠ 0 then (1 : ℝ) else 0) :
    linearNoiseEigenvalue (samplerLaw noise) S ≤ 1 - d := by
…

Mentions: OAI.UniqueGamesTheorem.Decoder.NoiseSampler.samplerLaw

theorem OAI.UniqueGamesTheorem.Decoder.NoiseSampler.rational_detection_eigenvalue_le line 330

Source documentation

The gadget may keep its finite probabilities rational throughout.

theorem rational_detection_eigenvalue_le [Nonempty Noise]
    (noise : Noise → V) (S : V →ₗ[F2] E)
    (hdetect : (1 : ℚ) / 8 ≤ 𝔼 n, if S (noise n) ≠ 0 then (1 : ℚ) else 0) :
    linearNoiseEigenvalue (samplerLaw noise) S ≤ 7 / 8 := by
…

Mentions: OAI.UniqueGamesTheorem.Decoder.NoiseSampler.samplerLaw

theorem OAI.UniqueGamesTheorem.Decoder.PositiveMultiplier.retained_mass_of_acceptance line 364

Source documentation

A 7/8 bound outside the retained set forces at least 0.92 retained mass when acceptance is at least 0.99. The statement keeps the exact rational constants, rather than assuming a low-rank mass premise.

theorem retained_mass_of_acceptance
    (w : J → ℝ) (a lam : (j : J) → I j → ℝ)
    (keep : (j : J) → I j → Prop)
    (hw : ∀ j, 0 ≤ w j) (htotal : energy w a = 1)
    (hone : ∀ j i, lam j i ≤ 1)
    (hhigh : ∀ j i, ¬ keep j i → lam j i ≤ 7 / 8)
    (haccept : (99 : ℝ) / 100 ≤ spectralEnergy w lam a) :
    (23 : ℝ) / 25 ≤ cutoffEnergy w keep a := by
…

theorem OAI.UniqueGamesTheorem.Decoder.PositiveMultiplier.positive_multiplier_comparison line 401

theorem OAI.UniqueGamesTheorem.Decoder.PositiveMultiplier.good_fiber_mass line 436

Source documentation

A finite probability law with mean at least 14.4 η assigns mass at least 10 η to acceptances at least 4 η.

theorem good_fiber_mass
    {Q : Type*} [Fintype Q] (μ p : Q → ℝ) (η : ℝ)
    (hμ : ∀ q, 0 ≤ μ q) (hμsum : ∑ q, μ q = 1)
    (hη : 0 ≤ η) (hp : ∀ q, p q ≤ 1)
    (hmean : (72 : ℝ) / 5 * η ≤ ∑ q, μ q * p q) :
    10 * η ≤ ∑ q, μ q * if 4 * η ≤ p q then 1 else 0 := by
…

def OAI.UniqueGamesTheorem.Decoder.PositiveMultiplier.equalityAcceptance line 468
Source documentation
The actual equality test, including zero perturbation factors.
```
def equalityAcceptance (ν : V → ℝ) (label : (E →ₗ[F2] V) → C) : ℝ := by
…
```
theorem OAI.UniqueGamesTheorem.Decoder.PositiveMultiplier.color_pair_sum line 475
theorem OAI.UniqueGamesTheorem.Decoder.PositiveMultiplier.equalityAcceptance_fourier line 485
Source documentation
Equality acceptance has the actual positive Fourier multiplier. Color indicators give the same equality expansion as output characters, with no extra factor depending on the output alphabet.
```
theorem equalityAcceptance_fourier (ν : V → ℝ)
    (label : (E →ₗ[F2] V) → C) :
    equalityAcceptance ν label =
      ∑ c, ∑ S : V →ₗ[F2] E,
        linearNoiseEigenvalue ν S * linearCoeff (colorIndicator label c) S ^ 2 := by
…
```
Mentions: OAI.UniqueGamesTheorem.Decoder.PositiveMultiplier.equalityAcceptance

theorem OAI.UniqueGamesTheorem.Decoder.PositiveMultiplier.matrix_test_comparison line 516

Source documentation

Spectral comparison applied to a genuine family of matrix labelings. The two explicit probability laws may be the latent gadget law and uniform sampling in the distinguished subspace, respectively.

theorem matrix_test_comparison
    (μ : Q → ℝ) (ν ρ : V → ℝ)
    (label : Q → (E →ₗ[F2] V) → C)
    (keep : (V →ₗ[F2] E) → Prop) (t : ℝ)
    (hμ : ∀ q, 0 ≤ μ q) (hμsum : ∑ q, μ q = 1)
    (hν : ∀ v, 0 ≤ ν v) (hνsum : ∑ v, ν v = 1)
    (hρ : ∀ v, 0 ≤ ρ v) (ht : 0 ≤ t)
    (hhigh : ∀ S : V →ₗ[F2] E, ¬ keep S → linearNoiseEigenvalue ν S ≤ 7 / 8)
    (hlow : ∀ S : V →ₗ[F2] E, keep S → t ≤ linearNoiseEigenvalue ρ S)
    (haccept : (99 : ℝ) / 100 ≤ ∑ q, μ q * equalityAcceptance ν (label q)) :
    (9 : ℝ) / 10 * t ≤ ∑ q, μ q * equalityAcceptance ρ (label q) := by
…

Mentions: OAI.UniqueGamesTheorem.Decoder.PositiveMultiplier.equalityAcceptance

def OAI.UniqueGamesTheorem.Decoder.PositiveMultiplier.subspaceLaw line 559
Source documentation
Pushforward of uniform sampling in K. For a subspace inclusion this is uniform sampling in that subspace; the definition also permits a linear map with nontrivial fibers without accidentally conditioning on nonzero vectors.
```
def subspaceLaw (ι : K →ₗ[F2] V) (v : V) : ℝ := by
…
```
theorem OAI.UniqueGamesTheorem.Decoder.PositiveMultiplier.subspaceLaw_nonneg line 564
theorem OAI.UniqueGamesTheorem.Decoder.PositiveMultiplier.subspaceLaw_sum line 573
theorem OAI.UniqueGamesTheorem.Decoder.PositiveMultiplier.subspaceLaw_normalized line 583
theorem OAI.UniqueGamesTheorem.Decoder.PositiveMultiplier.subspaceLaw_eigenvalue line 588
theorem OAI.UniqueGamesTheorem.Decoder.PositiveMultiplier.subspaceLaw_eigenvalue_lower line 615
theorem OAI.UniqueGamesTheorem.Decoder.PositiveMultiplier.matrix_spectral_comparison line 633
def OAI.UniqueGamesTheorem.Decoder.PrivateFourier.sign line 676
Source documentation
A real-valued binary character, with the uniform Fourier normalization.
```
def sign (a : F2) : ℝ := (binarySign a).re
```
theorem OAI.UniqueGamesTheorem.Decoder.PrivateFourier.sign_zero line 678
theorem OAI.UniqueGamesTheorem.Decoder.PrivateFourier.sign_one line 679
theorem OAI.UniqueGamesTheorem.Decoder.PrivateFourier.sign_sq line 681
theorem OAI.UniqueGamesTheorem.Decoder.PrivateFourier.sign_abs line 684
theorem OAI.UniqueGamesTheorem.Decoder.PrivateFourier.sign_add line 687
theorem OAI.UniqueGamesTheorem.Decoder.PrivateFourier.sign_add_one line 690
theorem OAI.UniqueGamesTheorem.Decoder.PrivateFourier.binary_neg_eq_self line 701
theorem OAI.UniqueGamesTheorem.Decoder.PrivateFourier.binary_add_eq_zero_iff line 707
theorem OAI.UniqueGamesTheorem.Decoder.PrivateFourier.average_sign_dual line 710
theorem OAI.UniqueGamesTheorem.Decoder.PrivateFourier.average_sign_primal line 716
theorem OAI.UniqueGamesTheorem.Decoder.PrivateFourier.average_sign_equality line 723
Source documentation
Exact character expansion of equality in the actual output space.
```
theorem average_sign_equality [Fintype (K →ₗ[F2] F2)] (x y : K) :
    (𝔼 σ : K →ₗ[F2] F2, sign (σ x) * sign (σ y)) =
      if x = y then 1 else 0 := by
…
```
Mentions: OAI.UniqueGamesTheorem.Decoder.PrivateFourier.sign
theorem OAI.UniqueGamesTheorem.Decoder.PrivateFourier.trivial_restriction_probability line 732
Source documentation
The ambient uniform character has trivial restriction to H with exactly the reciprocal cardinality of H. No conditioning on the private character is substituted for the real experiment.
```
theorem trivial_restriction_probability [Fintype H] [Fintype (K →ₗ[F2] F2)]
    (ι : H →ₗ[F2] K) (hι : Function.Injective ι) :
    (𝔼 σ : K →ₗ[F2] F2, if σ.comp ι = 0 then (1 : ℝ) else 0) =
      1 / (Fintype.card H : ℝ) := by
…
```
theorem OAI.UniqueGamesTheorem.Decoder.PrivateFourier.trivial_restriction_probability_pow line 753
def OAI.UniqueGamesTheorem.Decoder.PrivateFourier.tableSign line 776
Source documentation
The private sign function, formed from the table on one visible row fiber.
```
def tableSign (F : (E →ₗ[F2] H) → K) (σ : K →ₗ[F2] F2)
    (N : E →ₗ[F2] H) : ℝ := sign (σ (F N))
```
Mentions: OAI.UniqueGamesTheorem.Decoder.PrivateFourier.sign
def OAI.UniqueGamesTheorem.Decoder.PrivateFourier.frequencyWeight line 780
Source documentation
The actual probability assigned to a reverse-map frequency.
```
def frequencyWeight (f : (E →ₗ[F2] H) → ℝ) (Φ : H →ₗ[F2] E) : ℝ :=
…
```
theorem OAI.UniqueGamesTheorem.Decoder.PrivateFourier.frequencyWeight_nonneg line 784
theorem OAI.UniqueGamesTheorem.Decoder.PrivateFourier.tableSign_frequencyWeight_sum line 788
Source documentation
Squared Fourier coefficients of the private sign form a probability law.
```
theorem tableSign_frequencyWeight_sum (F : (E →ₗ[F2] H) → K)
    (σ : K →ₗ[F2] F2) :
    ∑ Φ : H →ₗ[F2] E, frequencyWeight (tableSign F σ) Φ = 1 := by
…
```
Mentions: OAI.UniqueGamesTheorem.Decoder.PrivateFourier.frequencyWeight, OAI.UniqueGamesTheorem.Decoder.PrivateFourier.tableSign
theorem OAI.UniqueGamesTheorem.Decoder.PrivateFourier.tableSign_antifold line 796

theorem OAI.UniqueGamesTheorem.Decoder.PrivateFourier.linearCoeff_translate line 806

Source documentation

Translation of the input multiplies a coefficient by its character.

theorem linearCoeff_translate (f : (E →ₗ[F2] H) → ℝ)
    (D : E →ₗ[F2] H) (Φ : H →ₗ[F2] E) :
    linearCoeff (fun N => f (N + D)) Φ =
      linearCoeff f Φ * (linearTraceCharacter Φ D).re := by
…

theorem OAI.UniqueGamesTheorem.Decoder.PrivateFourier.positive_frequency_first_bit line 823
Source documentation
Anti-folding forces every positive-mass frequency to return first bit one.
```
theorem positive_frequency_first_bit (f : (E →ₗ[F2] H) → ℝ)
    (τ : E →ₗ[F2] F2) (h : H) (Φ : H →ₗ[F2] E)
    (folded : ∀ N, f (N + τ.smulRight h) = -f N)
    (positive : 0 < frequencyWeight f Φ) : τ (Φ h) = 1 := by
…
```
Mentions: OAI.UniqueGamesTheorem.Decoder.PrivateFourier.frequencyWeight
def OAI.UniqueGamesTheorem.Decoder.PrivateFourier.frequencyCoset line 857
Source documentation
Frequencies in the affine target's annihilator coset. With q = Q.mkQ, this is exactly θ + Hom(H,Q) in the ambient reverse-map space.
```
def frequencyCoset (q : E →ₗ[F2] V) (θ : H →ₗ[F2] E) :
    Finset (H →ₗ[F2] E) := Finset.univ.filter fun Φ => q.comp (Φ + θ) = 0
```
def OAI.UniqueGamesTheorem.Decoder.PrivateFourier.sliceCorrelation line 862
Source documentation
Correlation on a genuine affine slice. N₀ is retained: its phase cannot be discarded when the witness has a nonzero affine intercept.
```
def sliceCorrelation (q : E →ₗ[F2] V) (N₀ : E →ₗ[F2] H)
    (f : (E →ₗ[F2] H) → ℝ) (θ : H →ₗ[F2] E) : ℝ :=
…
```
theorem OAI.UniqueGamesTheorem.Decoder.PrivateFourier.traceCharacter_re_mul line 869
theorem OAI.UniqueGamesTheorem.Decoder.PrivateFourier.sliceCorrelation_eq_coset line 876
Source documentation
The exact Fourier coset expansion of the affine conditional correlation.
```
theorem sliceCorrelation_eq_coset (q : E →ₗ[F2] V) (N₀ : E →ₗ[F2] H)
    (f : (E →ₗ[F2] H) → ℝ) (θ : H →ₗ[F2] E) :
    sliceCorrelation q N₀ f θ =
      ∑ Φ ∈ frequencyCoset q θ,
        linearCoeff f Φ * (linearTraceCharacter (Φ + θ) N₀).re := by
…
```
Mentions: OAI.UniqueGamesTheorem.Decoder.PrivateFourier.sliceCorrelation, OAI.UniqueGamesTheorem.Decoder.PrivateFourier.frequencyCoset
theorem OAI.UniqueGamesTheorem.Decoder.PrivateFourier.sliceCorrelation_sq_le_coset_mass line 903
Source documentation
Cauchy--Schwarz bounds an affine correlation by the actual Fourier mass in its target coset; no spectral mass is assumed.
```
theorem sliceCorrelation_sq_le_coset_mass (q : E →ₗ[F2] V)
    (N₀ : E →ₗ[F2] H) (f : (E →ₗ[F2] H) → ℝ) (θ : H →ₗ[F2] E) :
    sliceCorrelation q N₀ f θ ^ 2 ≤
      (frequencyCoset q θ).card *
        ∑ Φ ∈ frequencyCoset q θ, frequencyWeight f Φ := by
…
```
Mentions: OAI.UniqueGamesTheorem.Decoder.PrivateFourier.sliceCorrelation, OAI.UniqueGamesTheorem.Decoder.PrivateFourier.frequencyCoset, OAI.UniqueGamesTheorem.Decoder.PrivateFourier.frequencyWeight
theorem OAI.UniqueGamesTheorem.Decoder.PrivateFourier.target_character line 931
Source documentation
The pure-tensor target character is literally evaluation at z.
```
theorem target_character (σ : H →ₗ[F2] F2) (z : E) (N : E →ₗ[F2] H) :
    (linearTraceCharacter (σ.smulRight z) N).re = sign (σ (N z)) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Decoder.PrivateFourier.sign
theorem OAI.UniqueGamesTheorem.Decoder.PrivateFourier.affine_equality_character_expansion line 941
Source documentation
Affine target equality expands into the correlations with the intercept phase sign (σ b). In the projected experiment b = M₀ z + u.
```
theorem affine_equality_character_expansion (q : E →ₗ[F2] V)
    (N₀ : E →ₗ[F2] H) (F : (E →ₗ[F2] H) → K)
    (ι : H →ₗ[F2] K) (z : E) (b : K) :
    (𝔼 A : V →ₗ[F2] H,
      if F (N₀ + A.comp q) = b + ι ((N₀ + A.comp q) z) then (1 : ℝ) else 0) =
      𝔼 σ : K →ₗ[F2] F2, sign (σ b) *
        sliceCorrelation q N₀ (tableSign F σ) ((σ.comp ι).smulRight z) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Decoder.PrivateFourier.sign, OAI.UniqueGamesTheorem.Decoder.PrivateFourier.sliceCorrelation, OAI.UniqueGamesTheorem.Decoder.PrivateFourier.tableSign
theorem OAI.UniqueGamesTheorem.Decoder.PrivateFourier.sliceCorrelation_tableSign_abs_le_one line 971
Source documentation
Every slice correlation has absolute value at most one.
```
theorem sliceCorrelation_tableSign_abs_le_one (q : E →ₗ[F2] V)
    (N₀ : E →ₗ[F2] H) (F : (E →ₗ[F2] H) → K)
    (σ : K →ₗ[F2] F2) (θ : H →ₗ[F2] E) :
    |sliceCorrelation q N₀ (tableSign F σ) θ| ≤ 1 := by
…
```
Mentions: OAI.UniqueGamesTheorem.Decoder.PrivateFourier.sliceCorrelation, OAI.UniqueGamesTheorem.Decoder.PrivateFourier.tableSign

theorem OAI.UniqueGamesTheorem.Decoder.PrivateFourier.agreement_le_average_abs_correlation line 988

Source documentation

Dropping the unit intercept phase can only increase the average absolute correlation; the hypothesis is the actual affine-slice agreement probability.

theorem agreement_le_average_abs_correlation (q : E →ₗ[F2] V)
    (N₀ : E →ₗ[F2] H) (F : (E →ₗ[F2] H) → K)
    (ι : H →ₗ[F2] K) (z : E) (b : K) :
    (𝔼 A : V →ₗ[F2] H,
      if F (N₀ + A.comp q) = b + ι ((N₀ + A.comp q) z) then (1 : ℝ) else 0) ≤
      𝔼 σ : K →ₗ[F2] F2,
        |sliceCorrelation q N₀ (tableSign F σ) ((σ.comp ι).smulRight z)| := by
…

Mentions: OAI.UniqueGamesTheorem.Decoder.PrivateFourier.sliceCorrelation, OAI.UniqueGamesTheorem.Decoder.PrivateFourier.tableSign

theorem OAI.UniqueGamesTheorem.Decoder.PrivateFourier.frequencyCoset_card line 1014
Source documentation
The exact number of frequencies in the affine coset. Translation does not alter the annihilator cardinality, including when the target is nonzero.
```
theorem frequencyCoset_card (Q : Submodule F2 E) [Fintype (H →ₗ[F2] Q)]
    (θ : H →ₗ[F2] E) :
    (frequencyCoset Q.mkQ θ).card =
      2 ^ (Module.finrank F2 H * Module.finrank F2 Q) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Decoder.PrivateFourier.frequencyCoset
theorem OAI.UniqueGamesTheorem.Decoder.PrivateFourier.frequencyCoset_card_le line 1028

theorem OAI.UniqueGamesTheorem.Decoder.PrivateFourier.remove_bad_characters line 1043

Source documentation

Discarding a set of characters costs at most its actual uniform mass.

theorem remove_bad_characters (C : SigmaChar → ℝ) (good : SigmaChar → Prop)
    (a b : ℝ) (hC : ∀ σ, |C σ| ≤ 1)
    (hcorrelation : a ≤ 𝔼 σ, |C σ|)
    (hbad : (𝔼 σ, if good σ then (0 : ℝ) else 1) ≤ b) :
    a - b ≤ 𝔼 σ, if good σ then |C σ| else 0 := by
…

theorem OAI.UniqueGamesTheorem.Decoder.PrivateFourier.average_coset_mass_lower line 1063

Source documentation

The second Cauchy--Schwarz step in private decoding. The first step is sliceCorrelation_sq_le_coset_mass; the mass is the actual sampled Fourier mass and good selects nontrivial output characters.

theorem average_coset_mass_lower (C mass : SigmaChar → ℝ) (good : SigmaChar → Prop)
    (N c : ℝ) (hN : 0 < N) (hc : 0 ≤ c)
    (hcorrelation : c ≤ 𝔼 σ, if good σ then |C σ| else 0)
    (hpoint : ∀ σ, good σ → C σ ^ 2 ≤ N * mass σ) :
    c ^ 2 / N ≤ 𝔼 σ, if good σ then mass σ else 0 := by
…

theorem OAI.UniqueGamesTheorem.Decoder.PrivateFourier.contraction_mem_target_coset line 1093

Source documentation

A frequency in the target coset contracts into z + Q.

theorem contraction_mem_target_coset (Q : Submodule F2 E)
    (σ : H →ₗ[F2] F2) (z : E) (Φ : H →ₗ[F2] E) (h : H)
    (hσ : σ h = 1) (hcoset : Q.mkQ.comp (Φ + σ.smulRight z) = 0) :
    Φ h - z ∈ Q := by
…

theorem OAI.UniqueGamesTheorem.Decoder.PrivateFourier.uniform_preimage_probability line 1119
Source documentation
If the returned projected answer has a preimage in the candidate set, the uniform, independently sampled candidate finds a preimage with this probability.
```
theorem uniform_preimage_probability (s : Finset U) (π : U → O) (b : O)
    (preimage : ∃ u ∈ s, π u = b) :
    1 / (s.card : ℝ) ≤ 𝔼 u ∈ s, if π u = b then (1 : ℝ) else 0 := by
…
```

theorem OAI.UniqueGamesTheorem.Decoder.PrivateFourier.independent_agreement_lower line 1136

Source documentation

An explicit product sampling law: the left strategy samples uniformly from s, independently of the right strategy's private sample. Only positive-mass good samples need a preimage; no private Fourier information is passed left.

theorem independent_agreement_lower (s : Finset U) (π : U → O)
    (answer : Ω → O) (weight : Ω → ℝ) (good : Ω → Prop)
    (hweight : ∀ ω, 0 ≤ weight ω)
    (preimage : ∀ ω, good ω → 0 < weight ω → ∃ u ∈ s, π u = answer ω) :
    (∑ ω, if good ω then weight ω else 0) / (s.card : ℝ) ≤
      ∑ ω, weight ω * (𝔼 u ∈ s, if π u = answer ω then (1 : ℝ) else 0) := by
…