OAI/Computability/MaxCut/Games/MatrixNoise.lean

GitHub source file

37 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.

  1. theorem OAI.MaxCutGames.Fourier.MatrixNoise.character_average_shift line 27

    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
…
  2. def OAI.MaxCutGames.Fourier.MatrixNoise.dotCharacter line 43

    Source documentation

    The additive character obtained by pairing against a binary vector.

    def dotCharacter {m : Nat} (w : Vector m) : AddChar (Vector m) ℂ where
…
  3. theorem OAI.MaxCutGames.Fourier.MatrixNoise.dotCharacter_apply line 48
  4. theorem OAI.MaxCutGames.Fourier.MatrixNoise.dotCharacter_eq_zero_iff line 51
  5. theorem OAI.MaxCutGames.Fourier.MatrixNoise.average_dotCharacter line 64
  6. theorem OAI.MaxCutGames.Fourier.MatrixNoise.average_rankOne_character line 73

    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
…
  7. def OAI.MaxCutGames.Fourier.MatrixNoise.noiseOperator line 80
  8. def OAI.MaxCutGames.Fourier.MatrixNoise.noiseEigenvalue line 86

    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) : ℝ :=
…
  9. theorem OAI.MaxCutGames.Fourier.MatrixNoise.noiseOperator_character line 91

    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.MaxCutGames.Fourier.MatrixNoise.noiseOperator, OAI.MaxCutGames.Fourier.MatrixNoise.noiseEigenvalue

  10. theorem OAI.MaxCutGames.Fourier.MatrixNoise.noiseEigenvalue_nonneg line 104
  11. theorem OAI.MaxCutGames.Fourier.MatrixNoise.noiseEigenvalue_le_one line 112
  12. def OAI.MaxCutGames.Fourier.MatrixNoise.evaluationCharacter line 127

    Source documentation

    Evaluation of a uniformly chosen linear functional is a binary character.

    def evaluationCharacter (w : E) : AddChar (E →ₗ[F2] F2) ℂ where
…
  13. theorem OAI.MaxCutGames.Fourier.MatrixNoise.evaluationCharacter_apply line 132
  14. theorem OAI.MaxCutGames.Fourier.MatrixNoise.evaluationCharacter_eq_zero_iff line 135
  15. theorem OAI.MaxCutGames.Fourier.MatrixNoise.average_evaluationCharacter line 148
  16. theorem OAI.MaxCutGames.Fourier.MatrixNoise.average_smulRight_character line 158

    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
…
  17. def OAI.MaxCutGames.Fourier.MatrixNoise.linearNoiseOperator line 166
  18. theorem OAI.MaxCutGames.Fourier.MatrixNoise.linearNoiseOperator_sum line 170
  19. theorem OAI.MaxCutGames.Fourier.MatrixNoise.linearNoiseOperator_smul line 179
  20. def OAI.MaxCutGames.Fourier.MatrixNoise.linearNoiseEigenvalue line 191

    Source documentation

    Weighted probability that the dual map annihilates the sampled noise vector.

    def linearNoiseEigenvalue [Fintype F] (weight : F → ℝ) (S : F →ₗ[F2] E) : ℝ :=
…
  21. theorem OAI.MaxCutGames.Fourier.MatrixNoise.linearNoiseOperator_character line 195

    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.MaxCutGames.Fourier.MatrixNoise.linearNoiseOperator, OAI.MaxCutGames.Fourier.MatrixNoise.linearNoiseEigenvalue

  22. theorem OAI.MaxCutGames.Fourier.MatrixNoise.linearNoiseEigenvalue_nonneg line 209
  23. theorem OAI.MaxCutGames.Fourier.MatrixNoise.linearNoiseEigenvalue_le_one line 217
  24. def OAI.MaxCutGames.Fourier.MatrixNoise.linearRealNoiseOperator line 228
  25. theorem OAI.MaxCutGames.Fourier.MatrixNoise.linearRealNoiseOperator_complex line 232
  26. theorem OAI.MaxCutGames.Fourier.MatrixNoise.linearRealNoiseOperator_eq_re line 244
  27. theorem OAI.MaxCutGames.Fourier.MatrixNoise.linearRealNoiseOperator_sum line 251
  28. theorem OAI.MaxCutGames.Fourier.MatrixNoise.linearRealNoiseOperator_smul line 260
  29. theorem OAI.MaxCutGames.Fourier.MatrixNoise.linearRealNoiseOperator_character line 271
  30. theorem OAI.MaxCutGames.Fourier.MatrixNoise.linearRealNoiseOperator_expansion line 286

    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.MaxCutGames.Fourier.MatrixNoise.linearRealNoiseOperator, OAI.MaxCutGames.Fourier.MatrixNoise.linearNoiseEigenvalue

  31. theorem OAI.MaxCutGames.Fourier.MatrixNoise.linearRealNoiseOperator_pairing line 311

    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.MaxCutGames.Fourier.MatrixNoise.linearRealNoiseOperator, OAI.MaxCutGames.Fourier.MatrixNoise.linearNoiseEigenvalue

  32. theorem OAI.MaxCutGames.Fourier.MatrixNoise.linearRealNoiseOperator_selfAdjoint line 332

    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.MaxCutGames.Fourier.MatrixNoise.linearRealNoiseOperator

  33. theorem OAI.MaxCutGames.Fourier.MatrixNoise.linearRealNoiseOperator_coeff line 355

    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.MaxCutGames.Fourier.MatrixNoise.linearRealNoiseOperator, OAI.MaxCutGames.Fourier.MatrixNoise.linearNoiseEigenvalue

  34. theorem OAI.MaxCutGames.Fourier.MatrixNoise.linearRealNoiseOperator_energy line 376

    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.MaxCutGames.Fourier.MatrixNoise.linearRealNoiseOperator, OAI.MaxCutGames.Fourier.MatrixNoise.linearNoiseEigenvalue

  35. theorem OAI.MaxCutGames.Fourier.MatrixNoise.linearRealNoiseOperator_nonneg line 384

    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.MaxCutGames.Fourier.MatrixNoise.linearRealNoiseOperator

  36. theorem OAI.MaxCutGames.Fourier.MatrixNoise.linearRealNoiseOperator_cross_le line 393

    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.MaxCutGames.Fourier.MatrixNoise.linearRealNoiseOperator

  37. theorem OAI.MaxCutGames.Fourier.MatrixNoise.linearNoiseOperator_energy_re line 413

    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.MaxCutGames.Fourier.MatrixNoise.linearNoiseOperator, OAI.MaxCutGames.Fourier.MatrixNoise.linearNoiseEigenvalue