OAI/MathematicalPhysics/ContinuumCoulomb/Nuclei/GaussPositionCell.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The actual eight equal masses on any translated cube, with a fourth-order error bound from the ambient fourth Fréchet derivative.

  1. def OAI.ContinuumCoulomb.cubePoint line 13
  2. def OAI.ContinuumCoulomb.positionCellGauss line 17
  3. def OAI.ContinuumCoulomb.positionCellIntegral line 21
  4. theorem OAI.ContinuumCoulomb.cubePoint_contDiff line 25
  5. theorem OAI.ContinuumCoulomb.fourthDerivWithin_line_bound line 30
  6. theorem OAI.ContinuumCoulomb.cube_axis_fourth_bound line 40
  7. theorem OAI.ContinuumCoulomb.positionCellGauss_error line 50

    Source documentation

    A translated cell incurs at most C*h^7, so summing cell volumes leaves an h^4 global error.

    theorem positionCellGauss_error (f : Position → ℝ) (hf : ContDiff ℝ 4 f)
    (b : Position) {h C : ℝ} (hh : 0 ≤ h) (hC : 0 ≤ C)
    (hD : ∀ x ∈ Set.Icc (-1:ℝ) 1, ∀ y ∈ Set.Icc (-1:ℝ) 1,
      ∀ z ∈ Set.Icc (-1:ℝ) 1,
      ‖iteratedFDeriv ℝ 4 f (cubePoint b (h/2) x y z)‖ ≤ C) :
    |positionCellGauss b h f-positionCellIntegral b h f| ≤ C*h^7 := by
…

    Mentions: OAI.ContinuumCoulomb.Position, OAI.ContinuumCoulomb.cubePoint, OAI.ContinuumCoulomb.positionCellGauss, OAI.ContinuumCoulomb.positionCellIntegral