MatrixParityRow.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Fourier expansion of actual affine restrictions and parity extraction.

theorem OAI.UniqueGamesTheorem.Fourier.MatrixParityRow.traceCharacter_comp line 23
theorem OAI.UniqueGamesTheorem.Fourier.MatrixParityRow.traceCharacter_re_add line 28
theorem OAI.UniqueGamesTheorem.Fourier.MatrixParityRow.row_character_average line 40
Source documentation
Characters restricted to the row vanish unless the dual map lands in the kernel of Q. For Q = W.mkQ this is precisely range T ≤ W.
```
theorem row_character_average (Q : E →ₗ[F2] V) (T : C →ₗ[F2] E) :
    (𝔼 A : V →ₗ[F2] C, (linearTraceCharacter T (A.comp Q)).re) =
      if Q.comp T = 0 then 1 else 0 := by
…
```

theorem OAI.UniqueGamesTheorem.Fourier.MatrixParityRow.row_spectral_average line 53

Source documentation

Averaging a finite trace-character expansion on an actual affine row.

theorem row_spectral_average (Q : E →ₗ[F2] V) (X₀ : E →ₗ[F2] C)
    (a : (C →ₗ[F2] E) → ℝ) :
    (𝔼 A : V →ₗ[F2] C, ∑ T : C →ₗ[F2] E,
      a T * (linearTraceCharacter T (X₀ + A.comp Q)).re) =
    ∑ T : C →ₗ[F2] E, if Q.comp T = 0 then
      a T * (linearTraceCharacter T X₀).re else 0 := by
…

theorem OAI.UniqueGamesTheorem.Fourier.MatrixParityRow.row_fourier_average line 67

Source documentation

Equation (5.18), with the primal row parametrized by actual quotient maps.

theorem row_fourier_average (Q : E →ₗ[F2] V) (X₀ : E →ₗ[F2] C)
    (g : (E →ₗ[F2] C) → ℝ) :
    (𝔼 A : V →ₗ[F2] C, g (X₀ + A.comp Q)) =
    ∑ T : C →ₗ[F2] E, if Q.comp T = 0 then
      linearCoeff g T * (linearTraceCharacter T X₀).re else 0 := by
…

theorem OAI.UniqueGamesTheorem.Fourier.MatrixParityRow.shift_character_average line 78

theorem OAI.UniqueGamesTheorem.Fourier.MatrixParityRow.shift_fourier_average line 88

Source documentation

The folding average is the Fourier projection onto parity-zero frequencies.

theorem shift_fourier_average [Fintype C] (τ : E →ₗ[F2] F2)
    (X : E →ₗ[F2] C) (g : (E →ₗ[F2] C) → ℝ) :
    (𝔼 c : C, g (X + τ.smulRight c)) =
    ∑ T : C →ₗ[F2] E, (if τ.comp T = 0 then linearCoeff g T else 0) *
      (linearTraceCharacter T X).re := by
…

theorem OAI.UniqueGamesTheorem.Fourier.MatrixParityRow.row_shift_fourier_average line 108

Source documentation

The parity-zero row subtotal equals the row average of the folded average.

theorem row_shift_fourier_average [Fintype C] (Q : E →ₗ[F2] V)
    (τ : E →ₗ[F2] F2) (X₀ : E →ₗ[F2] C) (g : (E →ₗ[F2] C) → ℝ) :
    (𝔼 A : V →ₗ[F2] C, 𝔼 c : C, g (X₀ + A.comp Q + τ.smulRight c)) =
    ∑ T : C →ₗ[F2] E, if Q.comp T = 0 ∧ τ.comp T = 0 then
      linearCoeff g T * (linearTraceCharacter T X₀).re else 0 := by
…

theorem OAI.UniqueGamesTheorem.Fourier.MatrixParityRow.signed_coefficient_le_abs line 121

theorem OAI.UniqueGamesTheorem.Fourier.MatrixParityRow.coefficient_of_dense_row line 130

Source documentation

