OAI/RepresentationTheory/Unitary/Spectral.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CoordinateSweeps.UnitaryIrrep.projector_trace line 34
2. lemma OAI.CoordinateSweeps.UnitaryIrrep.dimension_le_of_projector_one line 50
3. lemma OAI.CoordinateSweeps.UnitaryIrrep.projector_map line 65
4. abbrev OAI.CoordinateSweeps.SpectralBlock.Level line 77
5. lemma OAI.CoordinateSweeps.SpectralBlock.mul_restrict line 80
6. def OAI.CoordinateSweeps.SpectralBlock.representation line 95
7. lemma OAI.CoordinateSweeps.SpectralBlock.projector_representation line 106
8. lemma OAI.CoordinateSweeps.SpectralBlock.offDiagonal_zero line 114
9. lemma OAI.CoordinateSweeps.SpectralBlock.projector_on_level line 125
10. lemma OAI.CoordinateSweeps.SpectralBlock.level_card_le_trace line 137
11. lemma OAI.CoordinateSweeps.SpectralBlock.dimension_mul_eigenvalue_le_trace line 148

    Source comment

    Positive spectral blocks supported on an actual character projector have at least the actual irreducible dimension. No decomposition is assumed.

    lemma dimension_mul_eigenvalue_le_trace (ρ : UnitaryIrrep Γ) (τ : Γ →* Matrix n n ℂ)
        (r : n → ℝ) (hr : ∀ i, 0 ≤ r i)
        (hτ : ∀ g, τ g * Matrix.diagonal (fun i => (r i : ℂ)) =
          Matrix.diagonal (fun i => (r i : ℂ)) * τ g)
        (hP : ρ.projector τ * Matrix.diagonal (fun i => (r i : ℂ)) = Matrix.diagonal (fun i => (r i : ℂ)))
        (i : n) : (ρ.dimension : ℝ)*r i ≤ ∑ j, r j := by
    …

    Mentions: OAI.CoordinateSweeps.UnitaryIrrep

12. theorem OAI.CoordinateSweeps.UnitaryIrrep.supported_trace_domination line 173

    Source comment

    Source06's dimension-normalized spectral estimate, for every genuine finite group representation. A is supported on the actual central projection.

    theorem supported_trace_domination (ρ : UnitaryIrrep Γ) (τ : Γ →* Matrix n n ℂ)
        (A : Matrix n n ℂ) (hA : A.PosSemidef)
        (hcomm : ∀ g, τ g * A = A * τ g) (hP : ρ.projector τ * A = A) :
        (Matrix.trace A • (1 : Matrix n n ℂ) - (ρ.dimension : ℂ) • A).PosSemidef := by
    …

    Mentions: OAI.CoordinateSweeps.UnitaryIrrep

13. theorem OAI.CoordinateSweeps.UnitaryIrrep.invariant_projector_trace_domination line 209

    Source comment

    Compression of a positive invariant unit-trace operator to any isotypic type is at most inverse irreducible dimension in operator order.

    theorem invariant_projector_trace_domination (ρ : UnitaryIrrep Γ) (τ : Γ →* Matrix n n ℂ)
        (hu : ∀ g, (τ g).conjTranspose=τ g⁻¹) (T : Matrix n n ℂ) (hT : T.PosSemidef)
        (hcomm : ∀ g, τ g*T=T*τ g) :
        (Matrix.trace T • (1 : Matrix n n ℂ) - (ρ.dimension : ℂ) •
          (ρ.projector τ * T * ρ.projector τ)).PosSemidef := by
    …

    Mentions: OAI.CoordinateSweeps.UnitaryIrrep

14. lemma OAI.CoordinateSweeps.Overlap.norm_le_trace line 258
15. lemma OAI.CoordinateSweeps.Overlap.norm_sq_le_trace line 268
16. lemma OAI.CoordinateSweeps.Overlap.projection_product_posSemidef line 274
17. lemma OAI.CoordinateSweeps.Overlap.overlap_norm_sq_le_trace line 280
18. lemma OAI.CoordinateSweeps.Overlap.whitened_projector_domination line 298
19. lemma OAI.CoordinateSweeps.Overlap.trace_mixture_re line 337
20. lemma OAI.CoordinateSweeps.Overlap.trace_smul_re line 343
21. lemma OAI.CoordinateSweeps.Overlap.trace_four_swap line 348
22. theorem OAI.CoordinateSweeps.Overlap.finite_mixture_overlap line 357

    Source comment

    Finite density mixtures plus genuine whitened isotypic domination give the row-column overlap bound, before the harmless epsilon limit.

    theorem finite_mixture_overlap (R Q P : Matrix n n ℂ)
        (hR : R.IsHermitian) (hR2 : R*R=R) (hQ : Q.IsHermitian) (hQ2 : Q*Q=Q)
        (hP : P.IsHermitian) (hP2 : P*P=P) (hPQ : P*Q=Q*P)
        (u : I → ℝ) (v : J → ℝ) (hu : ∀ i, 0 ≤ u i) (hv : ∀ j, 0 ≤ v j)
        (hsu : ∑ i, u i=1) (hsv : ∑ j, v j=1)
        (U : I → Matrix n n ℂ) (V : J → Matrix n n ℂ) (A : I → Matrix n n ℂ)
        (hU : ∀ i, (U i).PosSemidef) (hA : ∀ i, (A i).IsHermitian)
        (cr cc D t E : ℝ) (hcr : 0 ≤ cr) (hcc : 0 ≤ cc) (hD : 0 ≤ D) (ht : 0 ≤ t)
        (hrow : ((cr : ℂ) • (∑ i, (u i : ℂ) • U i)-R).PosSemidef)
        (hcol : ((cc : ℂ) • (∑ j, (v j : ℂ) • V j)-Q).PosSemidef)
        (hwhite : ∀ i, ((t : ℂ) • (A i*Q*A i)-(D : ℂ) • (Q*P)).PosSemidef)
        (hpair : ∀ i j, (Matrix.trace (A i*U i*A i*V j)).re ≤ E) :
    …