Walsh.lean`

28 declarations, 0 contain sorry, 0 declared as axioms

Walsh characters of the Boolean cube

The characters are the real sign monomials, regarded as complex-valued functions. Counting orthogonality proves linear independence; the cardinality comparison then gives a basis. The degree filtration and its dimensions are constructed from this concrete basis.

def OAI.LeanBlast.GotsmanLinial.walshChar line 28
Source documentation
The complex-valued Walsh character associated to a subset of coordinates.
```
def walshChar {n : ℕ} (S : Finset (Fin n)) (x : Cube n) : ℂ :=
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.Cube
theorem OAI.LeanBlast.GotsmanLinial.walshChar_empty line 31
theorem OAI.LeanBlast.GotsmanLinial.walshChar_singleton line 34
theorem OAI.LeanBlast.GotsmanLinial.walshChar_eq_prod_univ line 37
theorem OAI.LeanBlast.GotsmanLinial.star_walshChar line 41
theorem OAI.LeanBlast.GotsmanLinial.walshChar_mul line 45
theorem OAI.LeanBlast.GotsmanLinial.walshChar_mul_self line 54
theorem OAI.LeanBlast.GotsmanLinial.walshChar_univ_mul line 58
theorem OAI.LeanBlast.GotsmanLinial.sum_walshChar line 65
theorem OAI.LeanBlast.GotsmanLinial.walshChar_orthogonality line 82
Source documentation
Orthogonality for the unnormalized counting inner product.
```
theorem walshChar_orthogonality {n : ℕ} (S T : Finset (Fin n)) :
    (∑ x : Cube n, star (walshChar S x) * walshChar T x) =
      if S = T then (2 : ℂ) ^ n else 0 := by
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.Cube, OAI.LeanBlast.GotsmanLinial.walshChar
def OAI.LeanBlast.GotsmanLinial.walshCoefficientLinear line 90
Source documentation
Unnormalized Fourier coefficient as a linear functional.
```
def walshCoefficientLinear {n : ℕ} (S : Finset (Fin n)) :
    (Cube n → ℂ) →ₗ[ℂ] ℂ where
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.Cube
theorem OAI.LeanBlast.GotsmanLinial.walshCoefficientLinear_char line 96
theorem OAI.LeanBlast.GotsmanLinial.walshChar_linearIndependent line 100
theorem OAI.LeanBlast.GotsmanLinial.walsh_index_card line 111
def OAI.LeanBlast.GotsmanLinial.walshBasis line 116
Source documentation
The concrete Walsh basis, indexed by coordinate subsets.
```
def walshBasis (n : ℕ) : Basis (Finset (Fin n)) ℂ (Cube n → ℂ) :=
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.Cube
theorem OAI.LeanBlast.GotsmanLinial.walshBasis_apply line 119
def OAI.LeanBlast.GotsmanLinial.fourierSpace line 124
Source documentation
Functions of Fourier degree at most k.
```
def fourierSpace (n k : ℕ) : Submodule ℂ (Cube n → ℂ) :=
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.Cube
theorem OAI.LeanBlast.GotsmanLinial.fourierSpace_mono line 127
theorem OAI.LeanBlast.GotsmanLinial.fourierSpace_eq_top line 133
def OAI.LeanBlast.GotsmanLinial.fourierEuclideanSpace line 142
Source documentation
Fourier degree filtration in the Hilbert space with counting inner product.
```
def fourierEuclideanSpace (n k : ℕ) : Submodule ℂ (EuclideanSpace ℂ (Cube n)) :=
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.Cube
theorem OAI.LeanBlast.GotsmanLinial.mem_fourierEuclideanSpace line 146
theorem OAI.LeanBlast.GotsmanLinial.fourierEuclideanSpace_mono line 154
theorem OAI.LeanBlast.GotsmanLinial.fourierEuclideanSpace_eq_top line 158
def OAI.LeanBlast.GotsmanLinial.fourierFlag line 166
Source documentation
Shift the degree filtration so that its zeroth member is bottom.
```
def fourierFlag (n : ℕ) : ℕ → Submodule ℂ (EuclideanSpace ℂ (Cube n))
  | 0 => ⊥
  | k + 1 => fourierEuclideanSpace n k
```
Mentions: OAI.LeanBlast.GotsmanLinial.Cube, OAI.LeanBlast.GotsmanLinial.fourierEuclideanSpace
theorem OAI.LeanBlast.GotsmanLinial.fourierFlag_zero line 170
theorem OAI.LeanBlast.GotsmanLinial.fourierFlag_succ line 172
theorem OAI.LeanBlast.GotsmanLinial.fourierFlag_mono line 175
theorem OAI.LeanBlast.GotsmanLinial.fourierFlag_top line 184