OAI/Computability/QuantumFactoring/PolySchemaPoly.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.PolySchemaPoly.coeffs line 11
2. lemma OAI.ExactQuantumFactoring.PolySchemaPoly.C line 13
3. lemma OAI.ExactQuantumFactoring.PolySchemaPoly.X line 15
4. lemma OAI.ExactQuantumFactoring.PolySchemaPoly.constant line 16
5. lemma OAI.ExactQuantumFactoring.PolySchemaPoly.add line 18
6. lemma OAI.ExactQuantumFactoring.PolySchemaPoly.negation line 20
7. lemma OAI.ExactQuantumFactoring.PolySchemaPoly.sub line 22
8. lemma OAI.ExactQuantumFactoring.PolySchemaPoly.mul line 24
9. lemma OAI.ExactQuantumFactoring.PolySchemaPoly.pow line 26
10. lemma OAI.ExactQuantumFactoring.PolySchemaPoly.comp line 30
11. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.dynamicRamp_poly line 54
12. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.dynamicRampLin_poly line 60
13. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.dynamicSplineRe_poly line 66
14. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.dynamicSplineIm_poly line 73
15. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.dynamicPhaseRe_poly line 81
16. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.dynamicPhaseIm_poly line 88
17. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.linearPoly_poly line 96
18. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.integralZero_poly line 100
19. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.integralSlope_poly line 105
20. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.dynamicMassZero_poly line 112
21. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.dynamicMassSlope_poly line 116
22. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.dynamicMassCoeff_poly line 121