SplitProjectionBudget.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The full planar slice penalty is controlled by transverse mass and the finite family of actual tensor-orbital coefficients.

theorem OAI.ContinuumCoulomb.planarCoefficient_mass_split line 13
theorem OAI.ContinuumCoulomb.split_projection_budget line 62
Source documentation
The estimate removes the spurious infinite-dimensional planar penalty in the excited transverse sector, retaining only actual tensor coefficients.
```
theorem split_projection_budget {freq D : ℝ} (hfreq : 0 < freq)
    {m : ℕ} (u : Fin m → PlanarPosition)
    (hsep : ∀ i j, i ≠ j → D ≤ ‖u i-u j‖)
    (f : SplitPosition → ℝ) (hf : MemLp f 2) :
    (∫ z, ∑ i, (planarCoefficient (u i) f z)^2) ≤
      (1+m*localizedOverlapBound D)*
        ((∫ p, f p^2)-(∫ r, (verticalCoefficient freq f r)^2)) +
      ∑ i, (∫ p, f p*localizedMode freq (u i) p)^2 := by
…
```
Mentions: OAI.ContinuumCoulomb.PlanarPosition, OAI.ContinuumCoulomb.SplitPosition, OAI.ContinuumCoulomb.planarCoefficient, OAI.ContinuumCoulomb.localizedOverlapBound, OAI.ContinuumCoulomb.verticalCoefficient, OAI.ContinuumCoulomb.localizedMode