OAI/MathematicalPhysics/ContinuumCoulomb/Nuclei/SlabInterior.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Interior horizontal flatness and the full finite-slab approximation.

  1. theorem OAI.ContinuumCoulomb.coulombLine_setIntegral_variation line 13
  2. theorem OAI.ContinuumCoulomb.slabOtherMeasure_mass line 23
  3. theorem OAI.ContinuumCoulomb.slabInteriorSection_integrable line 35
  4. theorem OAI.ContinuumCoulomb.regularizedSlab_coordinate_variation line 47
  5. theorem OAI.ContinuumCoulomb.slabPotential_coordinate_variation line 89
  6. theorem OAI.ContinuumCoulomb.slabPotential_horizontal_variation line 104
  7. theorem OAI.ContinuumCoulomb.slabPotential_interior_error line 127

    Source documentation

    The finite slab approximates the harmonic potential throughout its central horizontal half-box and vertical thickness.

    theorem slabPotential_interior_error {rho H S : ℝ} (hrho : 0 ≤ rho)
    (hH : 0 < H) (hS : 0 ≤ S) (y : Position)
    (hy0 : |y 0| ≤ H/2) (hy1 : |y 1| ≤ H/2) (hy2 : |y 2| ≤ S) :
    |slabPotential rho H S y-slabPotential rho H S 0-2*Real.pi*rho*(y 2)^2| ≤
      64*rho*S*((y 0)^2+(y 1)^2)/H+6*Real.pi*rho*S^3/H := by
…

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