OAI/MathematicalPhysics/Heisenberg/PinSymmetrization.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Heisenberg.Pin.pairAssignment line 15
2. lemma OAI.Heisenberg.Pin.prod_pairAssignment line 19
3. lemma OAI.Heisenberg.Pin.ofReal_presence line 30
4. lemma OAI.Heisenberg.Pin.eval_presencePolynomial_pair line 34
5. lemma OAI.Heisenberg.Pin.presence_mono line 54
6. theorem OAI.Heisenberg.Pin.presence_pair_inequality line 66
7. theorem OAI.Heisenberg.Pin.presence_insert_le line 116
8. theorem OAI.Heisenberg.Pin.presence_product line 145
9. lemma OAI.Heisenberg.Pin.product_le_mean_pow line 159
10. theorem OAI.Heisenberg.Pin.presence_mean_bound line 170
11. def OAI.Heisenberg.Pin.MultiAffine line 183
12. lemma OAI.Heisenberg.Pin.prod_pow_update line 185
13. lemma OAI.Heisenberg.Pin.eval_update_affine line 195
14. lemma OAI.Heisenberg.Pin.exists_biaffine_section line 210
15. def OAI.Heisenberg.Pin.symmetrize line 231
16. lemma OAI.Heisenberg.Pin.MultiAffine.add line 236
17. lemma OAI.Heisenberg.Pin.MultiAffine.const_mul line 241
18. lemma OAI.Heisenberg.Pin.MultiAffine.rename line 247
19. lemma OAI.Heisenberg.Pin.MultiAffine.symmetrize line 257
20. theorem OAI.Heisenberg.Pin.stable_symmetrize line 261