Langmuir adsorption model #

This section defines Langmuir adsorption model from kinetics for a single adsorbate on a single site:
$$ θ = \frac{K Pₐ}{1 + K Pₐ} $$ where:

θ is the fractional occupancy of the adsorption sites
K is the adsorption constant describing the adsorption/desorption rates in equilibrium
Pₐ is the partial pressure of the adsorbate

Assumption #

The model assumes the rate of adsorption r_ad = k_ad * Pₐ * S and
the rate of desorption r_d = k_d * A are equal at equilibrium conditions where:

k_ad is the adsorption constant
k_d is the desorption constant
S is the concentartion of all sites
A is the concentartion of occupied sites

Constraints generated by Lean #

S ≠ 0
k_d ≠ 0

To-Do #

Proof statistical mechanical derivation of the model
Generalize proof from properties of system

source

theorem Langmuir_single_site_old (Pₐ k_ad k_d A S : ℝ) (hreaction : let r_ad : ℝ := k_ad * Pₐ * S, r_d : ℝ := k_d * A in r_ad = r_d) (hS : S ≠ 0) (hk_d : k_d ≠ 0) :

let θ : ℝ := A / (S + A), K : ℝ := k_ad / k_d in θ = K * Pₐ / (1 + K * Pₐ)

source

noncomputable def langmuir_single_site_model (equilibrium_constant : ℝ) :

ℝ → ℝ

Equations

langmuir_single_site_model equilibrium_constant = λ (P : ℝ), equilibrium_constant * P / (1 + equilibrium_constant * P)

source

def hernys_law_model (equilibrium_constant : ℝ) :

ℝ → ℝ

Equations

hernys_law_model equilibrium_constant = λ (P : ℝ), equilibrium_constant * P

source

theorem langmuir_single_site_kinetic_derivation {Pₐ k_ad k_d A S : ℝ} (hreaction : let r_ad : ℝ := k_ad * Pₐ * S, r_d : ℝ := k_d * A in r_ad = r_d) (hS : S ≠ 0) (hk_d : k_d ≠ 0) :

let θ : ℝ := A / (S + A), K : ℝ := k_ad / k_d in θ = langmuir_single_site_model K Pₐ

source

theorem langmuir_zero_loading_at_zero_pressure {k_ad k_d : ℝ} :

langmuir_single_site_model (k_ad / k_d) 0 = 0