WalshDimensions.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Dimensions of the Walsh degree filtration, derived from the linear independence of the concrete characters.

theorem OAI.LeanBlast.GotsmanLinial.card_finset_card_le line 21
Source documentation
Count low-degree character indices by partitioning them according to cardinality.
```
theorem card_finset_card_le (n k : ℕ) :
    Fintype.card {S : Finset (Fin n) // S.card ≤ k} =
      ∑ j ∈ Finset.range (k + 1), n.choose j := by
…
```
theorem OAI.LeanBlast.GotsmanLinial.fourierSpace_finrank line 44
Source documentation
The dimension of the degree-k Fourier subspace is the number of indices of cardinality at most k. This formula remains valid beyond the saturated stage.
```
theorem fourierSpace_finrank (n k : ℕ) :
    finrank ℂ (fourierSpace n k) = ∑ j ∈ Finset.range (k + 1), n.choose j := by
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.fourierSpace
theorem OAI.LeanBlast.GotsmanLinial.fourierSpace_finrank_add line 56
Source documentation
Each new degree contributes exactly the next binomial multiplicity.
```
theorem fourierSpace_finrank_add (n k : ℕ) :
    finrank ℂ (fourierSpace n k) + n.choose (k + 1) =
      finrank ℂ (fourierSpace n (k + 1)) := by
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.fourierSpace
theorem OAI.LeanBlast.GotsmanLinial.fourierSpace_finrank_sub line 62
theorem OAI.LeanBlast.GotsmanLinial.fourierSpace_zero_finrank line 68
theorem OAI.LeanBlast.GotsmanLinial.fourierSpace_finrank_of_le line 73
Source documentation
At or above degree n, the Fourier space has the full cube dimension.
```
theorem fourierSpace_finrank_of_le {n k : ℕ} (hnk : n ≤ k) :
    finrank ℂ (fourierSpace n k) = 2 ^ n := by
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.fourierSpace
theorem OAI.LeanBlast.GotsmanLinial.map_fourierSpace_finrank line 79
Source documentation
Arbitrary invertible linear changes of coordinates preserve every Fourier dimension.
```
theorem map_fourierSpace_finrank {E : Type*} [AddCommGroup E] [Module ℂ E]
    (n k : ℕ) (D : (Cube n → ℂ) ≃ₗ[ℂ] E) :
    finrank ℂ ((fourierSpace n k).map D.toLinearMap) =
      ∑ j ∈ Finset.range (k + 1), n.choose j := by
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.Cube, OAI.LeanBlast.GotsmanLinial.fourierSpace
theorem OAI.LeanBlast.GotsmanLinial.fourierEuclideanSpace_finrank line 86
Source documentation
Passing to the counting Euclidean Hilbert space changes no dimensions.
```
theorem fourierEuclideanSpace_finrank (n k : ℕ) :
    finrank ℂ (fourierEuclideanSpace n k) =
      ∑ j ∈ Finset.range (k + 1), n.choose j := by
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.fourierEuclideanSpace
theorem OAI.LeanBlast.GotsmanLinial.fourierFlag_finrank line 92
Source documentation
With the bottom stage inserted, stage k contains exactly degrees below k.
```
theorem fourierFlag_finrank (n k : ℕ) :
    finrank ℂ (fourierFlag n k) = ∑ j ∈ Finset.range k, n.choose j := by
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.fourierFlag
theorem OAI.LeanBlast.GotsmanLinial.fourierFlag_finrank_add line 101
Source documentation
The degree-k layer has the prescribed binomial dimension increment.
```
theorem fourierFlag_finrank_add (n k : ℕ) :
    finrank ℂ (fourierFlag n k) + n.choose k =
      finrank ℂ (fourierFlag n (k + 1)) := by
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.fourierFlag
theorem OAI.LeanBlast.GotsmanLinial.fourierFlag_finrank_sub line 107
theorem OAI.LeanBlast.GotsmanLinial.map_fourierFlag_finrank line 114
Source documentation
Any invertible weight preserves the dimensions of all stages of the Euclidean flag.
```
theorem map_fourierFlag_finrank (n k : ℕ)
    (D : EuclideanSpace ℂ (Cube n) ≃ₗ[ℂ] EuclideanSpace ℂ (Cube n)) :
    finrank ℂ ((fourierFlag n k).map D.toLinearMap) =
      ∑ j ∈ Finset.range k, n.choose j := by
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.Cube, OAI.LeanBlast.GotsmanLinial.fourierFlag

theorem OAI.LeanBlast.GotsmanLinial.map_fourierFlag_finrank_add line 121

Source documentation

In particular, an invertible weight preserves each binomial dimension increment.

theorem map_fourierFlag_finrank_add (n k : ℕ)
    (D : EuclideanSpace ℂ (Cube n) ≃ₗ[ℂ] EuclideanSpace ℂ (Cube n)) :
    finrank ℂ ((fourierFlag n k).map D.toLinearMap) + n.choose k =
      finrank ℂ ((fourierFlag n (k + 1)).map D.toLinearMap) := by
…

Mentions: OAI.LeanBlast.GotsmanLinial.Cube, OAI.LeanBlast.GotsmanLinial.fourierFlag