CoordinateDegree.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Coordinate multiplication raises the Fourier degree by at most one

The unweighted polynomial degree bound is transported to the actual diagonal matrices and continuous linear operators on the counting-inner-product Euclidean space, including the shifted flag used by the weighted grading construction.

theorem OAI.LeanBlast.GotsmanLinial.coordinateSignMatrix_mem_fourierSpace line 24
Source documentation
The actual coordinate-sign matrix raises the unweighted degree by at most one.
```
theorem coordinateSignMatrix_mem_fourierSpace (i : Fin n) {a : Cube n → ℂ}
    (ha : a ∈ fourierSpace n k) :
    coordinateSignMatrix i *ᵥ a ∈ fourierSpace n (k + 1) := by
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.Cube, OAI.LeanBlast.GotsmanLinial.fourierSpace, OAI.LeanBlast.GotsmanLinial.coordinateSignMatrix
theorem OAI.LeanBlast.GotsmanLinial.coordinateMultiplier_mem_fourierEuclideanSpace line 31
Source documentation
The continuous coordinate multiplier has the same degree shift in Euclidean space.
```
theorem coordinateMultiplier_mem_fourierEuclideanSpace (i : Fin n)
    {a : EuclideanSpace ℂ (Cube n)} (ha : a ∈ fourierEuclideanSpace n k) :
    coordinateMultiplier i a ∈ fourierEuclideanSpace n (k + 1) := by
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.Cube, OAI.LeanBlast.GotsmanLinial.fourierEuclideanSpace, OAI.LeanBlast.GotsmanLinial.coordinateMultiplier
theorem OAI.LeanBlast.GotsmanLinial.coordinateMultiplier_map_fourierEuclideanSpace_le line 39
Source documentation
Submodule-map form of the Euclidean coordinate-degree shift.
```
theorem coordinateMultiplier_map_fourierEuclideanSpace_le (i : Fin n) :
    (fourierEuclideanSpace n k).map (coordinateMultiplier i).toLinearMap ≤
      fourierEuclideanSpace n (k + 1) := by
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.fourierEuclideanSpace, OAI.LeanBlast.GotsmanLinial.coordinateMultiplier
theorem OAI.LeanBlast.GotsmanLinial.coordinateMultiplier_fourierFlag_shift line 46
Source documentation
The shifted flag also has a one-step coordinate shift, including its bottom term.
```
theorem coordinateMultiplier_fourierFlag_shift (i : Fin n) :
    ∀ k (a : EuclideanSpace ℂ (Cube n)), a ∈ fourierFlag n k →
      coordinateMultiplier i a ∈ fourierFlag n (k + 1) := by
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.Cube, OAI.LeanBlast.GotsmanLinial.fourierFlag, OAI.LeanBlast.GotsmanLinial.coordinateMultiplier