MatrixFourier.lean`

21 declarations, 0 contain sorry, 0 declared as axioms

Normalized Fourier analysis of finite binary linear-map spaces

The coefficient normalization is uniform expectation on the primal space. The Parseval sum over frequencies is an unnormalized sum. The underlying complex Fourier system is the actual trace-character family on the finite additive group. Completeness is proved directly from character cancellation and finite sums.

def OAI.MaxCutGames.Fourier.MatrixFourier.fourierCoeff line 30
Source documentation
Uniformly normalized complex Fourier coefficient.
```
def fourierCoeff (f : G → ℂ) (ψ : AddChar G ℂ) : ℂ :=
…
```
theorem OAI.MaxCutGames.Fourier.MatrixFourier.fourierCoeff_sum line 33
theorem OAI.MaxCutGames.Fourier.MatrixFourier.fourierCoeff_smul line 39
theorem OAI.MaxCutGames.Fourier.MatrixFourier.star_expect line 45
theorem OAI.MaxCutGames.Fourier.MatrixFourier.star_fourierCoeff line 49
def OAI.MaxCutGames.Fourier.MatrixFourier.linearCoeff line 62
Source documentation
Real coefficient on the actual space of binary linear maps.
```
def linearCoeff (f : (E →ₗ[F2] F) → ℝ) (S : F →ₗ[F2] E) : ℝ :=
…
```
theorem OAI.MaxCutGames.Fourier.MatrixFourier.card_linearMap_reverse line 65
theorem OAI.MaxCutGames.Fourier.MatrixFourier.linearTraceCharacter_star line 87
theorem OAI.MaxCutGames.Fourier.MatrixFourier.linearMap_add_eq_zero_iff line 97

theorem OAI.MaxCutGames.Fourier.MatrixFourier.linear_character_kernel line 107

Source documentation

Exact trace-character orthogonality with the frequency sum unnormalized.

theorem linear_character_kernel (X Y : E →ₗ[F2] F) :
    ∑ S : F →ₗ[F2] E, star (linearTraceCharacter S X) * linearTraceCharacter S Y =
      if X = Y then (Fintype.card (E →ₗ[F2] F) : ℂ) else 0 := by
…

theorem OAI.MaxCutGames.Fourier.MatrixFourier.linear_complexCoeff_character line 125
theorem OAI.MaxCutGames.Fourier.MatrixFourier.linear_complex_inversion line 138
Source documentation
Fourier inversion obtained directly from the finite trace orthogonality sum.
```
theorem linear_complex_inversion (f : (E →ₗ[F2] F) → ℂ) (Y : E →ₗ[F2] F) :
    ∑ S : F →ₗ[F2] E, fourierCoeff f (linearTraceCharacter S) *
      linearTraceCharacter S Y = f Y := by
…
```
Mentions: OAI.MaxCutGames.Fourier.MatrixFourier.fourierCoeff
theorem OAI.MaxCutGames.Fourier.MatrixFourier.linear_complex_parseval line 150
Source documentation
Mixed Parseval with normalized primal expectation and unnormalized frequency sum.
```
theorem linear_complex_parseval (f g : (E →ₗ[F2] F) → ℂ) :
    ∑ S : F →ₗ[F2] E, star (fourierCoeff f (linearTraceCharacter S)) *
      fourierCoeff g (linearTraceCharacter S) = 𝔼 X, star (f X) * g X := by
…
```
Mentions: OAI.MaxCutGames.Fourier.MatrixFourier.fourierCoeff
theorem OAI.MaxCutGames.Fourier.MatrixFourier.complex_ofReal_expect line 168
theorem OAI.MaxCutGames.Fourier.MatrixFourier.linearCoeff_complex line 175
theorem OAI.MaxCutGames.Fourier.MatrixFourier.linear_parseval_inner line 184
Source documentation
Parseval for real functions and the real binary trace coefficients.
```
theorem linear_parseval_inner (f g : (E →ₗ[F2] F) → ℝ) :
    ∑ S : F →ₗ[F2] E, linearCoeff f S * linearCoeff g S =
      𝔼 X, f X * g X := by
…
```
Mentions: OAI.MaxCutGames.Fourier.MatrixFourier.linearCoeff
theorem OAI.MaxCutGames.Fourier.MatrixFourier.linear_parseval line 204
theorem OAI.MaxCutGames.Fourier.MatrixFourier.linear_fourier_inversion line 208
theorem OAI.MaxCutGames.Fourier.MatrixFourier.linearCoeff_sum line 226
theorem OAI.MaxCutGames.Fourier.MatrixFourier.linearCoeff_smul line 233
theorem OAI.MaxCutGames.Fourier.MatrixFourier.linearCoeff_character line 239