OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumRawEnvelope.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

A natural polynomial envelope for the actual rational raw compiler. Only the raw term count, coefficient magnitude and unary precision enter it.

  1. def OAI.ContinuumCoulomb.QuantumRawExchange.budgetNat line 11
  2. def OAI.ContinuumCoulomb.QuantumRawExchange.scaleNat line 12
  3. def OAI.ContinuumCoulomb.QuantumRawExchange.outputNat line 13
  4. theorem OAI.ContinuumCoulomb.QuantumRawExchange.mass_nonneg line 17
  5. theorem OAI.ContinuumCoulomb.QuantumRawExchange.mass_bound line 20
  6. theorem OAI.ContinuumCoulomb.QuantumRawExchange.scale_nat_bound line 32
  7. theorem OAI.ContinuumCoulomb.QuantumRawExchange.outputNat_cast line 49
  8. theorem OAI.ContinuumCoulomb.QuantumRawExchange.compile_bond_bound line 54
  9. theorem OAI.ContinuumCoulomb.QuantumRawExchange.compile_scalar_bound line 62