MatrixNoiseLemmas.lean`

74 declarations, 0 contain sorry, 0 declared as axioms

The actual rank-one averaging operator on finite binary matrix spaces. The outer weights describe any finite law for v; the functional ℓ is uniform. Normalization is needed for eigenvalue bounds, not diagonalization.

theorem OAI.UniqueGamesTheorem.Fourier.MatrixNoise.character_average_shift line 33

Source documentation

Uniform subgroup averaging is diagonal on every additive character.

theorem character_average_shift (ψ : AddChar G ℂ) (A : H →+ G) (x : G) :
    (𝔼 h, ψ (x + A h)) =
      (if ψ.compAddMonoidHom A = 0 then (1 : ℂ) else 0) * ψ x := by
…

def OAI.UniqueGamesTheorem.Fourier.MatrixNoise.dotCharacter line 49
Source documentation
The additive character obtained by pairing against a binary vector.
```
def dotCharacter {m : Nat} (w : Vector m) : AddChar (Vector m) ℂ where
…
```
theorem OAI.UniqueGamesTheorem.Fourier.MatrixNoise.dotCharacter_apply line 54
theorem OAI.UniqueGamesTheorem.Fourier.MatrixNoise.dotCharacter_eq_zero_iff line 57
theorem OAI.UniqueGamesTheorem.Fourier.MatrixNoise.average_dotCharacter line 70

theorem OAI.UniqueGamesTheorem.Fourier.MatrixNoise.average_rankOne_character line 79

Source documentation

Uniform linear functionals detect precisely whether S v vanishes.

theorem average_rankOne_character {m n : Nat}
    (S : Matrix (Fin m) (Fin n) F2) (v : Vector n) :
    (𝔼 ℓ : Vector m, traceCharacter S (Matrix.vecMulVec v ℓ)) =
      if S *ᵥ v = 0 then (1 : ℂ) else 0 := by
…

def OAI.UniqueGamesTheorem.Fourier.MatrixNoise.noiseOperator line 86
def OAI.UniqueGamesTheorem.Fourier.MatrixNoise.noiseEigenvalue line 92
Source documentation
The probability of the event S v = 0, with the supplied finite weights.
```
def noiseEigenvalue {m n : Nat} (weight : Vector n → ℝ)
    (S : Matrix (Fin m) (Fin n) F2) : ℝ :=
…
```
theorem OAI.UniqueGamesTheorem.Fourier.MatrixNoise.noiseOperator_character line 97
Source documentation
Equation (5.3), for the actual finite binary matrix operator.
```
theorem noiseOperator_character {m n : Nat} (weight : Vector n → ℝ)
    (S : Matrix (Fin m) (Fin n) F2) (X : Matrix (Fin n) (Fin m) F2) :
    noiseOperator weight (traceCharacter S) X =
      (noiseEigenvalue weight S : ℂ) * traceCharacter S X := by
