OAI/MathematicalPhysics/ContinuumCoulomb/Nuclei/GaussGrid.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Error accounting for a finite rectangular selection of equal-mass Gauss cells. The constants may vary between cells, retaining spatial decay.

  1. theorem OAI.ContinuumCoulomb.interval_grid_integral line 13
  2. theorem OAI.ContinuumCoulomb.weighted_cubature_error line 23

    Source documentation

    The fourth-order total estimate retains the sum of volume-weighted local fourth derivative bounds, rather than multiplying by the entire box volume.

    theorem weighted_cubature_error {ι : Type*} [Fintype ι] (h rho : ℝ)
    (Q I C : ι → ℝ) (hrho : 0 ≤ rho)
    (herr : ∀ i, |Q i-I i| ≤ C i*h^7) :
    |rho*(∑ i, Q i)-rho*(∑ i, I i)| ≤ rho*h^4*(∑ i, C i*h^3) := by
…