OAI/MathematicalPhysics/Heisenberg/StablePolynomials.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Heisenberg.Pin.Upper line 11
2. def OAI.Heisenberg.Pin.Stable line 13
3. lemma OAI.Heisenberg.Pin.isOpen_upper line 16
4. def OAI.Heisenberg.Pin.linePolynomial line 22
5. lemma OAI.Heisenberg.Pin.linePolynomial_eval line 26
6. lemma OAI.Heisenberg.Pin.eval_sum_of_support_subset line 34
7. lemma OAI.Heisenberg.Pin.locallyUniform_const line 42
8. lemma OAI.Heisenberg.Pin.locallyUniform_finset_sum line 49
9. lemma OAI.Heisenberg.Pin.coefficient_limit_locallyUniform line 62
10. theorem OAI.Heisenberg.Pin.stable_coefficient_limit line 78
11. theorem OAI.Heisenberg.Pin.stable_locallyUniform_limit line 114
12. lemma OAI.Heisenberg.Pin.locallyUniform_eval line 150
13. def OAI.Heisenberg.Pin.specialize line 166
14. lemma OAI.Heisenberg.Pin.eval_specialize line 170
15. theorem OAI.Heisenberg.Pin.stable_specialize_real line 183
16. def OAI.Heisenberg.Pin.variablePolynomial line 218
17. lemma OAI.Heisenberg.Pin.variablePolynomial_eval line 222
18. lemma OAI.Heisenberg.Pin.variablePolynomial_pderiv line 233
19. lemma OAI.Heisenberg.Pin.polynomial_logDerivative_im_nonpos line 252
20. lemma OAI.Heisenberg.Pin.stable_add_imaginary_derivative line 277
21. theorem OAI.Heisenberg.Pin.stable_pderiv line 306