RepulsionBound.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Coulomb repulsion as a form-domain to L² multiplier

Both continuum comparisons need control of the repulsion applied to a localized many-electron vector, including its mixed block with the continuum complement. Translated pair Hardy and finite Cauchy--Schwarz prove a bound on the actual full repulsion, without summing over an exponentially large spin operator matrix.

def OAI.ContinuumCoulomb.pairRepulsionTerm line 20
def OAI.ContinuumCoulomb.repulsionPotential line 24
theorem OAI.ContinuumCoulomb.pair_hardy_square line 27
theorem OAI.ContinuumCoulomb.repulsionPotential_measurable line 37
theorem OAI.ContinuumCoulomb.repulsionPotential_square_bound line 52
theorem OAI.ContinuumCoulomb.repulsionPotential_spin_L2_bound line 62
theorem OAI.ContinuumCoulomb.repulsionPotential_L2_bound line 113
Source documentation
The full spinful L² multiplication estimate with an explicit polynomial factor in the electron count.
```
theorem repulsionPotential_L2_bound {n : ℕ} (state : Coulomb.H1Vector n) :
    (∑ spin : Coulomb.Spins n,
      ∫ x, repulsionPotential x ^ 2 * ‖state.value spin x‖ ^ 2) ≤
      8 * (n : ℝ) ^ 3 * Coulomb.kinetic state := by
…
```
Mentions: OAI.Coulomb.H1Vector, OAI.Coulomb.Spins, OAI.ContinuumCoulomb.repulsionPotential, OAI.Coulomb.kinetic
theorem OAI.ContinuumCoulomb.repulsion_mul_memLp line 126
theorem OAI.ContinuumCoulomb.repulsion_mul_norm_bound line 139
Source documentation
Equivalently, this controls the squared norm of the actual Coulomb multiplication operator on every component of a full spinful vector.
```
theorem repulsion_mul_norm_bound {n : ℕ} (state : Coulomb.H1Vector n) :
    (∑ spin : Coulomb.Spins n,
      ∫ x, ‖(repulsionPotential x : ℂ) * state.value spin x‖ ^ 2) ≤
      8 * (n : ℝ) ^ 3 * Coulomb.kinetic state := by
…
```
Mentions: OAI.Coulomb.H1Vector, OAI.Coulomb.Spins, OAI.ContinuumCoulomb.repulsionPotential, OAI.Coulomb.kinetic