VerticalSliceProjection.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The actual transverse Gaussian defines a contraction on the full L2 product space. No compact-support or smoothness hypothesis is imposed here.

theorem OAI.ContinuumCoulomb.line_pair_sq_le line 12
def OAI.ContinuumCoulomb.verticalCoefficient line 25
theorem OAI.ContinuumCoulomb.split_memLp_vertical_slices line 28
theorem OAI.ContinuumCoulomb.verticalCoefficient_contraction line 37
Source documentation
The normalized Gaussian coefficient is an L2 contraction on arbitrary real wavefunctions, including the closure needed for the continuum form.
```
theorem verticalCoefficient_contraction {freq : ℝ} (hfreq : 0 < freq)
    (f : SplitPosition → ℝ) (hf : MemLp f 2) :
    MemLp (verticalCoefficient freq f) 2 ∧
      (∫ r, (verticalCoefficient freq f r)^2) ≤ ∫ p, f p^2 := by
…
```
Mentions: OAI.ContinuumCoulomb.SplitPosition, OAI.ContinuumCoulomb.verticalCoefficient
theorem OAI.ContinuumCoulomb.verticalCoefficient_sub_ae line 62