scilib documentation

LeanChemicalTheories / molecular_mechanics.lennard_jones

Lennard-Jones potential function #

We define the properties of Lennard-Jonnes potential function that describes intermolecular pair potentials in molecular simulations. The commonly used expression is:
$$ E = 4ε [(\frac{σ}{r})^{12} - (\frac{σ}{r})^6] $$ where:

E is the intermolecular potential between the two atoms or molecules
ε is the well depth and a measure of how strongly the two particles attract each other
σ is the distance at which the intermolecular potential between the two particles is zero
r is the distance of separation between both particles

Here we use our own proof of deriv defined in math.deriv to show that Lennard-Jones potential has its minimum at a distance of r = r_min = 2^1/6 σ, where the potential energy has the value -ε

noncomputable def LJ (ε minRadius r : ℝ) :

Equations

LJ ε minRadius r = let σ : ℝ := 1 / 2 ^ (1 / 6) * minRadius in 4 * ε * (‖σ / r‖ ^ 12 - ‖σ / r‖ ^ 6)

theorem two_pow_one_div_six_pow_six_eq_two :

(2 ^ (1 / 6)) ^ 6 = 2

theorem two_pow_one_div_six_pow_twelve_eq_four :

(2 ^ (1 / 6)) ^ 12 = 4

theorem one_lt_six :

1 < 6

theorem one_lt_twelve :

1 < 12

theorem LJ.minRadius_rpow_div_const_pos (minRadius r y : ℝ) :

0 < minRadius → 0 < r → 0 < y → 0 < minRadius ^ y / r

theorem LJ.const_mul_minRadius_rpow_pos (minRadius r y : ℝ) :

0 < minRadius → 0 < r → 0 < y → 0 < r * minRadius ^ y

theorem LJ.repulsive_2 (minRadius : ℝ) (hminRadius : 0 < minRadius) :

(λ (r : ℝ), |minRadius / (2 ^ (1 / 6) * r)| ^ 12) = λ (r : ℝ), |minRadius ^ 12 / 4| / |r ^ 12|

theorem LJ.repulsive_3 (minRadius : ℝ) (hminRadius : 0 < minRadius) :

(λ (r : ℝ), (|minRadius| / (|2 ^ (1 / 6)| * |r|)) ^ 12) = λ (r : ℝ), |minRadius ^ 12 / 4| / |r ^ 12|

theorem LJ.repulsive_4 (minRadius : ℝ) (hminRaiuds : 0 < minRadius) :

(λ (r : ℝ), minRadius ^ 12 / (2 ^ (1 / 6) * r) ^ 12) = λ (r : ℝ), minRadius ^ 12 / 4 / r ^ 12

theorem LJ.attractive_2 (minRadius : ℝ) (hminRadius : 0 < minRadius) :

(λ (r : ℝ), |minRadius / (2 ^ (1 / 6) * r)| ^ 6) = λ (r : ℝ), |minRadius ^ 6 / 2| / |r ^ 6|

theorem LJ.attractive_3 (minRadius : ℝ) (hminRadius : 0 < minRadius) :

(λ (r : ℝ), (|minRadius| / (|2 ^ (1 / 6)| * |r|)) ^ 6) = λ (r : ℝ), |minRadius ^ 6 / 2| / |r ^ 6|

theorem LJ.attractive_4 (minRadius : ℝ) (hminRadius : 0 < minRadius) :

(λ (r : ℝ), minRadius ^ 6 / (2 ^ (1 / 6) * r) ^ 6) = λ (r : ℝ), minRadius ^ 6 / 2 / r ^ 6

theorem LJ.deriv_of_LJ (ε minRadius : ℝ) (hminRadius : 0 < minRadius) :

set.eq_on (deriv (λ (r : ℝ), LJ ε minRadius r)) (λ (r : ℝ), 4 * ε * ((-3) * minRadius ^ 12 / r ^ 13 - (-3) * minRadius ^ 6 / r ^ 7)) {r : ℝ | r = 0}ᶜ

theorem LJ.has_deriv_at_of_LJ (ε minRadius : ℝ) {r : ℝ} (hminRadius : 0 < minRadius) (hr : r ≠ 0) :

has_deriv_at (λ (r : ℝ), LJ ε minRadius r) (4 * ε * ((-3) * minRadius ^ 12 / r ^ 13 - (-3) * minRadius ^ 6 / r ^ 7)) r

