scilib documentation

LeanChemicalTheories / adsorption.BETInfinite

BET #

This section defines the Brunauer–Emmett–Teller (BET) adsorption theory where we relax the assumption of the Langmuir model that restricts adsorption on a single site to be one molecule; instead, molecules can stack on top of each other in layers.

Definitions #

structure BET.system :

Type

C_1 : ℝ
C_L : ℝ
s₀ : ℝ
P₀ : ℝ
hCL : 0 < self.C_L
hC1 : 0 < self.C_1
hs₀ : 0 < self.s₀
hP₀ : 0 < self.P₀

Instances for BET.system

BET.system.has_sizeof_inst

def BET.first_layer_adsoprtion_rate (S : BET.system) (P : ℝ) :

Equations

BET.first_layer_adsoprtion_rate S P = S.C_1 * P

def BET.n_layer_adsorption_rate (S : BET.system) (P : ℝ) :

Equations

BET.n_layer_adsorption_rate S P = S.C_L * P

noncomputable def BET.adsorption_constant (S : BET.system) :

Equations

BET.adsorption_constant S = S.C_1 / S.C_L

noncomputable def BET.seq (S : BET.system) (P : ℝ) :

Equations

BET.seq S P n.succ = BET.n_layer_adsorption_rate S P ^ (n + 1) * S.s₀ * BET.adsorption_constant S
BET.seq S P 0 = S.s₀

noncomputable def BET.volume_adsorbed (S : BET.system) (V₀ P : ℝ) :

Equations

BET.volume_adsorbed S V₀ P = V₀ * ∑' (k : ℕ), ↑k * BET.seq S P k

noncomputable def BET.catalyst_area (S : BET.system) (P : ℝ) :

Equations

BET.catalyst_area S P = ∑' (k : ℕ), BET.seq S P k

Proof #

theorem BET.sequence_math {S : BET.system} {P : ℝ} (hx1 : BET.n_layer_adsorption_rate S P < 1) (hx2 : 0 < BET.n_layer_adsorption_rate S P) :

(∑' (k : ℕ), (↑k + 1) * BET.seq S P (k + 1)) / (S.s₀ + ∑' (k : ℕ), BET.seq S P (k + 1)) = BET.adsorption_constant S * BET.n_layer_adsorption_rate S P / ((1 - BET.n_layer_adsorption_rate S P) * (1 - BET.n_layer_adsorption_rate S P + BET.n_layer_adsorption_rate S P * BET.adsorption_constant S))

theorem BET.regression_form {P V₀ : ℝ} (S : BET.system) (hx1 : BET.n_layer_adsorption_rate S P < 1) (hx2 : 0 < BET.n_layer_adsorption_rate S P) (hθ : 0 < S.s₀) (hP : 0 < P) :

let a : ℝ := V₀ * S.C_1, b : ℝ := S.C_L, c : ℝ := S.C_1, q : ℝ := BET.volume_adsorbed S V₀ P / BET.catalyst_area S P in q = a * P / ((1 - b * P) * (1 - b * P + c * P))

noncomputable def BET.brunauer_26 (S : BET.system) (P : ℝ) :

Equations

BET.brunauer_26 S = λ (P : ℝ), BET.adsorption_constant S * BET.n_layer_adsorption_rate S P / ((1 - BET.n_layer_adsorption_rate S P) * (1 - BET.n_layer_adsorption_rate S P + BET.adsorption_constant S * BET.n_layer_adsorption_rate S P))

theorem BET.brunauer_26_from_seq {P V₀ : ℝ} {S : BET.system} (hx1 : BET.n_layer_adsorption_rate S P < 1) (hx2 : 0 < BET.n_layer_adsorption_rate S P) (hP : 0 < P) :

BET.volume_adsorbed S V₀ P / BET.catalyst_area S P = V₀ * BET.brunauer_26 S P

theorem BET.tendsto_at_top_at_inv_CL (S : BET.system) :

filter.tendsto (BET.brunauer_26 S) (nhds_within (1 / S.C_L) (set.Ioo 0 (1 / S.C_L))) filter.at_top

theorem BET.tendsto_at_bot_at_inv_CL (S : BET.system) (hCL : S.C_1 < S.C_L) :

filter.tendsto (BET.brunauer_26 S) (nhds_within (1 / S.C_L) (set.Ioo (1 / S.C_L) (1 / (S.C_L - S.C_1)))) filter.at_bot

theorem BET.tendsto_at_bot_at_inv_CL' (S : BET.system) (hCL : S.C_L ≤ S.C_1) :

filter.tendsto (BET.brunauer_26 S) (nhds_within (1 / S.C_L) (set.Ioi (1 / S.C_L))) filter.at_bot

noncomputable def BET.brunauer_28 (S : BET.system) (P : ℝ) :

Equations

BET.brunauer_28 S = λ (P : ℝ), BET.adsorption_constant S * P / ((S.P₀ - P) * (1 + (BET.adsorption_constant S - 1) * (P / S.P₀)))

theorem BET.brunauer_28_from_seq {P V₀ : ℝ} (S : BET.system) (h27 : S.P₀ = 1 / S.C_L) (hx1 : BET.n_layer_adsorption_rate S P < 1) (hx2 : 0 < BET.n_layer_adsorption_rate S P) (hP : 0 < P) :

BET.volume_adsorbed S V₀ P / BET.catalyst_area S P = V₀ * BET.brunauer_28 S P