…
```
Mentions: OAI.UniqueGamesTheorem.Fourier.MatrixNoise.noiseOperator, OAI.UniqueGamesTheorem.Fourier.MatrixNoise.noiseEigenvalue
theorem OAI.UniqueGamesTheorem.Fourier.MatrixNoise.noiseEigenvalue_nonneg line 110
theorem OAI.UniqueGamesTheorem.Fourier.MatrixNoise.noiseEigenvalue_le_one line 118
def OAI.UniqueGamesTheorem.Fourier.MatrixNoise.evaluationCharacter line 135
Source documentation
Evaluation of a uniformly chosen linear functional is a binary character.
```
def evaluationCharacter (w : E) : AddChar (E →ₗ[F2] F2) ℂ where
…
```
theorem OAI.UniqueGamesTheorem.Fourier.MatrixNoise.evaluationCharacter_apply line 140
theorem OAI.UniqueGamesTheorem.Fourier.MatrixNoise.evaluationCharacter_eq_zero_iff line 143
theorem OAI.UniqueGamesTheorem.Fourier.MatrixNoise.average_evaluationCharacter line 156

theorem OAI.UniqueGamesTheorem.Fourier.MatrixNoise.average_smulRight_character line 166

Source documentation

Basis-independent uniform-functional cancellation in Lemma 5.1.

theorem average_smulRight_character [FiniteDimensional F2 F]
    [Fintype (E →ₗ[F2] F2)] (S : F →ₗ[F2] E) (v : F) :
    (𝔼 ℓ : E →ₗ[F2] F2, linearTraceCharacter S (ℓ.smulRight v)) =
      if S v = 0 then (1 : ℂ) else 0 := by
…

def OAI.UniqueGamesTheorem.Fourier.MatrixNoise.linearNoiseOperator line 174
theorem OAI.UniqueGamesTheorem.Fourier.MatrixNoise.linearNoiseOperator_sum line 178
theorem OAI.UniqueGamesTheorem.Fourier.MatrixNoise.linearNoiseOperator_smul line 187
def OAI.UniqueGamesTheorem.Fourier.MatrixNoise.linearNoiseEigenvalue line 199
Source documentation
Weighted probability that the dual map annihilates the sampled noise vector.
```
def linearNoiseEigenvalue [Fintype F] (weight : F → ℝ) (S : F →ₗ[F2] E) : ℝ :=
…
```

theorem OAI.UniqueGamesTheorem.Fourier.MatrixNoise.linearNoiseOperator_character line 203

Source documentation

Equation (5.3), without a choice of bases.

theorem linearNoiseOperator_character [FiniteDimensional F2 F]
    [Fintype F] [Fintype (E →ₗ[F2] F2)] (weight : F → ℝ)
    (S : F →ₗ[F2] E) (X : E →ₗ[F2] F) :
    linearNoiseOperator weight (linearTraceCharacter S) X =
      (linearNoiseEigenvalue weight S : ℂ) * linearTraceCharacter S X := by
…

Mentions: OAI.UniqueGamesTheorem.Fourier.MatrixNoise.linearNoiseOperator, OAI.UniqueGamesTheorem.Fourier.MatrixNoise.linearNoiseEigenvalue

theorem OAI.UniqueGamesTheorem.Fourier.MatrixNoise.linearNoiseEigenvalue_nonneg line 217
theorem OAI.UniqueGamesTheorem.Fourier.MatrixNoise.linearNoiseEigenvalue_le_one line 225
def OAI.UniqueGamesTheorem.Fourier.MatrixNoise.linearRealNoiseOperator line 236
theorem OAI.UniqueGamesTheorem.Fourier.MatrixNoise.linearRealNoiseOperator_complex line 240
theorem OAI.UniqueGamesTheorem.Fourier.MatrixNoise.linearRealNoiseOperator_eq_re line 252
theorem OAI.UniqueGamesTheorem.Fourier.MatrixNoise.linearRealNoiseOperator_sum line 259
theorem OAI.UniqueGamesTheorem.Fourier.MatrixNoise.linearRealNoiseOperator_smul line 268
theorem OAI.UniqueGamesTheorem.Fourier.MatrixNoise.linearRealNoiseOperator_character line 279
theorem OAI.UniqueGamesTheorem.Fourier.MatrixNoise.linearRealNoiseOperator_expansion line 294
Source documentation
Fourier expansion of the actual noise operator on every real function.
```
theorem linearRealNoiseOperator_expansion (weight : F → ℝ)
    (f : (E →ₗ[F2] F) → ℝ) (X : E →ₗ[F2] F) :
    linearRealNoiseOperator weight f X =
      ∑ S : F →ₗ[F2] E, linearNoiseEigenvalue weight S * linearCoeff f S *
        (linearTraceCharacter S X).re := by
…
```
Mentions: OAI.UniqueGamesTheorem.Fourier.MatrixNoise.linearRealNoiseOperator, OAI.UniqueGamesTheorem.Fourier.MatrixNoise.linearNoiseEigenvalue
theorem OAI.UniqueGamesTheorem.Fourier.MatrixNoise.linearRealNoiseOperator_pairing line 319
Source documentation
Exact spectral pairing identity for the actual operator.
```
theorem linearRealNoiseOperator_pairing (weight : F → ℝ)
    (f g : (E →ₗ[F2] F) → ℝ) :
    (𝔼 X, f X * linearRealNoiseOperator weight g X) =
      ∑ S : F →ₗ[F2] E,
        linearNoiseEigenvalue weight S * linearCoeff f S * linearCoeff g S := by
