OAI/Analysis/FreeWords/FiniteSpectrum.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.KKSpectralSupport.spectralBand_mul_cutline 28 - theorem
OAI.KKSpectralSupport.spectralBand_orthogonalline 34 - theorem
OAI.KKSpectralSupport.partition_error_boundline 40 - theorem
OAI.KKSpectralSupport.finite_spectrum_approximation_centralline 68 - theorem
OAI.KKSpectralSupport.finite_spectrum_approximationline 111