OAI/MathematicalPhysics/ContinuumCoulomb/Nuclei/SlabMonotonicity.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Coordinatewise monotonicity of the actual singular slab potential. This strengthens centering to comparison at any two absolute coordinates.

  1. theorem OAI.ContinuumCoulomb.coulombLineIntegral_abs_antitone line 13
  2. theorem OAI.ContinuumCoulomb.coulombLine_setIntegral_abs_antitone line 28
  3. theorem OAI.ContinuumCoulomb.regularizedSections_integrable line 38
  4. theorem OAI.ContinuumCoulomb.regularizedSlab_coordinate_antitone line 49
  5. theorem OAI.ContinuumCoulomb.slabPotential_coordinate_monotone line 69

    Source documentation

    Increasing a single absolute coordinate increases the singular slab potential.

    theorem slabPotential_coordinate_monotone {rho H S : ℝ} (hrho : 0 ≤ rho)
    (hH : 0 ≤ H) (hS : 0 ≤ S) (x y : Position) (i : Fin 3)
    (hother : ∀ j : Fin 2, x (i.succAbove j) = y (i.succAbove j))
    (hxy : |x i| ≤ |y i|) : slabPotential rho H S x ≤ slabPotential rho H S y := by
…

    Mentions: OAI.ContinuumCoulomb.Position, OAI.ContinuumCoulomb.slabPotential