OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumForkListInitialWeights.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The first odd subdivision satisfies the same polynomial envelope as the subsequent fork rounds, with its actual rational coefficients.

  1. theorem OAI.ContinuumCoulomb.QuantumForkList.initialScale_abs_bound line 14
  2. theorem OAI.ContinuumCoulomb.QuantumForkList.initial_coefficientBound line 52