OAI/Computability/QuantumFactoring/MajorantTemplateEmission.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.linearPolyE line 18
  2. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.integralZeroE line 20
  3. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.integralSlopeE line 24
  4. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.massZeroE line 29
  5. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.massSlopeE line 33
  6. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.massCoeffE line 37
  7. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.roundedE line 40
  8. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.roundingDenE line 42
  9. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.lowE line 44
  10. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.highE line 46
  11. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.pieceSumE line 48
  12. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.majorantSumExpr line 54
  13. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.dynamicRampE line 57
  14. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.dynamicRampLinE line 59
  15. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.dynamicSplineReE line 61
  16. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.dynamicSplineImE line 64
  17. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.dynamicPhaseReE line 67
  18. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.dynamicPhaseImE line 70
  19. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.dynamicMassZeroE line 73
  20. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.dynamicMassSlopeE line 76
  21. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.dynamicMassCoeffE line 81
  22. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.quarterE line 85
  23. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.majorantExpr line 86