TensorFilter.lean`

29 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.RowColumn.MatrixState.hsVector_tensor_norm_sq line 16
lemma OAI.RowColumn.MatrixState.sectorTensor_hermitian line 24
lemma OAI.RowColumn.MatrixState.sectorTensor_positive line 33
lemma OAI.RowColumn.MatrixState.sectorTensor_root_square line 38

lemma OAI.RowColumn.MatrixState.sector_unitary_sandwich_bound line 50

Source documentation

The restriction is taken only after factoring the positive weighted Hilbert--Schmidt norm. In particular no diagonal of a nonpositive product is compared to the full trace.

lemma sector_unitary_sandwich_bound (odd : C → Prop) [DecidablePred odd] (k : ℕ)
    (M N : S → Matrix C C ℂ) (U : Matrix C C ℂ)
    (hM : ∀ i, (M i).PosSemidef) (hN : ∀ i, (N i).PosSemidef)
    (heM : ∀ i, M i ∈ evenAlgebra odd) (_ : ∀ i, N i ∈ evenAlgebra odd)
    (heU : U ∈ evenAlgebra odd) :
    ‖hsVector (sectorTensor odd k (fun i => CFC.sqrt (M i)) *
      sectorTensor odd k (fun _ : S => U) *
      sectorTensor odd k (fun i => CFC.sqrt (N i)))‖^2 ≤
        ∏ i, (M i * U * N i * U.conjTranspose).trace.re := by
…

Mentions: OAI.RowColumn.MatrixState.evenAlgebra, OAI.RowColumn.MatrixState.hsVector, OAI.RowColumn.MatrixState.sectorTensor

lemma OAI.RowColumn.MatrixState.algebra_reconstruction_hilbert_bound line 77

Source documentation

Use the intrinsic spectral order on the closed finite C*-algebra. Its physical Hilbert--Schmidt structure and existing operator norm are unchanged.

lemma algebra_reconstruction_hilbert_bound
    {E H G : Type*} [NormedAddCommGroup E] [InnerProductSpace ℂ E]
    [FiniteDimensional ℂ E] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [Group G]
    (A : StarSubalgebra ℂ (E →L[ℂ] E)) (u : G →* unitary A)
    (hspan : Submodule.span ℂ (Set.range fun g : G => (u g : A)) = ⊤)
    (B : A) (F : A →ₗ[ℂ] H) (R : ℝ) (hR : 0 ≤ R)
    (hU : ∀ g, ‖F (u g : A)‖ ≤ R) :
    ‖F B‖ ≤ 4 * (Module.finrank ℂ A : ℝ) * ‖B‖ * R := by
…

def OAI.RowColumn.MatrixState.algebraMatrix line 92
Source documentation
Matrix form of an actual algebra element, with the unchanged physical coordinate basis on the signed tensor sector.
```
def algebraMatrix {I : Type*} [Fintype I] [DecidableEq I]
    (A : StarSubalgebra ℂ (EuclideanSpace ℂ I →L[ℂ] EuclideanSpace ℂ I)) :
    A →ₗ[ℂ] Matrix I I ℂ :=
