VerticalResidual.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Exact L2 mass splitting into the Gaussian transverse mode and its orthogonal residual, for arbitrary product-space wavefunctions.

def OAI.ContinuumCoulomb.verticalLift line 12
def OAI.ContinuumCoulomb.verticalResidual line 15
theorem OAI.ContinuumCoulomb.verticalLift_memLp line 18
theorem OAI.ContinuumCoulomb.verticalLift_mass line 32
theorem OAI.ContinuumCoulomb.verticalCoefficient_lift line 39
theorem OAI.ContinuumCoulomb.verticalCoefficient_pair_identity line 47

theorem OAI.ContinuumCoulomb.verticalResidual_mass line 68

Source documentation

Exact Pythagoras identity for the actual transverse projection.

theorem verticalResidual_mass {freq : ℝ} (hfreq : 0 < freq)
    (f : SplitPosition → ℝ) (hf : MemLp f 2) :
    MemLp (verticalResidual freq f) 2 ∧
      (∫ p, (verticalResidual freq f p)^2) =
        (∫ p, f p^2)-(∫ r, (verticalCoefficient freq f r)^2) := by
…

Mentions: OAI.ContinuumCoulomb.SplitPosition, OAI.ContinuumCoulomb.verticalResidual, OAI.ContinuumCoulomb.verticalCoefficient

theorem OAI.ContinuumCoulomb.verticalResidual_coefficient_zero line 93
theorem OAI.ContinuumCoulomb.verticalResidual_orthogonal line 104
Source documentation
The residual is orthogonal to every product with the transverse mode.
```
theorem verticalResidual_orthogonal {freq : ℝ} (hfreq : 0 < freq)
    (f : SplitPosition → ℝ) (hf : MemLp f 2)
    (a : PlanarPosition → ℝ) (ha : MemLp a 2) :
    (∫ p, verticalResidual freq f p*verticalLift freq a p) = 0 := by
…
```
Mentions: OAI.ContinuumCoulomb.SplitPosition, OAI.ContinuumCoulomb.PlanarPosition, OAI.ContinuumCoulomb.verticalResidual, OAI.ContinuumCoulomb.verticalLift