OAI/Computability/QuantumFactoring/StaticMajorantResources.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.rampPoly_poly line 12
2. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.rampLin_poly line 16
3. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.splineRePoly_poly line 20
4. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.splineImPoly_poly line 27
5. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.phaseRePoly_poly line 35
6. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.phaseImPoly_poly line 42
7. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.massZero_poly line 50
8. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.massSlope_poly line 54
9. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.massCoeff_poly line 58
10. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.low_poly line 62
11. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.high_poly line 66
12. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.pieceSum_poly line 71
13. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.majorantSumE_poly line 82