…
```
Mentions: OAI.UniqueGamesTheorem.Fourier.MatrixNoise.linearRealNoiseOperator, OAI.UniqueGamesTheorem.Fourier.MatrixNoise.linearNoiseEigenvalue
theorem OAI.UniqueGamesTheorem.Fourier.MatrixNoise.linearRealNoiseOperator_selfAdjoint line 340
Source documentation
The actual real operator is self-adjoint under uniform measure.
```
theorem linearRealNoiseOperator_selfAdjoint (weight : F → ℝ)
    (f g : (E →ₗ[F2] F) → ℝ) :
    (𝔼 X, f X * linearRealNoiseOperator weight g X) =
      𝔼 X, linearRealNoiseOperator weight f X * g X := by
…
```
Mentions: OAI.UniqueGamesTheorem.Fourier.MatrixNoise.linearRealNoiseOperator
theorem OAI.UniqueGamesTheorem.Fourier.MatrixNoise.linearRealNoiseOperator_coeff line 363
Source documentation
The actual noise operator multiplies each Fourier coefficient by its annihilation probability. Uniform outer weights specialize to the kernel-rank multiplier used in Appendix A.
```
theorem linearRealNoiseOperator_coeff (weight : F → ℝ)
    (f : (E →ₗ[F2] F) → ℝ) (S : F →ₗ[F2] E) :
    linearCoeff (linearRealNoiseOperator weight f) S =
      linearNoiseEigenvalue weight S * linearCoeff f S := by
…
```
Mentions: OAI.UniqueGamesTheorem.Fourier.MatrixNoise.linearRealNoiseOperator, OAI.UniqueGamesTheorem.Fourier.MatrixNoise.linearNoiseEigenvalue
theorem OAI.UniqueGamesTheorem.Fourier.MatrixNoise.linearRealNoiseOperator_energy line 384
Source documentation
The actual operator's quadratic form is precisely its weighted Fourier mass.
```
theorem linearRealNoiseOperator_energy (weight : F → ℝ)
    (f : (E →ₗ[F2] F) → ℝ) :
    (𝔼 X, f X * linearRealNoiseOperator weight f X) =
      ∑ S : F →ₗ[F2] E, linearNoiseEigenvalue weight S * linearCoeff f S ^ 2 := by
…
```
Mentions: OAI.UniqueGamesTheorem.Fourier.MatrixNoise.linearRealNoiseOperator, OAI.UniqueGamesTheorem.Fourier.MatrixNoise.linearNoiseEigenvalue
theorem OAI.UniqueGamesTheorem.Fourier.MatrixNoise.linearRealNoiseOperator_nonneg line 392
Source documentation
Nonnegative weights make the actual noise operator positive semidefinite.
```
theorem linearRealNoiseOperator_nonneg (weight : F → ℝ) (hw : ∀ v, 0 ≤ weight v)
    (f : (E →ₗ[F2] F) → ℝ) :
    0 ≤ 𝔼 X, f X * linearRealNoiseOperator weight f X := by
…
```
Mentions: OAI.UniqueGamesTheorem.Fourier.MatrixNoise.linearRealNoiseOperator

theorem OAI.UniqueGamesTheorem.Fourier.MatrixNoise.linearRealNoiseOperator_cross_le line 401

Source documentation

The actual two-side inequality used to select one labeling in §5.1.

theorem linearRealNoiseOperator_cross_le (weight : F → ℝ) (hw : ∀ v, 0 ≤ weight v)
    (f g : (E →ₗ[F2] F) → ℝ) :
    2 * (𝔼 X, f X * linearRealNoiseOperator weight g X) ≤
      (𝔼 X, f X * linearRealNoiseOperator weight f X) +
        (𝔼 X, g X * linearRealNoiseOperator weight g X) := by
…

Mentions: OAI.UniqueGamesTheorem.Fourier.MatrixNoise.linearRealNoiseOperator

theorem OAI.UniqueGamesTheorem.Fourier.MatrixNoise.linearNoiseOperator_energy_re line 421
Source documentation
The complex implementation agrees with the real spectral energy identity.
```
theorem linearNoiseOperator_energy_re (weight : F → ℝ)
    (f : (E →ₗ[F2] F) → ℝ) :
    (𝔼 X, f X * (linearNoiseOperator weight (fun Y => (f Y : ℂ)) X).re) =
      ∑ S : F →ₗ[F2] E, linearNoiseEigenvalue weight S * linearCoeff f S ^ 2 := by
