GradingShift.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

A degree shift is tridiagonal in the associated orthogonal grading

These lemmas retain the degree-shift premise explicitly. The cube application discharges it using coordinate multiplication and the weighted Fourier flag.

theorem OAI.LeanBlast.GotsmanLinial.flagProjection_mul_shift_eq_zero line 27

Source documentation

An operator that raises the flag index by at most one has no blocks strictly above the first off-diagonal.

theorem flagProjection_mul_shift_eq_zero
    (K : ℕ → Submodule 𝕜 E) (hK : Monotone K) (Z : E →L[𝕜] E)
    (hshift : ∀ k x, x ∈ K k → Z x ∈ K (k + 1))
    {r s : ℕ} (hrs : r + 1 < s) :
    flagProjection K s * Z * flagProjection K r = 0 := by
…

Mentions: OAI.LeanBlast.GotsmanLinial.flagProjection

theorem OAI.LeanBlast.GotsmanLinial.flagProjection_tridiagonal line 39

Source documentation

Self-adjointness gives the other half of the band by taking adjoints.

theorem flagProjection_tridiagonal
    (K : ℕ → Submodule 𝕜 E) (hK : Monotone K) (Z : E →L[𝕜] E)
    (hZ : IsSelfAdjoint Z)
    (hshift : ∀ k x, x ∈ K k → Z x ∈ K (k + 1))
    {r s : ℕ} (hrs : r + 1 < s ∨ s + 1 < r) :
    flagProjection K s * Z * flagProjection K r = 0 := by
…

Mentions: OAI.LeanBlast.GotsmanLinial.flagProjection

theorem OAI.LeanBlast.GotsmanLinial.map_flagProjection_tridiagonal line 53

Source documentation

The band property is preserved by taking matrices or any other ring representation of the operator algebra.

theorem map_flagProjection_tridiagonal
    {A : Type*} [Ring A] (F : (E →L[𝕜] E) →+* A)
    (K : ℕ → Submodule 𝕜 E) (hK : Monotone K) (Z : E →L[𝕜] E)
    (hZ : IsSelfAdjoint Z)
    (hshift : ∀ k x, x ∈ K k → Z x ∈ K (k + 1))
    {r s : ℕ} (hrs : r + 1 < s ∨ s + 1 < r) :
    F (flagProjection K s) * F Z * F (flagProjection K r) = 0 := by
…

Mentions: OAI.LeanBlast.GotsmanLinial.flagProjection

theorem OAI.LeanBlast.GotsmanLinial.shift_mem_map_of_commute line 64

Source documentation

Commutation transports a degree-shift statement through a weight map.

theorem shift_mem_map_of_commute
    (V : ℕ → Submodule 𝕜 E) (D Z : E →ₗ[𝕜] E)
    (hcommute : ∀ x, Z (D x) = D (Z x))
    (hshift : ∀ k x, x ∈ V k → Z x ∈ V (k + 1))
    (k : ℕ) {x : E} (hx : x ∈ (V k).map D) :
    Z x ∈ (V (k + 1)).map D := by
…

theorem OAI.LeanBlast.GotsmanLinial.operatorMatrix_flagProjection_tridiagonal line 83

Source documentation

The concrete matrix form consumed by the commutator estimate.

theorem operatorMatrix_flagProjection_tridiagonal
    (b : OrthonormalBasis ι ℂ E)
    (K : ℕ → Submodule ℂ E) (hK : Monotone K) (Z : E →L[ℂ] E)
    (hZ : IsSelfAdjoint Z)
    (hshift : ∀ k x, x ∈ K k → Z x ∈ K (k + 1))
    (n : ℕ) (r s : Fin (n + 1))
    (hrs : r.val + 1 < s.val ∨ s.val + 1 < r.val) :
    operatorMatrix b (flagProjection K s.val) * operatorMatrix b Z *
      operatorMatrix b (flagProjection K r.val) = 0 := by
…

Mentions: OAI.LeanBlast.GotsmanLinial.operatorMatrix, OAI.LeanBlast.GotsmanLinial.flagProjection

