OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumForkListOutputBounds.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A single explicit coefficient envelope for every edge in the actual output, including the retained active-star edges, and for its scalar offset.

  1. theorem OAI.ContinuumCoulomb.QuantumForkList.CoefficientBound.full line 12
  2. def OAI.ContinuumCoulomb.QuantumForkList.outputCoefficient line 21
  3. theorem OAI.ContinuumCoulomb.QuantumForkList.initial_iterate_coefficientBound line 25
  4. theorem OAI.ContinuumCoulomb.QuantumForkList.initial_iterate_full_weight line 52