OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/VerticalCutoffTail.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Gaussian control of the inner-slab projection error for the actual transverse cutoff. The loss decays exponentially in the square of the slab width, with the oscillator frequency fixed by the construction.

  1. def OAI.ContinuumCoulomb.verticalCutoffError line 13
  2. theorem OAI.ContinuumCoulomb.verticalCutoffError_memLp line 16
  3. def OAI.ContinuumCoulomb.verticalCutoffTailConstant line 31
  4. theorem OAI.ContinuumCoulomb.verticalCutoffTailConstant_nonnegative line 34
  5. theorem OAI.ContinuumCoulomb.verticalCutoffError_square_bound line 40
  6. theorem OAI.ContinuumCoulomb.verticalCutoffError_integral_bound line 74
  7. theorem OAI.ContinuumCoulomb.verticalCutoff_pair_error line 90

    Source documentation

    The projection error is bounded for every actual L2 test function.

    theorem verticalCutoff_pair_error {freq S : ℝ} (hfreq : 0 < freq) (hS : 0 < S)
    (u : ℝ → ℝ) (hu : MemLp u 2) :
    ((∫ z, (verticalInnerCutoff S z*u z)*verticalMode freq z) -
      (∫ z, u z*verticalMode freq z))^2 ≤
      (∫ z, u z^2)*(verticalCutoffTailConstant freq * Real.exp (-freq*S^2/8)) := by
…

    Mentions: OAI.ContinuumCoulomb.verticalInnerCutoff, OAI.ContinuumCoulomb.verticalMode, OAI.ContinuumCoulomb.verticalCutoffTailConstant