OAI/MathematicalPhysics/Heisenberg/StableSections.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Heisenberg.Pin.biaffine line 14
2. def OAI.Heisenberg.Pin.StableSection line 16
3. def OAI.Heisenberg.Pin.rootCriterion line 19
4. lemma OAI.Heisenberg.Pin.quotient_im line 22
5. lemma OAI.Heisenberg.Pin.section_swap line 28
6. lemma OAI.Heisenberg.Pin.rootCriterion_nonneg line 37
7. lemma OAI.Heisenberg.Pin.symmetrization_identity line 53
8. lemma OAI.Heisenberg.Pin.criterion_ne_zero line 64
9. theorem OAI.Heisenberg.Pin.partial_symmetrization line 81
10. def OAI.Heisenberg.Pin.subsetMonomial line 108
11. lemma OAI.Heisenberg.Pin.subsetMonomial_empty line 111
12. lemma OAI.Heisenberg.Pin.subsetMonomial_insert line 115
13. lemma OAI.Heisenberg.Pin.pderiv_subsetMonomial line 120
14. def OAI.Heisenberg.Pin.presence line 138
15. def OAI.Heisenberg.Pin.presencePolynomial line 141
16. lemma OAI.Heisenberg.Pin.eval_presencePolynomial_one line 144
17. lemma OAI.Heisenberg.Pin.pderiv_presencePolynomial line 148
18. lemma OAI.Heisenberg.Pin.presence_nonneg line 168
19. lemma OAI.Heisenberg.Pin.presence_polynomial_ne_zero line 173
20. theorem OAI.Heisenberg.Pin.stable_presencePolynomial line 180
21. def OAI.Heisenberg.Pin.boundarySection line 193
22. lemma OAI.Heisenberg.Pin.eval_boundarySection line 198
23. theorem OAI.Heisenberg.Pin.stable_boundarySection line 209
24. lemma OAI.Heisenberg.Pin.stable_section_real_rayleigh line 241