OAI/RepresentationTheory/SignedTensor/Overlap.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CoordinateSweeps.TensorBoard.board_trace_le_reindexed line 34
2. lemma OAI.CoordinateSweeps.UnitaryIrrep.projector_commute_lift line 52
3. lemma OAI.CoordinateSweeps.SignedTensor.densityPower_commute_projector line 63
4. lemma OAI.CoordinateSweeps.SignedTensor.even_average_trace line 71
5. abbrev OAI.CoordinateSweeps.SignedTensor.groupOperator line 90
6. def OAI.CoordinateSweeps.SignedTensor.rowProduct line 93
7. def OAI.CoordinateSweeps.SignedTensor.columnProduct line 96
8. theorem OAI.CoordinateSweeps.SignedTensor.board_overlap_regularized line 102

   Source comment

   Literal deleted-board overlap with actual signed tensor action. The two mixture dominations will be obtained by tensoring the local density theorem; the whitening and the full-group dimension loss are constructed here.

   theorem board_overlap_regularized {p l : ℕ} (hp : 0 < p)
       (F : Finset (R × C)) (e : Fin l ≃ F)
       (ρ : UnitaryIrrep (Equiv.Perm (Fin l)))
       (PR : Matrix (Word p l) (Word p l) ℂ) (xC : MonoidAlgebra ℂ (Equiv.Perm (Fin l)))
       (hPR : PR.IsHermitian) (hPR2 : PR*PR=PR)
       (hPC : (groupOperator (p := p) xC).IsHermitian)
   …

   Mentions: OAI.CoordinateSweeps.e, OAI.CoordinateSweeps.UnitaryIrrep, OAI.CoordinateSweeps.SignedTensor.Word, OAI.CoordinateSweeps.SignedTensor.groupOperator

9. theorem OAI.CoordinateSweeps.SignedTensor.board_overlap line 165
10. theorem OAI.CoordinateSweeps.SignedTensor.actual_board_overlap line 200

    Source comment

    Source 06:eq19 for literal row and column subgroup projectors on an arbitrary board with holes. The mixtures and signed regroupings are constructed.

    theorem actual_board_overlap (F : Finset (Fin r × Fin c))
        (e : Fin (Fintype.card F) ≃ F) (s : ℕ) (hp : 0 < p) (hps : p ≤ s)
        (hnR : ∀ i, FiberBlocks.size (fun x : F => x.val.1) i ≤ s)
        (hnC : ∀ j, FiberBlocks.size (fun x : F => x.val.2) j ≤ s)
        (ρR : ∀ i, UnitaryIrrep (Equiv.Perm (Fin (FiberBlocks.size (fun x : F => x.val.1) i))))
        (ρC : ∀ j, UnitaryIrrep (Equiv.Perm (Fin (FiberBlocks.size (fun x : F => x.val.2) j))))
        (ρ : UnitaryIrrep (Equiv.Perm (Fin (Fintype.card F)))) :
        (ρ.dimension : ℝ)*‖fiberProjector (p := p) (fun x : F => x.val.2) e ρC*
    …

    Mentions: OAI.CoordinateSweeps.c, OAI.CoordinateSweeps.e, OAI.CoordinateSweeps.FiberBlocks.size, OAI.CoordinateSweeps.UnitaryIrrep, OAI.CoordinateSweeps.SignedTensor.fiberProjector

11. lemma OAI.CoordinateSweeps.TensorBoard.board_trace_le_labels line 255
12. def OAI.CoordinateSweeps.SignedTensor.labelRowProduct line 283
13. def OAI.CoordinateSweeps.SignedTensor.labelColumnProduct line 286
14. theorem OAI.CoordinateSweeps.SignedTensor.label_board_overlap_regularized line 292

    Source comment

    Literal deleted-board overlap with actual signed tensor action. The two mixture dominations will be obtained by tensoring the local density theorem; the whitening and the full-group dimension loss are constructed here.

    theorem label_board_overlap_regularized {p l : ℕ} (hp : 0 < p)
        (e : Fin l → R × C) (hinj : Function.Injective e)
        (ρ : UnitaryIrrep (Equiv.Perm (Fin l)))
        (PR : Matrix (Word p l) (Word p l) ℂ) (xC : MonoidAlgebra ℂ (Equiv.Perm (Fin l)))
        (hPR : PR.IsHermitian) (hPR2 : PR*PR=PR)
        (hPC : (groupOperator (p := p) xC).IsHermitian)
    …

    Mentions: OAI.CoordinateSweeps.e, OAI.CoordinateSweeps.UnitaryIrrep, OAI.CoordinateSweeps.SignedTensor.Word, OAI.CoordinateSweeps.SignedTensor.groupOperator

15. theorem OAI.CoordinateSweeps.SignedTensor.label_board_overlap line 355
16. theorem OAI.CoordinateSweeps.SignedTensor.actual_label_overlap line 392