OAI/MathematicalPhysics/ContinuumCoulomb/Nuclei/TransportedNodes.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The actual tensor Gauss nodes on a cubic lattice are separated before transport, after transport, and after rational rounding. The enclosing finite set of cells will determine the nucleus count in the final construction.

  1. abbrev OAI.ContinuumCoulomb.GaussLatticeIndex line 15
  2. def OAI.ContinuumCoulomb.gaussLatticePoint line 17
  3. theorem OAI.ContinuumCoulomb.gaussAbscissa_bounds line 20
  4. theorem OAI.ContinuumCoulomb.gaussNode_bounds line 25
  5. theorem OAI.ContinuumCoulomb.gauss_lattice_coordinate_separation line 29
  6. theorem OAI.ContinuumCoulomb.gaussLatticePoint_separation line 58
  7. theorem OAI.ContinuumCoulomb.transportedGauss_rounding_injective line 74

    Source documentation

    The inverse Lipschitz estimate gives a quantitative separation suitable for rational nuclear placement, for any finite selection of cells.

    theorem transportedGauss_rounding_injective {m denominator : ℕ}
    (hdenom : 0 < denominator) {h : ℝ} (hh : 0 < h)
    (index : Fin m → GaussLatticeIndex) (hindex : Function.Injective index)
    (G : Position → Position) {C : ℝ≥0} (hC : 0 < C)
    (hG : AntilipschitzWith C G)
    (hprecision : 6 / (denominator : ℝ) < h / (3 * (C : ℝ))) :
    Function.Injective (fun i => roundPosition denominator (G (gaussLatticePoint h (index i)))) := by
…

    Mentions: OAI.ContinuumCoulomb.GaussLatticeIndex, OAI.ContinuumCoulomb.Position, OAI.ContinuumCoulomb.roundPosition, OAI.ContinuumCoulomb.gaussLatticePoint