OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/OneElectronFormDecomposition.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Exact full-graph decomposition into the corrected orbital component and its orthogonal remainder.

  1. theorem OAI.ContinuumCoulomb.correctedOneElectron_graph_decomposition line 12
  2. theorem OAI.ContinuumCoulomb.correctedOneElectron_form_decomposition line 34
  3. theorem OAI.ContinuumCoulomb.absorb_cross_term line 49

    Source documentation

    Scalar absorption of a mixed form; the denominator is the retained complement gap and no square root is introduced into the reduction.

    theorem absorb_cross_term {c B p q δ : ℝ}
    (hB : 0 ≤ B) (hp : 0 ≤ p) (hq : 0 ≤ q) (hδ : 0 < δ)
    (hc : c^2 ≤ B*p*q) : -(B/δ)*p-δ*q ≤ 2*c := by
…