OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/VerticalCappedForm.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

The actual capped transverse oscillator and its two-part IMS formula. The cutoff is one on the inner half-slab and zero beyond the slab.

  1. def OAI.ContinuumCoulomb.verticalCapPotential line 16
  2. def OAI.ContinuumCoulomb.verticalCappedForm line 19
  3. def OAI.ContinuumCoulomb.verticalCutoffAngle line 22
  4. def OAI.ContinuumCoulomb.verticalInnerCutoff line 25
  5. def OAI.ContinuumCoulomb.verticalOuterCutoff line 26
  6. theorem OAI.ContinuumCoulomb.verticalCutoffAngle_smooth line 28
  7. theorem OAI.ContinuumCoulomb.verticalInnerCutoff_smooth line 31
  8. theorem OAI.ContinuumCoulomb.verticalOuterCutoff_smooth line 34
  9. theorem OAI.ContinuumCoulomb.verticalCutoff_partition line 37
  10. theorem OAI.ContinuumCoulomb.verticalCutoff_inner line 40
  11. theorem OAI.ContinuumCoulomb.verticalCutoff_outer line 51
  12. theorem OAI.ContinuumCoulomb.vertical_deriv_square_integrable line 61
  13. theorem OAI.ContinuumCoulomb.vertical_product_integrable line 69
  14. theorem OAI.ContinuumCoulomb.verticalCutoffBump_deriv_bounded line 76
  15. def OAI.ContinuumCoulomb.verticalCutoffDerivativeConstant line 82
  16. theorem OAI.ContinuumCoulomb.verticalCutoffDerivativeConstant_nonnegative line 84
  17. def OAI.ContinuumCoulomb.verticalCutoffDerivativeBound line 87
  18. theorem OAI.ContinuumCoulomb.verticalCutoffAngle_deriv line 90
  19. theorem OAI.ContinuumCoulomb.verticalCutoffAngle_deriv_bound line 100
  20. theorem OAI.ContinuumCoulomb.verticalCutoff_deriv_identity line 107
  21. theorem OAI.ContinuumCoulomb.verticalCappedForm_IMS line 129

    Source documentation

    Exact IMS identity on the actual one-dimensional capped form.

    theorem verticalCappedForm_IMS (freq S : ℝ) (u : ℝ → ℝ)
    (hu : ContDiff ℝ 1 u) (hc : HasCompactSupport u) :
    verticalCappedForm freq S (fun z => verticalInnerCutoff S z*u z) +
      verticalCappedForm freq S (fun z => verticalOuterCutoff S z*u z) =
      verticalCappedForm freq S u + (1/2:ℝ)*∫ z, deriv (verticalCutoffAngle S) z^2*u z^2 := by
…

    Mentions: OAI.ContinuumCoulomb.verticalCappedForm, OAI.ContinuumCoulomb.verticalInnerCutoff, OAI.ContinuumCoulomb.verticalOuterCutoff, OAI.ContinuumCoulomb.verticalCutoffAngle

  22. theorem OAI.ContinuumCoulomb.verticalCappedForm_inner line 160

    Source documentation

    On the supported inner piece the capped potential is exactly harmonic.

    theorem verticalCappedForm_inner {S : ℝ} (hS : 0 < S) (freq : ℝ) (u : ℝ → ℝ) :
    verticalCappedForm freq S (fun z => verticalInnerCutoff S z*u z) =
      verticalForm freq (fun z => verticalInnerCutoff S z*u z) := by
…

    Mentions: OAI.ContinuumCoulomb.verticalCappedForm, OAI.ContinuumCoulomb.verticalInnerCutoff, OAI.ContinuumCoulomb.verticalForm