OAI/MathematicalPhysics/ContinuumCoulomb/Nuclei/SlabSections.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Finite product sections of the actual rectangular slab measure.

  1. def OAI.ContinuumCoulomb.slabSide line 12
  2. def OAI.ContinuumCoulomb.slabAxisMeasure line 14
  3. def OAI.ContinuumCoulomb.slabProductMeasure line 17
  4. def OAI.ContinuumCoulomb.slabProductDomain line 20
  5. theorem OAI.ContinuumCoulomb.slabProductDomain_preimage line 23
  6. theorem OAI.ContinuumCoulomb.slabProductMeasure_eq line 39
  7. theorem OAI.ContinuumCoulomb.slabProduct_measurePreserving line 44
  8. theorem OAI.ContinuumCoulomb.slabProduct_integral line 53
  9. theorem OAI.ContinuumCoulomb.slabProduct_integrable line 58
  10. theorem OAI.ContinuumCoulomb.regularizedKernel_eq_sqrt line 64
  11. theorem OAI.ContinuumCoulomb.regularizedKernel_section line 70
  12. instance OAI.ContinuumCoulomb.slabAxisMeasure_finite line 83
  13. def OAI.ContinuumCoulomb.zeroPositionCoordinate line 88
  14. theorem OAI.ContinuumCoulomb.zeroPositionCoordinate_same line 91
  15. theorem OAI.ContinuumCoulomb.zeroPositionCoordinate_other line 94
  16. theorem OAI.ContinuumCoulomb.regularizedProduct_integrable line 98
  17. theorem OAI.ContinuumCoulomb.regularizedSection_integrable line 104
  18. theorem OAI.ContinuumCoulomb.regularizedSlab_sectionIntegral line 116
  19. theorem OAI.ContinuumCoulomb.coulombLine_setIntegral_le_center line 130
  20. theorem OAI.ContinuumCoulomb.regularizedSlab_coordinate_max line 142

    Source documentation

    Centering one coordinate increases the attractive Coulomb integral. The statement holds for the actual finite slab, before taking the singular limit.

    theorem regularizedSlab_coordinate_max {epsilon H S : ℝ} (hepsilon : epsilon ≠ 0)
    (hH : 0 ≤ H) (hS : 0 ≤ S) (y : Position) (i : Fin 3) :
    (∫ x in slabDomain H S, NeutralAtom.regularizedKernel epsilon (y-x)) ≤
      ∫ x in slabDomain H S, NeutralAtom.regularizedKernel epsilon
        (zeroPositionCoordinate i y-x) := by
…

    Mentions: OAI.ContinuumCoulomb.Position, OAI.ContinuumCoulomb.slabDomain, OAI.NeutralAtom.regularizedKernel, OAI.ContinuumCoulomb.zeroPositionCoordinate

  21. theorem OAI.ContinuumCoulomb.slabPotential_coordinate_min line 162

    Source documentation

    The actual singular finite-slab potential is minimized in each centered coordinate. The regularized comparison passes through a dominated limit.

    theorem slabPotential_coordinate_min {rho H S : ℝ} (hrho : 0 ≤ rho)
    (hH : 0 ≤ H) (hS : 0 ≤ S) (y : Position) (i : Fin 3) :
    slabPotential rho H S (zeroPositionCoordinate i y) ≤ slabPotential rho H S y := by
…

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

  22. theorem OAI.ContinuumCoulomb.slabPotential_minimum line 177
  23. theorem OAI.ContinuumCoulomb.slabPotential_nonpositive line 190