OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumRationalPathStep.lean
8 declarations, 0 contain sorry, 0 declared as axioms
Exact rational graph data for a selected path-subdivision layer.
- structure
OAI.ContinuumCoulomb.QMARationalExchangeGraphline 13 - def
OAI.ContinuumCoulomb.QMARationalExchangeGraph.energyline 27 - def
OAI.ContinuumCoulomb.QMARationalExchangeGraph.pathScaleline 30 - theorem
OAI.ContinuumCoulomb.QMARationalExchangeGraph.pathScale_castline 36 - def
OAI.ContinuumCoulomb.QMARationalExchangeGraph.subdivideline 42 - theorem
OAI.ContinuumCoulomb.QMARationalExchangeGraph.subdivide_matrixline 57 - theorem
OAI.ContinuumCoulomb.QMARationalExchangeGraph.subdivide_energy_errorline 73 - theorem
OAI.ContinuumCoulomb.QMARationalExchangeGraph.subdivide_edge_countline 81