OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/GramCorrection.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Quantitative symmetric orthonormalization of a finite real Gram matrix. The correction is the actual spectral inverse square root, with Euclidean operator norm estimates independent of the ambient function space.

  1. lemma OAI.ContinuumCoulomb.GramCorrection.inverseSqrt_bounds line 15
  2. lemma OAI.ContinuumCoulomb.GramCorrection.eigenvalue_bounds line 44
  3. def OAI.ContinuumCoulomb.GramCorrection.correction line 66
  4. lemma OAI.ContinuumCoulomb.GramCorrection.correction_isHermitian line 69
  5. lemma OAI.ContinuumCoulomb.GramCorrection.correction_transpose line 73
  6. lemma OAI.ContinuumCoulomb.GramCorrection.correction_gram line 77
  7. lemma OAI.ContinuumCoulomb.GramCorrection.correction_norm_bounds line 97
  8. lemma OAI.ContinuumCoulomb.GramCorrection.entry_abs_le_norm line 121
  9. lemma OAI.ContinuumCoulomb.GramCorrection.correction_entry_bounds line 134
  10. theorem OAI.ContinuumCoulomb.GramCorrection.exists_symmetric_correction line 148

    Source documentation

    The actual symmetric correction orthonormalizes the given Gram matrix, changes coefficients by at most twice its overlap row bound, and has Euclidean operator norm at most two.

    theorem exists_symmetric_correction (hG : G.IsHermitian) {delta : ℝ} (hdelta : 0 ≤ delta)
    (hdiag : ∀ i, G i i = 1) (hoff : ∀ i j, i ≠ j → |G i j| ≤ delta)
    (hsmall : m * delta ≤ 1 / 2) :
    ∃ A : Matrix (Fin m) (Fin m) ℝ,
      Aᵀ = A ∧ Aᵀ * G * A = 1 ∧ ‖A - 1‖ ≤ 2 * m * delta ∧ ‖A‖ ≤ 2 := by
…