OAI/Analysis/FreeWords/UnitaryFiniteSpectrum.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KKSpectralSupport.complexPhase line 29
2. theorem OAI.KKSpectralSupport.complexPhase_norm line 31
3. theorem OAI.KKSpectralSupport.complexPhase_dist line 37
4. theorem OAI.KKSpectralSupport.projection_norm_one line 47
5. theorem OAI.KKSpectralSupport.partition_weight_mul line 54
6. theorem OAI.KKSpectralSupport.phase_partition_unitary line 64
7. theorem OAI.KKSpectralSupport.partition_phase_error line 79
8. theorem OAI.KKSpectralSupport.unitary_finite_spectrum_approximation line 118