…
```
Mentions: OAI.UniqueGamesTheorem.Fourier.MatrixNoise.linearNoiseOperator, OAI.UniqueGamesTheorem.Fourier.MatrixNoise.linearNoiseEigenvalue

theorem OAI.UniqueGamesTheorem.Fourier.MatrixProducts.linearTraceCharacter_re_add line 451

Source documentation

Multiplication of the real binary trace characters.

theorem linearTraceCharacter_re_add (S T : F →ₗ[F2] E) (X : E →ₗ[F2] F) :
    (linearTraceCharacter (S + T) X).re =
      (linearTraceCharacter S X).re * (linearTraceCharacter T X).re := by
…

theorem OAI.UniqueGamesTheorem.Fourier.MatrixProducts.linearCoeff_mul_character line 461

Source documentation

Multiplication by a trace character translates frequency.

theorem linearCoeff_mul_character (f : (E →ₗ[F2] F) → ℝ)
    (S T : F →ₗ[F2] E) :
    linearCoeff (fun X => f X * (linearTraceCharacter T X).re) S =
      linearCoeff f (S + T) := by
…

theorem OAI.UniqueGamesTheorem.Fourier.MatrixProducts.linearCoeff_mul line 475

Source documentation

Products transform to counting-measure convolution of normalized coefficients.

theorem linearCoeff_mul (f g : (E →ₗ[F2] F) → ℝ) (S : F →ₗ[F2] E) :
    linearCoeff (fun X => f X * g X) S =
      ∑ T : F →ₗ[F2] E, linearCoeff f T * linearCoeff g (S + T) := by
…

def OAI.UniqueGamesTheorem.Fourier.MatrixProducts.coefficientConvolution line 497
Source documentation
Frequency convolution, with counting measure on the frequency space.
```
def coefficientConvolution (f g : (E →ₗ[F2] F) → ℝ) (S : F →ₗ[F2] E) : ℝ :=
…
```
theorem OAI.UniqueGamesTheorem.Fourier.MatrixProducts.expect_fourth_eq_sum_convolution_sq line 501
Source documentation
The actual fourth moment equals the squared coefficient-convolution mass.
```
theorem expect_fourth_eq_sum_convolution_sq (f : (E →ₗ[F2] F) → ℝ) :
    (𝔼 X, f X ^ 4) =
      ∑ S : F →ₗ[F2] E, coefficientConvolution f f S ^ 2 := by
…
```
Mentions: OAI.UniqueGamesTheorem.Fourier.MatrixProducts.coefficientConvolution
def OAI.UniqueGamesTheorem.Appendix.F1Energy.rank line 534
def OAI.UniqueGamesTheorem.Appendix.F1Energy.Good line 536
abbrev OAI.UniqueGamesTheorem.Appendix.F1Energy.BoundedSplit line 539
theorem OAI.UniqueGamesTheorem.Appendix.F1Energy.add_self_cancel line 542
def OAI.UniqueGamesTheorem.Appendix.F1Energy.translate line 545
theorem OAI.UniqueGamesTheorem.Appendix.F1Energy.rank_le_of_rankBelow line 551
theorem OAI.UniqueGamesTheorem.Appendix.F1Energy.boundedSplit_rank line 555
theorem OAI.UniqueGamesTheorem.Appendix.F1Energy.good_of_trivial_intersections line 567
Source documentation
The checked geometric cover supplies exactly the F1 witness condition.
```
theorem good_of_trivial_intersections (X Y : G)
    (hi : (X.range ⊓ Y.range) ⊓ (X+Y).range = ⊥)
    (hk : X.ker ⊔ Y.ker ⊔ (X+Y).ker = ⊤) : Good X Y := by
