OAI/Computability/QuantumFactoring/DynamicMajorantExpressions.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.OrderTrial.Expressions.dynamicRamp line 14
2. def OAI.ExactQuantumFactoring.OrderTrial.Expressions.dynamicRampLin line 16
3. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.dynamicRamp_correct line 18
4. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.dynamicRampLin_correct line 21
5. def OAI.ExactQuantumFactoring.OrderTrial.Expressions.dynamicSplineRe line 25
6. def OAI.ExactQuantumFactoring.OrderTrial.Expressions.dynamicSplineIm line 28
7. def OAI.ExactQuantumFactoring.OrderTrial.Expressions.dynamicPhaseRe line 31
8. def OAI.ExactQuantumFactoring.OrderTrial.Expressions.dynamicPhaseIm line 33
9. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.dynamicSplineRe_correct line 36
10. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.dynamicSplineIm_correct line 39
11. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.dynamicPhaseRe_correct line 42
12. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.dynamicPhaseIm_correct line 45
13. def OAI.ExactQuantumFactoring.OrderTrial.Expressions.dynamicMassZero line 50
14. def OAI.ExactQuantumFactoring.OrderTrial.Expressions.dynamicMassSlope line 52
15. def OAI.ExactQuantumFactoring.OrderTrial.Expressions.dynamicMassCoeff line 56
16. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.dynamicMassCoeff_correct line 58
17. def OAI.ExactQuantumFactoring.OrderTrial.Expressions.quarter line 68
18. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.quarter_correct line 69
19. def OAI.ExactQuantumFactoring.OrderTrial.Expressions.majorantE line 74

    Source documentation

    Actual constant-depth arithmetic for U, including dynamic quarter selection. No residue loop and no polynomial-valued oracle occurs in this expression.

    def majorantE (Q B d j u : NatExpr v) : RatExpr v :=
    …

    Mentions: OAI.ExactQuantumFactoring.NatExpr, OAI.ExactQuantumFactoring.RatExpr

20. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.majorantE_correct line 80