Dilation.lean`

23 declarations, 0 contain sorry, 0 declared as axioms

Spatial dilation on the actual weak H¹ domain

The physical-energy amplification in both manuscripts changes coordinates on the full fermionic form domain. Here weak derivatives are transformed by changing variables in the compact-test identity, rather than assuming pointwise differentiability of an arbitrary state.

theorem OAI.ContinuumCoulomb.memLp_comp_dilation line 19
theorem OAI.ContinuumCoulomb.weak_partial_dilation line 27
def OAI.ContinuumCoulomb.dilateState line 87
theorem OAI.ContinuumCoulomb.dilateState_antisymmetric line 96
theorem OAI.ContinuumCoulomb.integral_dilation line 107
theorem OAI.ContinuumCoulomb.mass_dilateState line 113
theorem OAI.ContinuumCoulomb.kinetic_dilateState line 123
def OAI.ContinuumCoulomb.normalizedDilation line 140
Source documentation
The Jacobian factor makes spatial dilation preserve the physical norm.
```
def normalizedDilation {n : ℕ} (state : Coulomb.H1Vector n)
    (scale : ℝ) (hscale : scale ≠ 0) : Coulomb.H1Vector n :=
…
```
Mentions: OAI.Coulomb.H1Vector
theorem OAI.ContinuumCoulomb.mass_normalizedDilation line 145
theorem OAI.ContinuumCoulomb.kinetic_normalizedDilation line 152
theorem OAI.ContinuumCoulomb.normalizedDilation_antisymmetric line 165
theorem OAI.ContinuumCoulomb.h1Vector_ext line 170
theorem OAI.ContinuumCoulomb.normalizedDilation_inverse line 180
Source documentation
Inverse dilation acts on every weak-H¹ state, so lower energy estimates can be transferred back from the entire physical form domain.
```
theorem normalizedDilation_inverse {n : ℕ} (state : Coulomb.H1Vector n)
    (scale : ℝ) (hscale : scale ≠ 0) :
    normalizedDilation (normalizedDilation state scale hscale) scale⁻¹
      (inv_ne_zero hscale) = state := by
…
```
Mentions: OAI.Coulomb.H1Vector, OAI.ContinuumCoulomb.normalizedDilation
theorem OAI.ContinuumCoulomb.position_smul line 212
theorem OAI.ContinuumCoulomb.coulombKernel_smul line 217
def OAI.ContinuumCoulomb.dilatedNuclei line 224
Source documentation
Rescaling the nuclear positions leaves all nuclear charges unchanged.
```
def dilatedNuclei {M : ℕ} (S : Coulomb.Nuclei M) (scale : ℝ)
    (hscale : scale ≠ 0) : Coulomb.Nuclei M where
…
```
Mentions: OAI.Coulomb.Nuclei
theorem OAI.ContinuumCoulomb.attraction_dilatedNuclei line 236
theorem OAI.ContinuumCoulomb.nuclearEnergy_dilateState line 249
theorem OAI.ContinuumCoulomb.nuclearEnergy_normalizedDilation line 275
theorem OAI.ContinuumCoulomb.pairPotential_dilation line 290
theorem OAI.ContinuumCoulomb.pairEnergy_dilateState line 307
theorem OAI.ContinuumCoulomb.pairEnergy_normalizedDilation line 331
theorem OAI.ContinuumCoulomb.form_normalizedDilation line 346
Source documentation
Full electronic form under physical coordinate scaling; no projected sector or differentiability beyond weak H¹ is used.
```
theorem form_normalizedDilation {M n : ℕ} (S : Coulomb.Nuclei M)
    (state : Coulomb.H1Vector n) {scale : ℝ} (hscale : 0 < scale) :
    Coulomb.form (dilatedNuclei S scale hscale.ne')
        (normalizedDilation state scale hscale.ne') =
      scale ^ 2 * Coulomb.kinetic state - scale * Coulomb.nuclearEnergy S state +
        scale * Coulomb.pairEnergy state := by
…
```
Mentions: OAI.Coulomb.Nuclei, OAI.Coulomb.H1Vector, OAI.Coulomb.form, OAI.ContinuumCoulomb.dilatedNuclei, OAI.ContinuumCoulomb.normalizedDilation, OAI.Coulomb.kinetic, OAI.Coulomb.nuclearEnergy, OAI.Coulomb.pairEnergy