Actual coefficient extraction from a dense affine row and a uniformly small folding average. The row frequency count is an explicit finite cardinal bound; the quotient/subspace specialization supplies it by counting maps into W.

theorem coefficient_of_dense_row [Fintype C] (Q : E →ₗ[F2] V)
    (τ : E →ₗ[F2] F2) (X₀ : E →ₗ[F2] C) (g : (E →ₗ[F2] C) → ℝ)
    (ρ : ℝ) (N : Nat) (ρ_pos : 0 < ρ) (N_pos : 0 < N)
    (row_count : (Finset.univ.filter fun T : C →ₗ[F2] E => Q.comp T = 0).card ≤ N)
    (dense : ρ < 𝔼 A : V →ₗ[F2] C, g (X₀ + A.comp Q))
    (shift_bound : ∀ X, (𝔼 c : C, g (X + τ.smulRight c)) ≤ ρ / 2) :
    ∃ T : C →ₗ[F2] E, Q.comp T = 0 ∧ τ.comp T ≠ 0 ∧
      ρ / (2 * (N : ℝ)) < |linearCoeff g T| := by
…

theorem OAI.UniqueGamesTheorem.Fourier.MatrixParityRow.coefficient_of_folded_dense_row line 195

Source documentation

Dense-row extraction for a genuinely folded color map. The zero-parity subtotal bound follows from folding, rather than being supplied as a hypothesis.

theorem coefficient_of_folded_dense_row [Fintype C]
    {D : Type*} [AddCommGroup D] [Module F2 D]
    (Q : E →ₗ[F2] V) (τ : E →ₗ[F2] F2) (X₀ : E →ₗ[F2] C)
    (inclusion : C →ₗ[F2] D) (inclusion_injective : Function.Injective inclusion)
    (F : (E →ₗ[F2] C) → D)
    (folded : ∀ X c, F (X + τ.smulRight c) = F X + inclusion c)
    (y : D) (ρ : ℝ) (N : Nat) (ρ_pos : 0 < ρ) (N_pos : 0 < N)
    (color_bound : 1 / (Fintype.card C : ℝ) ≤ ρ / 2)
    (row_count : (Finset.univ.filter fun T : C →ₗ[F2] E => Q.comp T = 0).card ≤ N)
    (dense : ρ < 𝔼 A : V →ₗ[F2] C, if F (X₀ + A.comp Q) = y then (1 : ℝ) else 0) :
    ∃ T : C →ₗ[F2] E, Q.comp T = 0 ∧ τ.comp T ≠ 0 ∧
      ρ / (2 * (N : ℝ)) < |linearCoeff (fun X => if F X = y then 1 else 0) T| := by
…

lemma OAI.UniqueGamesTheorem.Fourier.MatrixParityRow.color_card_bound line 214
lemma OAI.UniqueGamesTheorem.Fourier.MatrixParityRow.fixed_row_folded line 232

theorem OAI.UniqueGamesTheorem.Fourier.MatrixParityRow.lemma53_quotient line 248

Source documentation

Lemma 5.3 on an actual quotient-parametrized dense row. The density parameter is stated as a ratio of natural powers, avoiding truncated negative exponents.

theorem lemma53_quotient [Fintype C]
    {D : Type*} [AddCommGroup D] [Module F2 D]
    (W : Submodule F2 E)
    [Fintype ((E ⧸ W) →ₗ[F2] C)] [Fintype (C →ₗ[F2] W)]
    (τ : E →ₗ[F2] F2) (X₀ : E →ₗ[F2] C)
    (inclusion : C →ₗ[F2] D) (inclusion_injective : Function.Injective inclusion)
    (F : (E →ₗ[F2] C) → D)
    (folded : ∀ X c, F (X + τ.smulRight c) = F X + inclusion c)
    (y : D) (r s : Nat) (ρ : ℝ)
    (hρ : ρ = 2 / (2 : ℝ) ^ (s - r))
    (hW : Module.finrank F2 W ≤ r)
    (hC : Module.finrank F2 C ≤ s)
…