OAI/Dynamics/EntropyCounterexample/ExactSequenceSpectrum.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem340.PolynomialSpectrum.intertwines_pow line 17
  2. theorem OAI.Problem340.PolynomialSpectrum.intertwines_aeval line 29
  3. theorem OAI.Problem340.PolynomialSpectrum.aeval_mul_eq_zero_of_exact line 46
  4. theorem OAI.Problem340.PolynomialSpectrum.aeval_pow_eq_zero_of_exact line 62
  5. theorem OAI.Problem340.PolynomialSpectrum.aeval_mul_eq_zero_of_shortComplex_exact line 79
  6. theorem OAI.Problem340.PolynomialSpectrum.finite_pairRadii_of_exact line 98
  7. theorem OAI.Problem340.PolynomialSpectrum.bddAbove_pairRadii_of_exact line 108
  8. theorem OAI.Problem340.PolynomialSpectrum.finite_iUnion_pairRadii_of_exact line 125
  9. theorem OAI.Problem340.PolynomialSpectrum.aeval_eq_zero_of_hasPair_of_pow line 145
  10. theorem OAI.Problem340.PolynomialSpectrum.finite_iUnion_pairRadii_of_pointwise_pow line 155
  11. theorem OAI.Problem340.PolynomialSpectrum.pairRadii_subset_zero_one_two_of_cubic_pow line 173
  12. theorem OAI.Problem340.PolynomialSpectrum.pairRadii_le_two_of_cubic_pow line 192
  13. theorem OAI.Problem340.PolynomialSpectrum.bddAbove_iUnion_pairRadii_of_cubic_pow line 198