OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/ComplexFormSplit.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The physical complex one-electron quadratic form splits exactly into its real and imaginary parts. Finite real-orbital penalties split as well.

  1. theorem OAI.ContinuumCoulomb.complex_norm_sq_parts line 13
  2. theorem OAI.ContinuumCoulomb.complex_mass_parts line 17
  3. theorem OAI.ContinuumCoulomb.complex_real_orbital_parts line 22
  4. theorem OAI.ContinuumCoulomb.realPart_partial line 35
  5. theorem OAI.ContinuumCoulomb.imagPart_partial line 40
  6. def OAI.ContinuumCoulomb.positionComplexKinetic line 45
  7. def OAI.ContinuumCoulomb.positionComplexForm line 48
  8. theorem OAI.ContinuumCoulomb.positionComplexForm_parts line 51
  9. theorem OAI.ContinuumCoulomb.real_form_lower_to_complex line 93

    Source documentation

    Real-valued orbitals give the same finite-rank lower estimate for arbitrary complex test functions, without a reality restriction on states.

    theorem real_form_lower_to_complex {ι : Type*} [Fintype ι]
    (V : Position → ℝ) (hV : Continuous V) (ψ : ι → Position → ℝ)
    (hψ : ∀ i, MemLp (ψ i) 2) (E κ : ℝ)
    (hbound : ∀ g : Position → ℝ, ContDiff ℝ 1 g → HasCompactSupport g →
      E*(∫ x, g x^2)-κ*(∑ i, (∫ x, g x*ψ i x)^2) ≤ positionRealForm V g)
    (f : Position → ℂ) (hf : ContDiff ℝ 1 f) (hc : HasCompactSupport f) :
    E*(∫ x, ‖f x‖^2)-κ*(∑ i, ‖∫ x, f x*(ψ i x : ℂ)‖^2) ≤ positionComplexForm V f := by
…

    Mentions: OAI.ContinuumCoulomb.Position, OAI.ContinuumCoulomb.positionRealForm, OAI.ContinuumCoulomb.positionComplexForm