…
```
Mentions: OAI.UniqueGamesTheorem.Appendix.F1Energy.Good
theorem OAI.UniqueGamesTheorem.Appendix.F1Energy.sum_translate line 601
theorem OAI.UniqueGamesTheorem.Appendix.F1Energy.card_bounded_splits_le line 605
theorem OAI.UniqueGamesTheorem.Appendix.F1Energy.card_predecessors_cast_le line 625
def OAI.UniqueGamesTheorem.Appendix.F1Energy.predecessorCoefficient line 634
def OAI.UniqueGamesTheorem.Appendix.F1Energy.gram line 637
def OAI.UniqueGamesTheorem.Appendix.F1Energy.predecessorEnergy line 640
def OAI.UniqueGamesTheorem.Appendix.F1Energy.goodConvolution line 643
theorem OAI.UniqueGamesTheorem.Appendix.F1Energy.predecessorCoefficient_nonneg line 648
theorem OAI.UniqueGamesTheorem.Appendix.F1Energy.gram_nonneg line 654
theorem OAI.UniqueGamesTheorem.Appendix.F1Energy.predecessorCoefficient_sq line 660
theorem OAI.UniqueGamesTheorem.Appendix.F1Energy.predecessor_energy_eq line 667
theorem OAI.UniqueGamesTheorem.Appendix.F1Energy.predecessor_energy_nonneg line 686
theorem OAI.UniqueGamesTheorem.Appendix.F1Energy.predecessor_energy_le line 690
theorem OAI.UniqueGamesTheorem.Appendix.F1Energy.goodConvolution_nonneg line 702
theorem OAI.UniqueGamesTheorem.Appendix.F1Energy.good_term_le line 710
Source documentation
Each supported good term has a bounded split witness. Its summand is counted with shared residual C=Y+R; all other summands are nonnegative.
```
theorem good_term_le (a : G → ℝ) (d : ℕ)
    (hdegree : ∀ Y, d < rank Y → a Y = 0) (X Y : G) :
    (if Good X Y then |a Y| * |a (X+Y)| else 0) ≤
      ∑ R : BoundedSplit d X,
        predecessorCoefficient a R.val (Y+R.val) *
          predecessorCoefficient a (X+R.val) (Y+R.val) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Appendix.F1Energy.rank, OAI.UniqueGamesTheorem.Appendix.F1Energy.Good, OAI.UniqueGamesTheorem.Appendix.F1Energy.BoundedSplit, OAI.UniqueGamesTheorem.Appendix.F1Energy.predecessorCoefficient
theorem OAI.UniqueGamesTheorem.Appendix.F1Energy.goodConvolution_le_gram line 758
theorem OAI.UniqueGamesTheorem.Appendix.F1Energy.goodConvolution_sq_le line 774
theorem OAI.UniqueGamesTheorem.Appendix.F1Energy.split_gram_energy_le line 796
theorem OAI.UniqueGamesTheorem.Appendix.F1Energy.goodConvolution_energy_le line 813
theorem OAI.UniqueGamesTheorem.Appendix.F1Energy.abs_complement_sum_le line 837
Source documentation
The complement of any bad event covered by Good is bounded without changing the signs of the coefficients in the bad part.
```
theorem abs_complement_sum_le (a : G → ℝ) (X : G) (bad : G → Prop)
    (hcover : ∀ Y, ¬ bad Y → Good X Y) :
    |∑ Y, if bad Y then 0 else a Y * a (X+Y)| ≤ goodConvolution a X := by
…
```
Mentions: OAI.UniqueGamesTheorem.Appendix.F1Energy.Good, OAI.UniqueGamesTheorem.Appendix.F1Energy.goodConvolution
theorem OAI.UniqueGamesTheorem.Appendix.F1Energy.convolution_split_square_le line 852
theorem OAI.UniqueGamesTheorem.Appendix.F1Energy.convolution_energy_le line 873
theorem OAI.UniqueGamesTheorem.Appendix.F1Energy.fourier_goodConvolution_energy_le line 893

theorem OAI.UniqueGamesTheorem.Appendix.F1Energy.fourth_moment_le_good_bad line 901

Source documentation

The actual fourth-moment identity reduced to the remaining signed bad convolution. Its geometric cover is supplied by good_of_trivial_intersections.

theorem fourth_moment_le_good_bad (f : (E →ₗ[F2] F) → ℝ) (d : ℕ)
    (hdegree : ∀ Y : F →ₗ[F2] E, d < rank Y → linearCoeff f Y = 0)
    (bad : (F →ₗ[F2] E) → (F →ₗ[F2] E) → Prop)
    (hcover : ∀ X Y, ¬ bad X Y → Good X Y) :
    (𝔼 X, f X^4) ≤ 2 * ((2:ℝ)^(6*d^2) * (𝔼 X, f X^2)^2) +
      2 * ∑ X, (∑ Y, if bad X Y then linearCoeff f Y * linearCoeff f (X+Y) else 0)^2 := by
…

Mentions: OAI.UniqueGamesTheorem.Appendix.F1Energy.rank, OAI.UniqueGamesTheorem.Appendix.F1Energy.Good