…
```
def OAI.RowColumn.MatrixState.sandwichMap line 97
lemma OAI.RowColumn.MatrixState.sandwichMap_apply line 102
lemma OAI.RowColumn.MatrixState.sector_unitary_matrix line 107

theorem OAI.RowColumn.MatrixState.whitened_reconstruction_bound line 115

Source documentation

Weighted reconstruction in the actual signed sector, with the exact occupied-board entropy loss and singular quarter-root normalization.

theorem whitened_reconstruction_bound {L K : Type*} [Fintype L] [Fintype K]
    [DecidableEq L] [DecidableEq K] [Nonempty S]
    (odd : C → Prop) [DecidablePred odd] (k : ℕ) (e : S ↪ L × K)
    (M : L → Matrix C C ℂ) (N : K → Matrix C C ℂ)
    (hM : ∀ i, (M i).PosSemidef) (hN : ∀ j, (N j).PosSemidef)
    (heM : ∀ i, M i ∈ evenAlgebra odd) (heN : ∀ j, N j ∈ evenAlgebra odd)
    (hMt : ∀ i, (M i).trace.re ≤ 1) (hNt : ∀ j, (N j).trace.re ≤ 1)
    (B : sectorAlgebra (S := S) odd k) :
…

Mentions: OAI.RowColumn.MatrixState.evenAlgebra, OAI.RowColumn.MatrixState.sectorAlgebra

lemma OAI.RowColumn.MatrixState.filtered_trace_identity line 178
lemma OAI.RowColumn.MatrixState.algebraMatrix_mul line 207
lemma OAI.RowColumn.MatrixState.algebraMatrix_star line 210
lemma OAI.RowColumn.MatrixState.algebraMatrix_hermitian line 213
lemma OAI.RowColumn.MatrixState.algebraMatrix_trace line 217
lemma OAI.RowColumn.MatrixState.tensorMatrix_trace_re line 227
lemma OAI.RowColumn.MatrixState.sectorTensor_trace_le line 236
lemma OAI.RowColumn.MatrixState.sectorTensor_substate_trace line 244
def OAI.RowColumn.MatrixState.positiveTensor line 251
lemma OAI.RowColumn.MatrixState.positiveTensor_matrix line 257
lemma OAI.RowColumn.MatrixState.positiveTensor_isPositive line 263
lemma OAI.RowColumn.MatrixState.positiveTensor_selfAdjoint line 268
lemma OAI.RowColumn.MatrixState.positiveTensor_trace_le_one line 274
lemma OAI.RowColumn.MatrixState.positiveTensor_quarter_four line 280
theorem OAI.RowColumn.MatrixState.quarter_tensor_filter_bound line 296
Source documentation
The actual irreducible-dimension filter acts on fourth powers of both mean-state tensors. Its quarter-root sandwich has squared norm at most 1/d.
```
theorem quarter_tensor_filter_bound (odd : C → Prop) [DecidablePred odd] (k : ℕ)
    (q : sectorAlgebra (S := S) odd k) (hqs : star q=q) (hqq : q*q=q)
…
```
Mentions: OAI.RowColumn.MatrixState.sectorAlgebra
lemma OAI.RowColumn.MatrixState.sector_unwhiten_identity line 316
theorem OAI.RowColumn.MatrixState.sector_filtered_trace_bound line 350
Source documentation
The quantitative global bridge: two arbitrary admissible fibre-product substates, on the actual signed sector and the actual central isotypic filter. No invertibility, sector-surrogate, or postselection bound is assumed.
```
theorem sector_filtered_trace_bound {L K : Type*} [Fintype L] [Fintype K]
    [DecidableEq L] [DecidableEq K] [Nonempty S]
    (odd : C → Prop) [DecidablePred odd] (k : ℕ) (e : S ↪ L × K)
    (q : sectorAlgebra (S := S) odd k) (hqs : star q=q) (hqq : q*q=q)
…
```
Mentions: OAI.RowColumn.MatrixState.sectorAlgebra
theorem OAI.RowColumn.MatrixState.exists_sector_isotypic_filter line 412
Source documentation
The filter used above exists in the concrete tensor algebra, for every actual irreducible that occurs. The identity condition on its isotypic carrier will be applied to the explicit isometric hook embedding.
```
theorem exists_sector_isotypic_filter {V : Type*} [AddCommGroup V]
    [Module ℂ V] [FiniteDimensional ℂ V]
    (odd : C → Prop) [DecidablePred odd] (k : ℕ)
    (ρ : Representation ℂ (Equiv.Perm S) V) [Representation.IsIrreducible ρ] :
    ∃ q : sectorAlgebra (S := S) odd k, star q=q ∧ q*q=q ∧ (∀ a, q*a=a*q) ∧
…
```
Mentions: OAI.RowColumn.MatrixState.sectorAlgebra