CoulombGramApprox.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Quantitative local duality for overlapping densities. The compact local tests are disjoint; the electron density packets need not be disjoint.

theorem OAI.ContinuumCoulomb.dualMatrix_quadratic_lower line 13
theorem OAI.ContinuumCoulomb.smoothTestPacket_sum_energy line 54

theorem OAI.ContinuumCoulomb.coulombGram_coercive_of_dual_lower line 84

Source documentation

Coercivity from approximate local duality; overlap of the densities is allowed and all Coulomb interactions remain in the matrix.

theorem coulombGram_coercive_of_dual_lower (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)))
    {K a : ℝ} (hK : 0 < K) (ha : 0 ≤ a)
    (henergy : ∀ i, (∫ x, Coulomb.testCharge (χ i) x * χ i x) ≤ K)
    (hdual : ∀ d : Fin m → ℝ, a * ∑ i, d i ^ 2 ≤
      ∑ i, ∑ j, d i * d j * ∫ x, Coulomb.tfExtend Ω (density i) x * χ j x)
    (d : Fin m → ℝ) :
    (a ^ 2 / 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.testCharge, OAI.Coulomb.tfExtend, OAI.ContinuumCoulomb.coulombGram

theorem OAI.ContinuumCoulomb.coulombGram_coercive_local_estimates line 133

Source documentation

The diagonal test mass may vary from site to site. Only a common lower bound and small off-site leakage are needed.

theorem coulombGram_coercive_local_estimates (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)))
    {K a delta : ℝ} (hK : 0 < K) (hdelta : 0 ≤ delta)
    (hmargin : 0 ≤ a - m * delta)
    (henergy : ∀ i, (∫ x, Coulomb.testCharge (χ i) x * χ i x) ≤ K)
    (hdiag : ∀ i, a ≤ ∫ x, Coulomb.tfExtend Ω (density i) x * χ i x)
    (hoff : ∀ i j, i ≠ j → |∫ x, Coulomb.tfExtend Ω (density i) x * χ j x| ≤ delta)
    (d : Fin m → ℝ) :
    ((a - m * delta) ^ 2 / K) * ∑ i, d i ^ 2 ≤
…

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