OAI/RepresentationTheory/RowColumn/OverlapBound.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RowColumn.Signed.intertwinerMatrix_toCLM line 17
2. lemma OAI.RowColumn.Signed.intertwinerMatrix_trace line 24
3. lemma OAI.RowColumn.Signed.intertwinerMatrix_product_trace line 33
4. lemma OAI.RowColumn.Signed.intertwinerMatrix_filtered line 44
5. def OAI.RowColumn.Signed.lineCost line 75
6. abbrev OAI.RowColumn.Signed.MixtureIndex line 76
7. lemma OAI.RowColumn.Signed.phases_card line 79
8. lemma OAI.RowColumn.Signed.types_card line 82
9. lemma OAI.RowColumn.Signed.mixtureIndex_card line 85
10. lemma OAI.RowColumn.Signed.lineCost_pos line 88
11. theorem OAI.RowColumn.Signed.signed_line_mixture line 92
12. lemma OAI.RowColumn.MatrixState.filtered_trace_mono line 118
13. lemma OAI.RowColumn.MatrixState.trace_filtered_smul_sum line 144
14. lemma OAI.RowColumn.MatrixState.trace_mixture_bound line 158
15. theorem OAI.RowColumn.MatrixState.occupied_commutant_trace line 194

    Source documentation

    Reconstruction of the occupied overlap for the actual signed row/column commutants. The two trace factors retain every prescribed copy.

    theorem occupied_commutant_trace (odd : C → Prop) [DecidablePred odd] (k : ℕ)
        (e : S ↪ L × K) (a₀ : S → C × C)
        (A : Representation.IntertwiningMap (lineRepresentation (odd := odd) (k := k) (fun i => (e i).1))
    …

16. theorem OAI.RowColumn.actual_copy_overlap_bound line 267

    Source documentation

    Actual hook-Specht all-copy overlap, with the concrete polynomial factors before absorption into the one absolute constant. Orthogonality and completeness are used later to bound the copy counts, not silently discarded from the main.

    theorem actual_copy_overlap_bound (board : S ↪ L × R)
        (a : YoungDiagram) (e : S ≃ Cell a) (h : ℕ) (H : InHook a h) (c₀ : HookModel.Color h)
        {u v : ℕ}
        (ρ : Representation ℂ (lineGroup (fun i => (board i).1)) V)
        (τ : Representation ℂ (lineGroup (fun i => (board i).2)) W)
        (hρ : IsUnitary ρ) (hτ : IsUnitary τ)
        (I : Fin u → V →ₗᵢ[ℂ] hilbertSpace a) (J : Fin v → W →ₗᵢ[ℂ] hilbertSpace a)
        (hI : ∀ i, Intertwines (V := V) (W := hilbertSpace a) ρ
    …

    Mentions: OAI.RowColumn.InHook, OAI.RowColumn.HookModel.Color, OAI.RowColumn.lineGroup, OAI.RowColumn.Intertwines