OAI/Dynamics/EntropyCounterexample/PolynomialSpectralBound.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem340.PolynomialSpectrum.HasPair line 13
  2. lemma OAI.Problem340.PolynomialSpectrum.hasPair_add line 16
  3. lemma OAI.Problem340.PolynomialSpectrum.hasPair_mul line 27
  4. lemma OAI.Problem340.PolynomialSpectrum.hasPair_algebraMap line 38
  5. lemma OAI.Problem340.PolynomialSpectrum.hasPair_pow line 42
  6. lemma OAI.Problem340.PolynomialSpectrum.hasPair_aeval line 49
  7. lemma OAI.Problem340.PolynomialSpectrum.hasPair_zero line 60
  8. lemma OAI.Problem340.PolynomialSpectrum.aeval_eq_zero_of_hasPair line 85
  9. def OAI.Problem340.PolynomialSpectrum.pairRadii line 91
  10. theorem OAI.Problem340.PolynomialSpectrum.finite_pairRadii_of_annihilator line 97
  11. theorem OAI.Problem340.PolynomialSpectrum.bddAbove_pairRadii_of_annihilator line 110
  12. theorem OAI.Problem340.PolynomialSpectrum.finite_pairRadii line 115
  13. theorem OAI.Problem340.PolynomialSpectrum.bddAbove_pairRadii line 119
  14. theorem OAI.Problem340.PolynomialSpectrum.finite_iUnion_pairRadii_of_annihilator line 122
  15. theorem OAI.Problem340.PolynomialSpectrum.bddAbove_iUnion_pairRadii_of_annihilator line 139
  16. theorem OAI.Problem340.PolynomialSpectrum.pairRadii_subset_zero_one_two_of_cubic line 146
  17. theorem OAI.Problem340.PolynomialSpectrum.pairRadii_le_two_of_cubic line 165
  18. theorem OAI.Problem340.PolynomialSpectrum.pairRadii_comp_subset line 174
  19. theorem OAI.Problem340.PolynomialSpectrum.finite_pairRadii_of_factor line 192
  20. theorem OAI.Problem340.PolynomialSpectrum.bddAbove_pairRadii_of_factor line 197
  21. theorem OAI.Problem340.PolynomialSpectrum.iUnion_pairRadii_comp_subset line 204
  22. theorem OAI.Problem340.PolynomialSpectrum.bddAbove_iUnion_pairRadii_comp line 216