OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/PlanarFrameBound.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The actual uncut planar modes satisfy the finite-frame bound needed when combining planar and transverse spectral estimates.

  1. theorem OAI.ContinuumCoulomb.frame_bound_from_synthesis line 13
  2. def OAI.ContinuumCoulomb.planarOrbitalL2 line 35
  3. theorem OAI.ContinuumCoulomb.planarOrbitalL2_inner line 39
  4. theorem OAI.ContinuumCoulomb.planarOrbitalL2_frame_bound line 54
  5. theorem OAI.ContinuumCoulomb.planar_modes_frame_bound line 77

    Source documentation

    Integral form, usable on almost-everywhere L2 slices.

    theorem planar_modes_frame_bound {D : ℝ} {m : ℕ} (u : Fin m → PlanarPosition)
    (hsep : ∀ i j, i ≠ j → D ≤ ‖u i-u j‖)
    (f : PlanarPosition → ℝ) (hf : MemLp f 2) :
    ∑ i, (∫ r, f r*normalizedPlanarMode (r-u i))^2 ≤
      (1+m*localizedOverlapBound D)*(∫ r, f r^2) := by
…

    Mentions: OAI.ContinuumCoulomb.PlanarPosition, OAI.ContinuumCoulomb.normalizedPlanarMode, OAI.ContinuumCoulomb.localizedOverlapBound