CoulombGram.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Coercivity of the actual Coulomb Gram matrix from local dual tests

The unit-charge paper retains all long-range direct interactions. Absolute row dominance need not hold. Smooth disjoint local tests instead give a uniform lower bound for the full Gram form. The hypotheses below concern normalization/localization of the actual densities and the tests; no charge gap or target spectral comparison is assumed.

def OAI.ContinuumCoulomb.coulombGram line 23
def OAI.ContinuumCoulomb.offDiagonalCoulombGram line 26
theorem OAI.ContinuumCoulomb.offDiagonalCoulombGram_symmetric line 29
theorem OAI.ContinuumCoulomb.offDiagonalCoulombGram_diag line 36
theorem OAI.ContinuumCoulomb.coulombGram_diagonal_split line 41
def OAI.ContinuumCoulomb.smoothTestPacket line 65
theorem OAI.ContinuumCoulomb.smoothTestPacket_pair line 70
theorem OAI.ContinuumCoulomb.smoothTestPacket_pair_test line 77
theorem OAI.ContinuumCoulomb.smoothTestPacket_orthogonal line 90
theorem OAI.ContinuumCoulomb.coulombGram_sum line 104

theorem OAI.ContinuumCoulomb.coulombGram_local_duality line 123

Source documentation

A cutoff equal to one on its own packet and disjoint from the other cutoffs is an exact local dual, including for Lp representatives.

theorem coulombGram_local_duality {m : ℕ}
    (density : Fin m → Coulomb.TFLp (volume.restrict Ω))
    (χ : Fin m → Position → ℝ)
    (hmass : ∀ i, (∫ x, Coulomb.tfExtend Ω (density i) x) = 1)
    (hown : ∀ i, ∀ᵐ x, Coulomb.tfExtend Ω (density i) x = 0 ∨ χ i x = 1)
    (hdisjoint : ∀ i j, i ≠ j → Disjoint (tsupport (χ i)) (tsupport (χ j)))
    (i j : Fin m) :
    (∫ x, Coulomb.tfExtend Ω (density i) x * χ j x) = if i = j then 1 else 0 := by
…

Mentions: OAI.Coulomb.TFLp, OAI.ContinuumCoulomb.Position, OAI.Coulomb.tfExtend

theorem OAI.ContinuumCoulomb.coulombGram_coercive line 156

Source documentation

Local duality and disjoint compact tests control the entire long-range Coulomb matrix, with no summability or row-dominance assumption.

theorem coulombGram_coercive (hΩ : MeasurableSet Ω) {m : ℕ}
    (density : Fin m → Coulomb.TFLp (volume.restrict Ω))
    (χ : Fin m → Position → ℝ) (hχ : ∀ i, ContDiff ℝ ∞ (χ i))
    (hc : ∀ i, HasCompactSupport (χ i)) (hs : ∀ i, tsupport (χ i) ⊆ Ω)
    (hdisjoint : ∀ i j, i ≠ j → Disjoint (tsupport (χ i)) (tsupport (χ j)))
    (hdual : ∀ i j, (∫ x, Coulomb.tfExtend Ω (density i) x * χ j x) =
      if i = j then 1 else 0)
    {K : ℝ} (hK : 0 < K)
    (henergy : ∀ i, (∫ x, Coulomb.testCharge (χ i) x * χ i x) ≤ K)
    (d : Fin m → ℝ) :
    (1 / K) * ∑ i, d i ^ 2 ≤ ∑ i, ∑ j, coulombGram density i j * d i * d j := by
…

Mentions: OAI.Coulomb.TFLp, OAI.ContinuumCoulomb.Position, OAI.Coulomb.tfExtend, OAI.Coulomb.testCharge, OAI.ContinuumCoulomb.coulombGram

theorem OAI.ContinuumCoulomb.coulombGram_uniform_charge_condition line 226

Source documentation

Separate the common onsite term from the actual full Coulomb matrix, in exactly the form used by the half-filled Hubbard charge estimate.

theorem coulombGram_uniform_charge_condition {m : ℕ}
    (density : Fin m → Coulomb.TFLp (volume.restrict Ω)) (U c : ℝ)
    (hdiag : ∀ i, coulombGram density i i = U)
    (hcoercive : ∀ d : Fin m → ℝ,
      c * ∑ i, d i ^ 2 ≤ ∑ i, ∑ j, coulombGram density i j * d i * d j)
    (d : Fin m → ℝ) :
    c * ∑ i, d i ^ 2 ≤ U * ∑ i, d i ^ 2 +
      ∑ i, ∑ j, offDiagonalCoulombGram density i j * d i * d j := by
…

Mentions: OAI.Coulomb.TFLp, OAI.ContinuumCoulomb.coulombGram, OAI.ContinuumCoulomb.offDiagonalCoulombGram