pith. machine review for the scientific record. sign in
theorem proved term proof

dft_exchange_one_statement

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 144theorem dft_exchange_one_statement :
 145    xcContribution 1 = 0 ∧
 146    (∀ x : ℝ, 0 < x → x ≠ 1 → 0 < xcContribution x) ∧
 147    (∀ x : ℝ, 0 < x → xcContribution x = xcContribution x⁻¹) ∧
 148    (0.11 < xcAtPhi ∧ xcAtPhi < 0.13) :=

proof body

Term-mode proof.

 149  ⟨xc_closed_shell_zero, xc_min_at_closed_shell, xc_spin_interchange, xc_at_phi_band⟩
 150
 151end
 152
 153end DFTExchangeFromJCost
 154end QuantumChemistry
 155end IndisputableMonolith

depends on (6)

Lean names referenced from this declaration's body.