OAI/Analysis/SymmetricDomains/InterpolateRealUpper.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Release061.SignElimination.realPartPolynomial line 35
2. lemma OAI.Release061.SignElimination.realPartPolynomial_coeff line 38
3. lemma OAI.Release061.SignElimination.realPartPolynomial_degree_lt line 41
4. lemma OAI.Release061.SignElimination.realPartPolynomial_map line 47
5. theorem OAI.Release061.SignElimination.real_interpolation line 54
6. theorem OAI.Release061.SignElimination.real_interpolation_indexed line 75
7. def OAI.Release061.SignElimination.realComplexNodes line 99
8. def OAI.Release061.SignElimination.conjugateSwap line 102
9. lemma OAI.Release061.SignElimination.realComplexNodes_conj line 105
10. lemma OAI.Release061.SignElimination.realComplexNodes_injective line 111
11. theorem OAI.Release061.SignElimination.interpolate_real_and_upper line 147