theorem LJ.has_deriv_at_of_LJ' (minRadius : ℝ) {r : ℝ} :

has_deriv_at (λ (x : ℝ), 2 * x ^ 6 / minRadius ^ 6 - 4 * x ^ 12 / minRadius ^ 12) (6 * r ^ 5 * (2 / minRadius ^ 6) - 12 * r ^ 11 * (4 / minRadius ^ 12)) r

theorem LJ.sub_to_div {f g : ℝ → ℝ} (hf : ∀ (x : ℝ), f x ≠ 0) (hg : ∀ (x : ℝ), g x ≠ 0) :

(λ (x : ℝ), f x - g x) = λ (x : ℝ), (1 / g x - 1 / f x) / (1 / (f x * g x))

theorem LJ.sub_eq_mul_one_sub_div {f g : ℝ → ℝ} (s : set ℝ) (hf : ∀ (x : ℝ), x ∈ s → f x ≠ 0) :

set.eq_on (λ (x : ℝ), f x - g x) (λ (x : ℝ), f x * (1 - g x / f x)) s

theorem LJ.fun_sub {f g : ℝ → ℝ} :

(λ (x : ℝ), f x - g x) = (λ (x : ℝ), f x) - λ (x : ℝ), g x

theorem LJ.inv_of_pow_eq_neg_pow {x : ℝ} (n : ℕ) :

(x ^ n)⁻¹ = x ^ -↑n

theorem LJ.inv_of_zpow_eq_neg_pow {x : ℝ} (z : ℤ) :

(x ^ z)⁻¹ = x ^ -z

theorem LJ.tendsto_at_zero_pow_seven_div_pow_one :

filter.tendsto (λ (x : ℝ), x ^ 7 / x) (nhds_within 0 (set.Ioi 0)) (nhds 0)

theorem LJ.tendsto_at_zero_pow_eight_div_pow_two :

filter.tendsto (λ (x : ℝ), x ^ 8 / x ^ 2) (nhds_within 0 (set.Ioi 0)) (nhds 0)

theorem LJ.tendsto_at_zero_pow_nine_div_pow_three :

filter.tendsto (λ (x : ℝ), x ^ 9 / x ^ 3) (nhds_within 0 (set.Ioi 0)) (nhds 0)

theorem LJ.tendsto_at_zero_pow_ten_div_pow_four :

filter.tendsto (λ (x : ℝ), x ^ 10 / x ^ 4) (nhds_within 0 (set.Ioi 0)) (nhds 0)

theorem LJ.tendsto_at_zero_pow_eleven_div_pow_five :

filter.tendsto (λ (x : ℝ), x ^ 11 / x ^ 5) (nhds_within 0 (set.Ioi 0)) (nhds 0)

theorem LJ.tendsto_at_zero_pow_twelve_div_pow_six :

filter.tendsto (λ (x : ℝ), x ^ 12 / x ^ 6) (nhds_within 0 (set.Ioi 0)) (nhds 0)

theorem LJ.sub_to_div' (minRadius : ℝ) (hm : 0 < minRadius) :

set.eq_on (λ (x : ℝ), minRadius ^ 12 / (2 ^ 6⁻¹) ^ 12 / x ^ 12 - minRadius ^ 6 / (2 ^ 6⁻¹) ^ 6 / x ^ 6) (λ (x : ℝ), minRadius ^ 12 / (2 ^ 6⁻¹) ^ 12 / x ^ 12 * (1 - minRadius ^ 6 / (2 ^ 6⁻¹) ^ 6 / x ^ 6 / (minRadius ^ 12 / (2 ^ 6⁻¹) ^ 12 / x ^ 12))) {r : ℝ | r ≠ 0}

theorem LJ.sub_to_div'' (minRadius : ℝ) (hm : 0 < minRadius) (hx : ∀ (x : ℝ), x ∈ {r : ℝ | r ≠ 0}) :

(λ (x : ℝ), minRadius ^ 12 / (2 ^ 6⁻¹) ^ 12 / x ^ 12 - minRadius ^ 6 / (2 ^ 6⁻¹) ^ 6 / x ^ 6) = λ (x : ℝ), minRadius ^ 12 / (2 ^ 6⁻¹) ^ 12 / x ^ 12 * (1 - minRadius ^ 6 / (2 ^ 6⁻¹) ^ 6 / x ^ 6 / (minRadius ^ 12 / (2 ^ 6⁻¹) ^ 12 / x ^ 12))