DensitySynthesis.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Nonnegative continuous-density synthesis for the unit-charge construction

The density is the uniform slab plus ΔV/(4π). Compact support of V inside the slab makes its attractive Coulomb field exactly the slab field plus V. A pointwise Laplacian bound makes the density nonnegative. Only C² regularity is required, as the manuscript's manufactured well is finitely smooth.

def OAI.ContinuumCoulomb.slabDomain line 21
theorem OAI.ContinuumCoulomb.slabDomain_isClosed line 24
theorem OAI.ContinuumCoulomb.slabDomain_isCompact line 33
def OAI.ContinuumCoulomb.slabDensity line 52
def OAI.ContinuumCoulomb.slabPotential line 55
def OAI.ContinuumCoulomb.synthesizedDensity line 58
theorem OAI.ContinuumCoulomb.slabDensity_integrable line 61
theorem OAI.ContinuumCoulomb.slabDensity_integral line 66
theorem OAI.ContinuumCoulomb.manufacturedCharge_continuous line 70
theorem OAI.ContinuumCoulomb.manufacturedCharge_compact line 74
theorem OAI.ContinuumCoulomb.manufacturedCharge_zero line 79
theorem OAI.ContinuumCoulomb.synthesizedDensity_bounds line 84
theorem OAI.ContinuumCoulomb.synthesizedDensity_lower_on_slab line 97
theorem OAI.ContinuumCoulomb.synthesizedDensity_integrable line 104
theorem OAI.ContinuumCoulomb.synthesizedDensity_integral line 113
Source documentation
The manufactured correction carries zero net charge, so the total density mass is exactly the uniform slab mass.
```
theorem synthesizedDensity_integral {H S : ℝ} (hH : 0 ≤ H) (hS : 0 ≤ S) (rho : ℝ)
    (V : Position → ℝ) (hV : ContDiff ℝ 2 V) (hc : HasCompactSupport V) :
    (∫ x, synthesizedDensity rho H S V x) = volume.real (slabDomain H S) * rho := by
…
```
Mentions: OAI.ContinuumCoulomb.Position, OAI.ContinuumCoulomb.synthesizedDensity, OAI.ContinuumCoulomb.slabDomain
theorem OAI.ContinuumCoulomb.synthesizedDensity_potential line 124
Source documentation
Equation (4) of the unit-charge manuscript, as an identity of the actual three-dimensional Coulomb integrals at every evaluation point.
```
theorem synthesizedDensity_potential {rho H S : ℝ} (hrho : 0 ≤ rho)
    (hH : 0 ≤ H) (hS : 0 ≤ S) (V : Position → ℝ)
    (hV : ContDiff ℝ 2 V) (hc : HasCompactSupport V)
    (hbound : ∀ x, |manufacturedCharge V x| ≤ rho / 2) (y : Position) :
    -(∫ x, Coulomb.coulombKernel (y - x) * synthesizedDensity rho H S V x) =
      slabPotential rho H S y + V y := by
…
```
Mentions: OAI.ContinuumCoulomb.Position, OAI.ContinuumCoulomb.manufacturedCharge, OAI.Coulomb.coulombKernel, OAI.ContinuumCoulomb.synthesizedDensity, OAI.ContinuumCoulomb.slabPotential