OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumOrderedWeightBounds.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Explicit polynomial envelopes for the literal four- and seven-word gadgets. Only the term count, input coefficient bound and unary precision enter these envelopes. No bound on the Hilbert-space dimension is used.

  1. def OAI.ContinuumCoulomb.QuantumOrderedXZ.weightEnvelope line 13
  2. theorem OAI.ContinuumCoulomb.QuantumOrderedXZ.weightEnvelope_nonneg line 16
  3. theorem OAI.ContinuumCoulomb.QuantumOrderedXZ.weightEnvelope_mono line 19
  4. theorem OAI.ContinuumCoulomb.QuantumOrderedXZ.input_square_bound line 25
  5. theorem OAI.ContinuumCoulomb.QuantumOrderedXZ.middle_bound line 30
  6. theorem OAI.ContinuumCoulomb.QuantumOrderedXZ.four_weight_bound line 33
  7. theorem OAI.ContinuumCoulomb.QuantumOrderedXZ.seven_weight_bound line 62
  8. def OAI.ContinuumCoulomb.QuantumOrderedXZ.scaleEnvelope line 107
  9. def OAI.ContinuumCoulomb.QuantumOrderedXZ.stepEnvelope line 110
  10. theorem OAI.ContinuumCoulomb.QuantumOrderedXZ.scaleEnvelope_nonneg line 112
  11. theorem OAI.ContinuumCoulomb.QuantumOrderedXZ.stepEnvelope_nonneg line 115
  12. theorem OAI.ContinuumCoulomb.QuantumOrderedXZ.scale_le_envelope line 120
  13. theorem OAI.ContinuumCoulomb.QuantumOrderedXZ.subdivision_coefficient_bound line 134
  14. theorem OAI.ContinuumCoulomb.QuantumOrderedXZ.third_coefficient_bound line 143
  15. def OAI.ContinuumCoulomb.QuantumOrderedXZ.pipelineBound line 153

    Source documentation

    A fixed fivefold composition of explicit polynomials.

    def pipelineBound (m : ℕ) (B : ℚ) (N : ℕ) : ℕ → ℚ
  | 0 => B
  | k+1 => stepEnvelope (3136*m) (pipelineBound m B N k) N

    Mentions: OAI.ContinuumCoulomb.QuantumOrderedXZ.stepEnvelope

  16. theorem OAI.ContinuumCoulomb.QuantumOrderedXZ.pipelineBound_nonneg line 157
  17. theorem OAI.ContinuumCoulomb.QuantumOrderedXZ.pipeline_coefficient_bound line 163