theorem OAI.LeanBlast.GotsmanLinial.coordinateMultiplier_sqrtWeight_commute line 102
Source documentation
Coordinate signs commute with the actual positive square-root weight.
```
theorem coordinateMultiplier_sqrtWeight_commute
    (w : Cube n → ℝ) (hw : ∀ x, 0 < w x) (i : Fin n)
    (a : EuclideanSpace ℂ (Cube n)) :
    coordinateMultiplier i (sqrtWeightEquiv w hw a) =
      sqrtWeightEquiv w hw (coordinateMultiplier i a) := by
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.Cube, OAI.LeanBlast.GotsmanLinial.coordinateMultiplier, OAI.LeanBlast.GotsmanLinial.sqrtWeightEquiv
theorem OAI.LeanBlast.GotsmanLinial.coordinateMultiplier_weightedFlag_shift line 112
Source documentation
The actual weighted Fourier flag retains the one-step coordinate shift.
```
theorem coordinateMultiplier_weightedFlag_shift
    (w : Cube n → ℝ) (hw : ∀ x, 0 < w x) (i : Fin n) :
    ∀ k (a : EuclideanSpace ℂ (Cube n)),
      a ∈ transportFlag (sqrtWeightEquiv w hw) (fourierFlag n) k →
      coordinateMultiplier i a ∈
        transportFlag (sqrtWeightEquiv w hw) (fourierFlag n) (k + 1) := by
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.Cube, OAI.LeanBlast.GotsmanLinial.transportFlag, OAI.LeanBlast.GotsmanLinial.sqrtWeightEquiv, OAI.LeanBlast.GotsmanLinial.fourierFlag, OAI.LeanBlast.GotsmanLinial.coordinateMultiplier
theorem OAI.LeanBlast.GotsmanLinial.weightedFlag_operatorMatrix_tridiagonal line 126
Source documentation
Tridiagonality for the actually constructed weighted Fourier projections, expressed in an arbitrary orthonormal coordinate system.
```
theorem weightedFlag_operatorMatrix_tridiagonal
    (w : Cube n → ℝ) (hw : ∀ x, 0 < w x)
    (b : OrthonormalBasis (Cube n) ℂ (EuclideanSpace ℂ (Cube n)))
    (i : Fin n) (r s : Fin (n + 1))
    (hrs : r.val + 1 < s.val ∨ s.val + 1 < r.val) :
    flagProjectionMatrix b (transportFlag (sqrtWeightEquiv w hw) (fourierFlag n)) s.val *
      operatorMatrix b (coordinateMultiplier i) *
      flagProjectionMatrix b (transportFlag (sqrtWeightEquiv w hw) (fourierFlag n)) r.val = 0 := by
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.Cube, OAI.LeanBlast.GotsmanLinial.flagProjectionMatrix, OAI.LeanBlast.GotsmanLinial.transportFlag, OAI.LeanBlast.GotsmanLinial.sqrtWeightEquiv, OAI.LeanBlast.GotsmanLinial.fourierFlag, OAI.LeanBlast.GotsmanLinial.operatorMatrix, OAI.LeanBlast.GotsmanLinial.coordinateMultiplier
theorem OAI.LeanBlast.GotsmanLinial.weightedProjectionMatrix_tridiagonal line 142
Source documentation
The raw coordinate-sign matrices are tridiagonal for the actual weighted Fourier projection family. There is no remaining degree-shift hypothesis.
```
theorem weightedProjectionMatrix_tridiagonal
    (w : Cube n → ℝ) (hw : ∀ x, 0 < w x)
    (i : Fin n) (r s : Fin (n + 1))
    (hrs : r.val + 1 < s.val ∨ s.val + 1 < r.val) :
    weightedProjectionMatrix w hw s * coordinateSignMatrix i *
      weightedProjectionMatrix w hw r = 0 := by
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.Cube, OAI.LeanBlast.GotsmanLinial.weightedProjectionMatrix, OAI.LeanBlast.GotsmanLinial.coordinateSignMatrix