Sectors.lean`

45 declarations, 0 contain sorry, 0 declared as axioms

def OAI.RowColumn.MatrixState.evenAlgebra line 14
lemma OAI.RowColumn.MatrixState.evenAlgebra_mem line 39
lemma OAI.RowColumn.MatrixState.tensorMatrix_even_support line 43
lemma OAI.RowColumn.MatrixState.oddCount_eq line 50
def OAI.RowColumn.MatrixState.sectorTensor line 55
lemma OAI.RowColumn.MatrixState.sectorTensor_mul line 59
lemma OAI.RowColumn.MatrixState.sectorTensor_star line 81
lemma OAI.RowColumn.MatrixState.sectorTensor_one line 89
def OAI.RowColumn.MatrixState.sectorPowerHom line 94
lemma OAI.RowColumn.Signed.frame_pred_congr line 110
lemma OAI.RowColumn.Signed.oddFrame_parity_congr line 122
lemma OAI.RowColumn.Signed.oddPerm_parity_congr line 129
def OAI.RowColumn.FiniteStarAlgebra.unitarySpan line 155
lemma OAI.RowColumn.FiniteStarAlgebra.unitarySpan_eq_span line 171
lemma OAI.RowColumn.FiniteStarAlgebra.unitarySpan_mem line 185
def OAI.RowColumn.FiniteStarAlgebra.unitarySpanHom line 188
lemma OAI.RowColumn.FiniteStarAlgebra.unitarySpanHom_spans line 196
def OAI.RowColumn.MatrixState.discreteContinuousHom line 212
def OAI.RowColumn.MatrixState.precompFunctionHom line 222
lemma OAI.RowColumn.MatrixState.sum_single_function line 231
lemma OAI.RowColumn.MatrixState.function_unitary line 236

theorem OAI.RowColumn.MatrixState.exists_spectral_phase_family line 247

Source documentation

A genuine finite spectral phase family inside the prescribed closed star algebra. In the application this is the even one-slot matrix algebra.

theorem exists_spectral_phase_family {C : Type*} [Fintype C] [DecidableEq C]
    (M : Matrix C C ℂ) (hM : M.IsHermitian)
    (K : StarSubalgebra ℂ (Matrix C C ℂ)) (hK : IsClosed (K : Set (Matrix C C ℂ)))
    (hMK : M ∈ K) :
    ∃ (d : ℕ) (P : Fin d → Matrix C C ℂ) (z : Fin d → ℂ),
      (∑ i, z i • P i) = M ∧ (∀ i, P i ∈ K) ∧
      ∀ θ : Fin d → ℂ, (∀ i, ‖θ i‖=1) → (∑ i, θ i • P i) ∈ unitary (Matrix C C ℂ) := by
…

lemma OAI.RowColumn.MatrixState.tensorMatrix_linear_combination line 293
def OAI.RowColumn.MatrixState.typeTensor line 303
lemma OAI.RowColumn.MatrixState.tensorMatrix_by_type line 308
def OAI.RowColumn.MatrixState.phaseMatrix line 321
lemma OAI.RowColumn.MatrixState.tensorMatrix_phase line 325
lemma OAI.RowColumn.MatrixState.typeTensor_fourier line 335
theorem OAI.RowColumn.MatrixState.tensorMatrix_mem_phase_span line 353
Source documentation
Every identical tensor of a linear combination of a finite family lies in the span of its finite phase tensors. Applied to an even spectral family, all the spanning tensors are genuine global even unitaries.
```
theorem tensorMatrix_mem_phase_span (P : J → Matrix C C ℂ) (z : J → ℂ) :
    tensorMatrix (fun _ : S => ∑ j, z j • P j) ∈
      Submodule.span ℂ (Set.range fun θ : Phases J (Fintype.card S) =>
        tensorMatrix (fun _ : S => phaseMatrix P θ)) := by
…
```
Mentions: OAI.RowColumn.MatrixState.tensorMatrix, OAI.RowColumn.MatrixState.phaseMatrix
abbrev OAI.RowColumn.MatrixState.Sector line 379
def OAI.RowColumn.MatrixState.sectorUnitary line 381
def OAI.RowColumn.MatrixState.sectorAlgebra line 385
lemma OAI.RowColumn.MatrixState.sectorUnitary_apply line 388
def OAI.RowColumn.MatrixState.tensorRestriction line 392
lemma OAI.RowColumn.MatrixState.tensorRestriction_apply line 400
theorem OAI.RowColumn.MatrixState.sectorTensor_mem_algebra line 406
Source documentation
Identical even positive tensors really belong to the finite algebra of actual global even unitary tensors. This is a proved phase-Fourier identity, not a commutant-duality assumption.
```
theorem sectorTensor_mem_algebra (M : Matrix C C ℂ) (hM : M.IsHermitian) (heven : M ∈ evenAlgebra odd) :
    (Matrix.toEuclideanCLM (n := Words (S := S) odd k) (𝕜 := ℂ)) (sectorTensor odd k (fun _ : S => M)) ∈ sectorAlgebra (S := S) odd k := by
…
```
Mentions: OAI.RowColumn.MatrixState.evenAlgebra, OAI.RowColumn.MatrixState.sectorTensor, OAI.RowColumn.MatrixState.sectorAlgebra
abbrev OAI.RowColumn.MatrixState.GlobalTypes line 440
def OAI.RowColumn.MatrixState.sectorTypeMatrix line 442
lemma OAI.RowColumn.MatrixState.sectorTensor_type_expansion line 447
lemma OAI.RowColumn.MatrixState.sectorAlgebra_le_type_span line 456
theorem OAI.RowColumn.MatrixState.sectorAlgebra_finrank line 471
Source documentation
Polynomial Fourier algebra dimension, counted by joint word types. No representation-theoretic carrier-dimension estimate is assumed.
```
theorem sectorAlgebra_finrank : Module.finrank ℂ (sectorAlgebra (S := S) odd k) ≤
…
```
Mentions: OAI.RowColumn.MatrixState.sectorAlgebra
lemma OAI.RowColumn.MatrixState.sectorTensor_transport line 497
lemma OAI.RowColumn.MatrixState.matrix_wordVector line 503
lemma OAI.RowColumn.MatrixState.tensor_commutes_signed line 509
theorem OAI.RowColumn.MatrixState.sectorAlgebra_commutes line 537
Source documentation
The polynomial-dimensional tensor algebra commutes with the genuine signed permutation representation, with no commutant-duality assumption.
```
theorem sectorAlgebra_commutes (a : sectorAlgebra (S := S) odd k)
…
```
Mentions: OAI.RowColumn.MatrixState.sectorAlgebra