Stochastic mass action, metabolic control and flux balance

DefinitionStochastic mass-action propensity#✓fully proved

The stochastic mass-action propensity of reaction r in state x (molecule counts): k r * ∏_s x_s (x_s - 1) ⋯ (x_s - src_s + 1), the falling factorial Nat.descFactorial x_s src_s (it vanishes when x_s < src_s). Anderson, Craciun & Kurtz (2010), §2.

noncomputable def propensity (k : ρ → ℝ) (r : ρ) (x : S → ℕ) : ℝ :=
  k r * ∏ s, ((x s).descFactorial (N.src r s) : ℝ)

Uses 1 · Used by 4

Statement usesChemical reaction network

Used byGenerator of the mass-action chain on a finite state class · Restricted mass-action generator is a rate matrix · Global balance of the product-form Poisson weights · Anderson–Craciun–Kurtz on a finite class

DefinitionState after one reaction firing#✓fully proved

The state reached from x by one firing of reaction r, x - src r + prod r (meaningful when src r ≤ x, the only case in which the propensity is nonzero).

def fire (r : ρ) (x : S → ℕ) : S → ℕ := fun s => x s - N.src r s + N.prod r s

Uses 1 · Used by 4

Statement usesChemical reaction network

Used byGenerator of the mass-action chain on a finite state class · Stationary law of the stochastic mass-action chain on a finite class · Restricted mass-action generator is a rate matrix · Anderson–Craciun–Kurtz on a finite class

DefinitionState before one reaction firing#✓fully proved

The state from which one firing of reaction r leads to x, x - prod r + src r (meaningful when prod r ≤ x).

def unfire (r : ρ) (x : S → ℕ) : S → ℕ := fun s => x s - N.prod r s + N.src r s

Uses 1 · Used by 3

Statement usesChemical reaction network

Used byStationary law of the stochastic mass-action chain on a finite class · Global balance of the product-form Poisson weights · Anderson–Craciun–Kurtz on a finite class

DefinitionProduct-form Poisson weight of a state#✓fully proved

The product-form Poisson weight ∏_s c_s ^ x_s e^{-c_s} / Nat.factorial x_s of a state x.

noncomputable def poissonWeight (c : S → ℝ) (x : S → ℕ) : ℝ :=
  ∏ s, c s ^ x s * Real.exp (-c s) / ((x s).factorial : ℝ)

Used by 4

Used byNormalized Poisson stationary law on a finite state class · Stationary law of the stochastic mass-action chain on a finite class · Global balance of the product-form Poisson weights · Anderson–Craciun–Kurtz on a finite class

DefinitionGenerator of the mass-action chain on a finite state class#✓fully proved

The generator of the stochastic mass-action chain restricted to a finite set Ω of states: Q x y = ∑_r λ_r(x) ([fire r x = y] - [x = y]). It is a rate matrix when Ω is closed under firing (isRateMatrix_classGenerator).

noncomputable def classGenerator (k : ρ → ℝ) (Ω : Finset (S → ℕ)) : Matrix Ω Ω ℝ :=
  fun x y => ∑ r, propensity N k r x *
    ((if fire N r x = (y : S → ℕ) then 1 else 0) - if x = y then 1 else 0)

Uses 3 · Used by 3

Statement usesChemical reaction network · State after one reaction firing · Stochastic mass-action propensity

Used byStationary law of the stochastic mass-action chain on a finite class · Restricted mass-action generator is a rate matrix · Anderson–Craciun–Kurtz on a finite class

TheoremGlobal balance of the product-form Poisson weights#✓fully proved

Global balance of the product-form Poisson weights (Anderson, Craciun & Kurtz 2010, Thm 4.1): if c is complex balanced for the deterministic mass-action system with rate constants k, then at every state x the total outflow π(x) ∑_r λ_r(x) equals the total inflow ∑_{r : prod r ≤ x} π(x - prod r + src r) λ_r(x - prod r + src r) for π = poissonWeight c. This is an algebraic identity valid for all real k and c.

theorem poissonWeight_mul_sum_propensity {k : ρ → ℝ} {c : S → ℝ}
    (hcb : N.IsComplexBalanced k c) (x : S → ℕ) :
    poissonWeight c x * ∑ r, propensity N k r x =
      ∑ r ∈ univ.filter (fun r => N.prod r ≤ x),
        poissonWeight c (unfire N r x) * propensity N k r (unfire N r x)

Uses 7 · Used by 1

Statement usesChemical reaction network · Complex-balanced concentrations · Product-form Poisson weight of a state · Stochastic mass-action propensity · State before one reaction firing

Proof usesMass-action reaction rate · Complex balance exchanges source and product sums

Used byAnderson–Craciun–Kurtz on a finite class

TheoremRestricted mass-action generator is a rate matrix#✓fully proved

The restricted generator is a rate matrix when the rate constants are nonnegative and Ω is closed under the reactions.

theorem isRateMatrix_classGenerator {k : ρ → ℝ} (hk : ∀ r, 0 ≤ k r) {Ω : Finset (S → ℕ)}
    (hfwd : ∀ x ∈ Ω, ∀ r, N.src r ≤ x → fire N r x ∈ Ω) :
    ProbabilityTheory.IsRateMatrix (classGenerator N k Ω)

Uses 5 · Used by 1

Statement usesChemical reaction network · Generator of the mass-action chain on a finite state class · State after one reaction firing · Rate matrix

Proof usesStochastic mass-action propensity

Used byStationary law of the stochastic mass-action chain on a finite class

TheoremAnderson–Craciun–Kurtz on a finite class#✓fully proved

Anderson–Craciun–Kurtz on a finite class (Anderson, Craciun & Kurtz 2010, Thm 4.1–4.2): if c is complex balanced and every state of Ω from which a reaction leads into Ω lies in Ω (hbwd), the Poisson weights restricted to Ω are invariant for the restricted generator: π Q = 0, for all real k and c. For a closed communicating class of a weakly reversible network with positive rate constants hbwd holds (the reverse reaction path leads back).

theorem poissonWeight_vecMul_classGenerator {k : ρ → ℝ} {c : S → ℝ}
    (hcb : N.IsComplexBalanced k c) {Ω : Finset (S → ℕ)}
    (hbwd : ∀ x ∈ Ω, ∀ r, N.prod r ≤ x → unfire N r x ∈ Ω) :
    (fun x : Ω => poissonWeight c x) ᵥ* classGenerator N k Ω = 0

Uses 8 · Used by 1

Statement usesChemical reaction network · Complex-balanced concentrations · Generator of the mass-action chain on a finite state class · Product-form Poisson weight of a state · State before one reaction firing

Proof usesState after one reaction firing · Global balance of the product-form Poisson weights · Stochastic mass-action propensity

Used byStationary law of the stochastic mass-action chain on a finite class

DefinitionNormalized Poisson stationary law on a finite state class#✓fully proved

The Poisson weights normalized on a finite set Ω of states.

noncomputable def classStationaryLaw (c : S → ℝ) (Ω : Finset (S → ℕ)) : Ω → ℝ :=
  fun x => poissonWeight c x / ∑ y ∈ Ω, poissonWeight c y

Uses 1 · Used by 1

Statement usesProduct-form Poisson weight of a state

Used byStationary law of the stochastic mass-action chain on a finite class

TheoremStationary law of the stochastic mass-action chain on a finite class#✓fully proved

Stationary law of the stochastic mass-action chain on a finite class (Anderson, Craciun & Kurtz 2010, Thm 4.1–4.2). Let the rate constants be nonnegative, c > 0 complex balanced, and Ω a nonempty finite set of states closed under the reactions in both directions. Then the restricted generator is a rate matrix, and the normalized product-form Poisson law π(x) ∝ ∏_s c_s^{x_s} e^{-c_s} / Nat.factorial x_s on Ω is a positive probability vector invariant under the transition semigroup: π P(t) = π for every t.

theorem classStationaryLaw_spec {k : ρ → ℝ} (hk : ∀ r, 0 ≤ k r) {c : S → ℝ}
    (hc : ∀ s, 0 < c s) (hcb : N.IsComplexBalanced k c) {Ω : Finset (S → ℕ)}
    (hΩ : Ω.Nonempty) (hfwd : ∀ x ∈ Ω, ∀ r, N.src r ≤ x → fire N r x ∈ Ω)
    (hbwd : ∀ x ∈ Ω, ∀ r, N.prod r ≤ x → unfire N r x ∈ Ω) :
    ProbabilityTheory.IsRateMatrix (classGenerator N k Ω) ∧
      (∀ x, 0 < classStationaryLaw c Ω x) ∧ ∑ x, classStationaryLaw c Ω x = 1 ∧
      ∀ t, classStationaryLaw c Ω ᵥ* ProbabilityTheory.ctmcTransition (classGenerator N k Ω) t =
        classStationaryLaw c Ω

Uses 12

Statement usesChemical reaction network · Complex-balanced concentrations · Generator of the mass-action chain on a finite state class · Normalized Poisson stationary law on a finite state class · State after one reaction firing · State before one reaction firing · Rate matrix · Transition semigroup of a continuous-time Markov chain

Proof usesRestricted mass-action generator is a rate matrix · Product-form Poisson weight of a state · Anderson–Craciun–Kurtz on a finite class · Invariance under the semigroup

DefinitionReaction fluxes proportional to enzyme levels#✓fully proved

Reaction rates v_i(e, s) = e_i f_i(s) proportional to enzyme levels e.

def flux (f : R → (M → ℝ) → ℝ) (e : R → ℝ) (s : M → ℝ) : R → ℝ := fun i => e i * f i s

Used by 7

Used byElasticity of a reaction rate · Regular steady states exist by the implicit function theorem · Regular steady state of a metabolic network · Steady-state fluxes along a steady-state map · Concentration summation theorem · Flux summation theorem · Flux connectivity theorem

DefinitionSteady-state fluxes along a steady-state map#✓fully proved

The steady-state fluxes J(e) = v(e, σ(e)) along a steady-state map σ.

def steadyFlux (f : R → (M → ℝ) → ℝ) (σ : (R → ℝ) → M → ℝ) (e : R → ℝ) : R → ℝ :=
  flux f e (σ e)

Uses 1 · Used by 4

Statement usesReaction fluxes proportional to enzyme levels

Used byFlux control coefficient · Concentration summation theorem · Flux summation theorem · Flux connectivity theorem

DefinitionFlux control coefficient#✓fully proved

The flux control coefficient C^{J_j}_{e_i} = (e_i / J_j) ∂J_j/∂e_i. It is meaningful when J_j ≠ 0 and the steady-state flux is differentiable at e; otherwise Lean's x / 0 = 0 and fderiv of a non-differentiable map, 0, give junk values.

noncomputable def fluxControl (f : R → (M → ℝ) → ℝ) (σ : (R → ℝ) → M → ℝ) (e : R → ℝ)
    (j i : R) : ℝ :=
  e i / steadyFlux f σ e j * fderiv ℝ (fun e' => steadyFlux f σ e' j) e (Pi.single i 1)

Uses 1 · Used by 2

Statement usesSteady-state fluxes along a steady-state map

Used byFlux summation theorem · Flux connectivity theorem

DefinitionConcentration control coefficient#✓fully proved

The concentration control coefficient C^{s_m}_{e_i} = (e_i / s_m) ∂s_m/∂e_i, meaningful for a positive concentration s_m and a steady state differentiable at e.

noncomputable def concControl (σ : (R → ℝ) → M → ℝ) (e : R → ℝ) (m : M) (i : R) : ℝ :=
  e i / σ e m * fderiv ℝ (fun e' => σ e' m) e (Pi.single i 1)

Used by 1

Used byConcentration summation theorem

DefinitionElasticity of a reaction rate#✓fully proved

The elasticity ε^{v_i}_{s_m} = (s_m / v_i) ∂v_i/∂s_m, meaningful for a nonzero rate v_i and a rate law differentiable at s.

noncomputable def elasticity [DecidableEq M] (f : R → (M → ℝ) → ℝ) (e : R → ℝ) (s : M → ℝ)
    (i : R) (m : M) : ℝ :=
  s m / flux f e s i * fderiv ℝ (fun s' => flux f e s' i) s (Pi.single m 1)

Uses 1 · Used by 1

Statement usesReaction fluxes proportional to enzyme levels

Used byFlux connectivity theorem

StructureRegular steady state of a metabolic network#✓fully proved

A regular steady state at enzyme levels e₀: σ is differentiable at e₀, the rate laws are differentiable at σ e₀, N v(e, σ e) = 0 for e near e₀, and the Jacobian δ ↦ N ∂_s v(e₀, σ e₀) δ is injective (it is square, so this is its invertibility).

structure IsRegularSteadyState (N : Matrix M R ℝ) (f : R → (M → ℝ) → ℝ)
    (σ : (R → ℝ) → M → ℝ) (e₀ : R → ℝ) : Prop where
  /-- The steady state depends differentiably on the enzyme levels. -/
  differentiableAt_steady : DifferentiableAt ℝ σ e₀
  /-- The rate laws are differentiable at the steady state. -/
  differentiableAt_rate : ∀ i, DifferentiableAt ℝ (f i) (σ e₀)
  /-- `σ e` is a steady state for `e` near `e₀`. -/
  steady : ∀ᶠ e in 𝓝 e₀, N *ᵥ flux f e (σ e) = 0
  /-- The Jacobian of the steady-state equation in the concentrations is injective. -/
  regular : Function.Injective fun δ : M → ℝ =>
    N *ᵥ fun i => e₀ i * fderiv ℝ (f i) (σ e₀) δ

Uses 1 · Used by 4

Statement usesReaction fluxes proportional to enzyme levels

Used byRegular steady states exist by the implicit function theorem · Concentration summation theorem · Flux summation theorem · Flux connectivity theorem

TheoremRegular steady states exist by the implicit function theorem#✓fully proved

If s₀ is a steady state at enzyme levels e₀, the rate laws are continuously differentiable at s₀, and the Jacobian δ ↦ N (e₀ ⊙ f'(s₀) δ) is injective, then the steady state continues to a map σ with σ e₀ = s₀ satisfying IsRegularSteadyState.

theorem exists_isRegularSteadyState [Fintype M] {N : Matrix M R ℝ} {f : R → (M → ℝ) → ℝ}
    {e₀ : R → ℝ} {s₀ : M → ℝ} (hf : ∀ i, ContDiffAt ℝ 1 (f i) s₀)
    (hss : N *ᵥ flux f e₀ s₀ = 0)
    (hreg : Function.Injective fun δ : M → ℝ => N *ᵥ fun i => e₀ i * fderiv ℝ (f i) s₀ δ) :
    ∃ σ : (R → ℝ) → M → ℝ, σ e₀ = s₀ ∧ IsRegularSteadyState N f σ e₀

Uses 2

Statement usesRegular steady state of a metabolic network · Reaction fluxes proportional to enzyme levels

TheoremConcentration summation theorem#✓fully proved

Concentration summation theorem (Heinrich & Rapoport 1974): for a positive steady-state concentration s_m, ∑_i C^{s_m}_{e_i} = 0. The positivity hypothesis is the domain on which the scaled concentration control coefficients have their biological meaning.

theorem sum_concControl {N : Matrix M R ℝ} {f : R → (M → ℝ) → ℝ} {σ : (R → ℝ) → M → ℝ}
    {e₀ : R → ℝ} (h : IsRegularSteadyState N f σ e₀) (m : M) (_hm : 0 < σ e₀ m) :
    ∑ i, concControl σ e₀ m i = 0

Uses 4

Statement usesRegular steady state of a metabolic network · Concentration control coefficient

Proof usesReaction fluxes proportional to enzyme levels · Steady-state fluxes along a steady-state map

TheoremFlux summation theorem#✓fully proved

Flux summation theorem (Kacser & Burns 1973; Heinrich & Rapoport 1974): for a nonzero steady-state flux J_j, ∑_i C^{J_j}_{e_i} = 1.

theorem sum_fluxControl {N : Matrix M R ℝ} {f : R → (M → ℝ) → ℝ} {σ : (R → ℝ) → M → ℝ}
    {e₀ : R → ℝ} (h : IsRegularSteadyState N f σ e₀) {j : R}
    (hj : steadyFlux f σ e₀ j ≠ 0) :
    ∑ i, fluxControl f σ e₀ j i = 1

Uses 4

Statement usesRegular steady state of a metabolic network · Flux control coefficient · Steady-state fluxes along a steady-state map

Proof usesReaction fluxes proportional to enzyme levels

TheoremFlux connectivity theorem#✓fully proved

Flux connectivity theorem (Kacser & Burns 1973): when all steady-state fluxes are nonzero, ∑_i C^{J_j}_{e_i} ε^{v_i}_{s_m} = 0 for every flux J_j and metabolite s_m.

theorem sum_fluxControl_mul_elasticity [DecidableEq M] {N : Matrix M R ℝ}
    {f : R → (M → ℝ) → ℝ} {σ : (R → ℝ) → M → ℝ} {e₀ : R → ℝ}
    (h : IsRegularSteadyState N f σ e₀)
    (hJ : ∀ i, steadyFlux f σ e₀ i ≠ 0) (j : R) (m : M) :
    ∑ i, fluxControl f σ e₀ j i * elasticity f e₀ (σ e₀) i m = 0

Uses 5

Statement usesRegular steady state of a metabolic network · Elasticity of a reaction rate · Flux control coefficient · Steady-state fluxes along a steady-state map

Proof usesReaction fluxes proportional to enzyme levels

DefinitionFeasible fluxes of flux balance analysis#✓fully proved

The feasible fluxes of flux balance analysis: S v = b, l ≤ v ≤ u.

def fbaFeasible (S : Matrix (Fin m) (Fin n) ℝ) (l u : Fin n → ℝ) (b : Fin m → ℝ) :
    Set (Fin n → ℝ) :=
  {v | S *ᵥ v = b ∧ l ≤ v ∧ v ≤ u}

Used by 9

Used byWeak duality for flux balance analysis · Strong duality for flux balance analysis · Feasible flux balance problem attains its optimum · The FBA value is piecewise linear · Finitely many dual solutions suffice · Shadow prices · Optimal value of flux balance analysis · Concavity of the flux balance optimum in the right-hand side · Shadow prices are derivatives when unique

DefinitionOptimal value of flux balance analysis#✓fully proved

The optimal value max {c ⬝ᵥ v | S v = b, l ≤ v ≤ u} of flux balance analysis (the supremum; it is 0 by convention when the problem is infeasible).

noncomputable def fbaValue (S : Matrix (Fin m) (Fin n) ℝ) (l u c : Fin n → ℝ)
    (b : Fin m → ℝ) : ℝ :=
  sSup ((fun v => c ⬝ᵥ v) '' fbaFeasible S l u b)

Uses 1 · Used by 7

Statement usesFeasible fluxes of flux balance analysis

Used byStrong duality for flux balance analysis · Feasible flux balance problem attains its optimum · The FBA value is piecewise linear · Finitely many dual solutions suffice · Shadow prices · Concavity of the flux balance optimum in the right-hand side · Shadow prices are derivatives when unique

DefinitionDual feasibility for flux balance analysis#✓fully proved

Dual feasibility for flux balance analysis: y prices the metabolites, α, β ≥ 0 the upper and lower flux bounds, and Sᵀ y + α - β = c.

def fbaDualFeasible (S : Matrix (Fin m) (Fin n) ℝ) (c : Fin n → ℝ) (y : Fin m → ℝ)
    (α β : Fin n → ℝ) : Prop :=
  0 ≤ α ∧ 0 ≤ β ∧ Sᵀ *ᵥ y + α - β = c

Used by 6

Used byWeak duality for flux balance analysis · Strong duality for flux balance analysis · The FBA value is piecewise linear · Finitely many dual solutions suffice · Shadow prices · Shadow prices are derivatives when unique

DefinitionDual objective of flux balance analysis#✓fully proved

The dual objective b ⬝ᵥ y + u ⬝ᵥ α - l ⬝ᵥ β.

def fbaDualValue (l u : Fin n → ℝ) (b : Fin m → ℝ) (y : Fin m → ℝ) (α β : Fin n → ℝ) : ℝ :=
  b ⬝ᵥ y + u ⬝ᵥ α - l ⬝ᵥ β

Used by 6

Used byWeak duality for flux balance analysis · Strong duality for flux balance analysis · The FBA value is piecewise linear · Finitely many dual solutions suffice · Shadow prices · Shadow prices are derivatives when unique

TheoremFeasible flux balance problem attains its optimum#✓fully proved

A feasible flux balance problem attains its optimum.

theorem exists_fbaValue_eq {S : Matrix (Fin m) (Fin n) ℝ} {l u c : Fin n → ℝ}
    {b : Fin m → ℝ} (hb : (fbaFeasible S l u b).Nonempty) :
    ∃ v ∈ fbaFeasible S l u b, fbaValue S l u c b = c ⬝ᵥ v ∧
      ∀ w ∈ fbaFeasible S l u b, c ⬝ᵥ w ≤ c ⬝ᵥ v

Uses 2 · Used by 6

Statement usesFeasible fluxes of flux balance analysis · Optimal value of flux balance analysis

Used byStrong duality for flux balance analysis · The FBA value is piecewise linear · Finitely many dual solutions suffice · Shadow prices · Concavity of the flux balance optimum in the right-hand side · Shadow prices are derivatives when unique

TheoremWeak duality for flux balance analysis#✓fully proved

Weak duality for flux balance analysis.

theorem dotProduct_le_fbaDualValue {S : Matrix (Fin m) (Fin n) ℝ} {l u c : Fin n → ℝ}
    {b : Fin m → ℝ} {v : Fin n → ℝ} (hv : v ∈ fbaFeasible S l u b) {y : Fin m → ℝ}
    {α β : Fin n → ℝ} (hd : fbaDualFeasible S c y α β) :
    c ⬝ᵥ v ≤ fbaDualValue l u b y α β

Uses 3 · Used by 5

Statement usesDual feasibility for flux balance analysis · Dual objective of flux balance analysis · Feasible fluxes of flux balance analysis

Used byStrong duality for flux balance analysis · The FBA value is piecewise linear · Finitely many dual solutions suffice · Shadow prices · Shadow prices are derivatives when unique

TheoremStrong duality for flux balance analysis#✓fully proved

Strong duality for flux balance analysis: a feasible problem has a dual feasible point whose value is the optimal value.

theorem exists_fbaDualValue_eq {S : Matrix (Fin m) (Fin n) ℝ} {l u c : Fin n → ℝ}
    {b : Fin m → ℝ} (hb : (fbaFeasible S l u b).Nonempty) :
    ∃ y α β, fbaDualFeasible S c y α β ∧ fbaDualValue l u b y α β = fbaValue S l u c b

Uses 7 · Used by 2

Statement usesDual feasibility for flux balance analysis · Dual objective of flux balance analysis · Feasible fluxes of flux balance analysis · Optimal value of flux balance analysis

Proof usesStrong linear programming duality · Weak duality for flux balance analysis · Feasible flux balance problem attains its optimum

Used byFinitely many dual solutions suffice · Shadow prices

TheoremConcavity of the flux balance optimum in the right-hand side#✓fully proved

The optimal value is concave in the right-hand side b on the set of feasible b.

theorem fbaValue_concave {S : Matrix (Fin m) (Fin n) ℝ} {l u c : Fin n → ℝ}
    {b₁ b₂ : Fin m → ℝ} (h₁ : (fbaFeasible S l u b₁).Nonempty)
    (h₂ : (fbaFeasible S l u b₂).Nonempty) {t : ℝ} (ht₀ : 0 ≤ t) (ht₁ : t ≤ 1) :
    t * fbaValue S l u c b₁ + (1 - t) * fbaValue S l u c b₂ ≤
      fbaValue S l u c (t • b₁ + (1 - t) • b₂)

Uses 3

Statement usesFeasible fluxes of flux balance analysis · Optimal value of flux balance analysis

Proof usesFeasible flux balance problem attains its optimum

TheoremShadow prices#✓fully proved

Shadow prices (Orth, Thiele & Palsson 2010): at a feasible b, the metabolite prices y of the optimal dual solutions are exactly the supergradients of the optimal value: fbaValue b' ≤ fbaValue b + y ⬝ᵥ (b' - b) for every feasible b'.

theorem exists_optimal_dual_iff_supergradient {S : Matrix (Fin m) (Fin n) ℝ}
    {l u c : Fin n → ℝ} {b : Fin m → ℝ} (hb : (fbaFeasible S l u b).Nonempty) (y : Fin m → ℝ) :
    (∃ α β, fbaDualFeasible S c y α β ∧ ∀ y' α' β', fbaDualFeasible S c y' α' β' →
        fbaDualValue l u b y α β ≤ fbaDualValue l u b y' α' β') ↔
      ∀ b', (fbaFeasible S l u b').Nonempty →
        fbaValue S l u c b' ≤ fbaValue S l u c b + y ⬝ᵥ (b' - b)

Uses 7

Statement usesDual feasibility for flux balance analysis · Dual objective of flux balance analysis · Feasible fluxes of flux balance analysis · Optimal value of flux balance analysis

Proof usesWeak duality for flux balance analysis · Strong duality for flux balance analysis · Feasible flux balance problem attains its optimum

TheoremUniqueness of Sinkhorn scaling#✓fully proved

Two diagonal scalings of a positive matrix to doubly stochastic form differ by a positive scalar.

theorem sinkhorn_scaling_unique {n : ℕ} {A : Matrix (Fin n) (Fin n) ℝ}
    (hA : ∀ i j, 0 < A i j) {r c r' c' : Fin n → ℝ} (hr : ∀ i, 0 < r i) (hc : ∀ j, 0 < c j)
    (hr' : ∀ i, 0 < r' i) (hc' : ∀ j, 0 < c' j)
    (h : (fun i j => r i * A i j * c j) ∈ doublyStochastic ℝ (Fin n))
    (h' : (fun i j => r' i * A i j * c' j) ∈ doublyStochastic ℝ (Fin n)) :
    ∃ t : ℝ, 0 < t ∧ r' = t • r ∧ c' = t⁻¹ • c

Used by 1

Used bySymmetric matrix balancing

TheoremSymmetric matrix balancing#✓fully proved

Symmetric matrix balancing (Sinkhorn 1964; the "equal visibility" normalization of Imakaev et al. 2012): a symmetric matrix with positive entries has a unique positive vector d with diag(d) A diag(d) doubly stochastic.

theorem existsUnique_symmetric_balancing {n : ℕ} {A : Matrix (Fin n) (Fin n) ℝ}
    (hsymm : A.IsSymm) (hA : ∀ i j, 0 < A i j) :
    ∃! d : Fin n → ℝ, (∀ i, 0 < d i) ∧
      (fun i j => d i * A i j * d j) ∈ doublyStochastic ℝ (Fin n)

Uses 2

Proof usesUniqueness of Sinkhorn scaling · Sinkhorn's scaling theorem

DefinitionTotal support of a square matrix#✓fully proved

A square matrix has total support if it is nonzero and every positive entry lies on a positive diagonal: for A i j > 0 there is a permutation σ with σ i = j and A k (σ k) > 0 for all k (Sinkhorn & Knopp 1967; Csima & Datta 1972).

def HasTotalSupport {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) : Prop :=
  A ≠ 0 ∧ ∀ i j, 0 < A i j → ∃ σ : Equiv.Perm (Fin n), σ i = j ∧ ∀ k, 0 < A k (σ k)

Used by 3

Used byNecessity of total support · Csima–Datta theorem · Csima–Datta: sufficiency of total support

TheoremNecessity of total support#✓fully proved

Necessity of total support (Sinkhorn & Knopp 1967; Csima & Datta 1972): if a positive diagonal scaling diag(d) A diag(d) is doubly stochastic, then A has total support. The proof uses Birkhoff's theorem. The converse for symmetric nonnegative A is exists_symmetric_balancing_of_hasTotalSupport.

theorem hasTotalSupport_of_balancing {n : ℕ} (hn : 0 < n) {A : Matrix (Fin n) (Fin n) ℝ}
    {d : Fin n → ℝ} (hd : ∀ i, 0 < d i)
    (h : (fun i j => d i * A i j * d j) ∈ doublyStochastic ℝ (Fin n)) : HasTotalSupport A

Uses 1 · Used by 1

Statement usesTotal support of a square matrix

Used byCsima–Datta theorem

DefinitionInteraction graph of a Boolean network#✓fully proved

In the interaction graph of f : {0,1}ⁿ → {0,1}ⁿ there is an edge j → i when the i-th coordinate of f depends on the j-th variable.

def Influences (f : (Fin n → Bool) → Fin n → Bool) (j i : Fin n) : Prop :=
  ∃ x, f (Function.update x j (!x j)) i ≠ f x i

Used by 2

Used byAcyclic interaction graph · Robert's theorem

DefinitionAcyclic interaction graph#✓fully proved

The interaction graph of f has no directed cycle (loops included).

def IsAcyclic (f : (Fin n → Bool) → Fin n → Bool) : Prop :=
  ∀ i, ¬ Relation.TransGen (Influences f) i i

Uses 1 · Used by 1

Statement usesInteraction graph of a Boolean network

Used byRobert's theorem

TheoremRobert's theorem#✓fully proved

Robert's theorem (Robert 1980): if the interaction graph of f : {0,1}ⁿ → {0,1}ⁿ is acyclic, f has a unique fixed point p, and every synchronous trajectory reaches it within n steps.

theorem robert_fixed_point {f : (Fin n → Bool) → Fin n → Bool} (hf : IsAcyclic f) :
    ∃ p, f p = p ∧ (∀ q, f q = q → q = p) ∧ ∀ x, f^[n] x = p

Uses 2

Statement usesAcyclic interaction graph

Proof usesInteraction graph of a Boolean network

DefinitionSpanning in-tree rooted at a state#✓fully proved

t : ι → ι is a spanning in-tree rooted at r (each i ≠ r points to its parent t i): t r = r and iterating t from any state reaches r.

def IsInTree (r : ι) (t : ι → ι) : Prop :=
  t r = r ∧ ∀ i, ∃ k, t^[k] i = r

Used by 3

Used byTotal weight of spanning in-trees · In-tree weights of an irreducible rate matrix are positive · Markov chain tree theorem

DefinitionTotal weight of spanning in-trees#✓fully proved

The total weight ∑_t ∏_{i ≠ r} Q i (t i) of the spanning in-trees rooted at r.

noncomputable def treeWeight (Q : Matrix ι ι ℝ) (r : ι) : ℝ := by
  classical
  exact ∑ t ∈ univ.filter (IsInTree r), ∏ i ∈ univ.erase r, Q i (t i)

Uses 1 · Used by 3

Statement usesSpanning in-tree rooted at a state

Used byUniqueness in the Markov chain tree theorem · In-tree weights of an irreducible rate matrix are positive · Markov chain tree theorem

DefinitionIrreducible rate matrix#✓fully proved

A rate matrix is irreducible if every state reaches every other state through positive jump rates.

def IsIrreducible (Q : Matrix ι ι ℝ) : Prop :=
  ∀ i j, Relation.ReflTransGen (fun a b => a ≠ b ∧ 0 < Q a b) i j

Used by 2

Used byUniqueness in the Markov chain tree theorem · In-tree weights of an irreducible rate matrix are positive

TheoremMarkov chain tree theorem#✓fully proved

Markov chain tree theorem (King & Altman 1956; Hill 1966): the in-tree weights are invariant for every matrix with zero row sums, w Q = 0. The proof matches both sides with the maps g : ι → ι whose functional graph has its cycle through j (Anantharam & Tsoucas 1989).

theorem treeWeight_vecMul_eq_zero {Q : Matrix ι ι ℝ} (hQ : ∀ i, ∑ j, Q i j = 0) :
    treeWeight Q ᵥ* Q = 0

Uses 2 · Used by 1

Statement usesTotal weight of spanning in-trees

Proof usesSpanning in-tree rooted at a state

Used byUniqueness in the Markov chain tree theorem

TheoremIn-tree weights of an irreducible rate matrix are positive#✓fully proved

For an irreducible rate matrix every in-tree weight is positive.

theorem treeWeight_pos {Q : Matrix ι ι ℝ} (hQ : ProbabilityTheory.IsRateMatrix Q)
    (hirr : IsIrreducible Q) (r : ι) : 0 < treeWeight Q r

Uses 4 · Used by 1

Statement usesIrreducible rate matrix · Total weight of spanning in-trees · Rate matrix

Proof usesSpanning in-tree rooted at a state

Used byUniqueness in the Markov chain tree theorem

TheoremUniqueness in the Markov chain tree theorem#✓fully proved

For an irreducible rate matrix every invariant vector is a multiple of the in-tree weights: the stationary law is proportional, at each state, to the weight of the spanning in-trees rooted there.

theorem eq_smul_treeWeight_of_vecMul_eq_zero {Q : Matrix ι ι ℝ}
    (hQ : ProbabilityTheory.IsRateMatrix Q) (hirr : IsIrreducible Q) {π : ι → ℝ}
    (hπ : π ᵥ* Q = 0) : ∃ a : ℝ, π = a • treeWeight Q

Uses 5

Statement usesIrreducible rate matrix · Total weight of spanning in-trees · Rate matrix

Proof usesIn-tree weights of an irreducible rate matrix are positive · Markov chain tree theorem

TheoremFinitely many dual solutions suffice#✓fully proved

There is a finite set T of pairs (y, u ⬝ᵥ α - l ⬝ᵥ β) with (y, α, β) dual feasible, such that for every feasible b some pair in T is optimal: y ⬝ᵥ b + κ = fbaValue S l u c b.

theorem exists_finset_optimal_fbaDual (S : Matrix (Fin m) (Fin n) ℝ) (l u c : Fin n → ℝ) :
    ∃ T : Finset ((Fin m → ℝ) × ℝ),
      (∀ p ∈ T, ∃ α β, fbaDualFeasible S c p.1 α β ∧ p.2 = u ⬝ᵥ α - l ⬝ᵥ β) ∧
      ∀ b : Fin m → ℝ, (fbaFeasible S l u b).Nonempty →
        ∃ p ∈ T, p.1 ⬝ᵥ b + p.2 = fbaValue S l u c b

Uses 7 · Used by 2

Statement usesDual feasibility for flux balance analysis · Feasible fluxes of flux balance analysis · Optimal value of flux balance analysis

Proof usesWeak duality for flux balance analysis · Strong duality for flux balance analysis · Feasible flux balance problem attains its optimum · Dual objective of flux balance analysis

Used byThe FBA value is piecewise linear · Shadow prices are derivatives when unique

TheoremThe FBA value is piecewise linear#✓fully proved

There are finitely many affine functions b ↦ y ⬝ᵥ b + κ whose minimum is the optimal value at every feasible right-hand side b.

theorem exists_finset_isLeast_fbaValue (S : Matrix (Fin m) (Fin n) ℝ)
    (l u c : Fin n → ℝ) :
    ∃ T : Finset ((Fin m → ℝ) × ℝ), ∀ b : Fin m → ℝ, (fbaFeasible S l u b).Nonempty →
      IsLeast ((fun p : (Fin m → ℝ) × ℝ => p.1 ⬝ᵥ b + p.2) '' (T : Set _))
        (fbaValue S l u c b)

Sources

• Rockafellar (1970), Thm 19.3; Orth, Thiele & Palsson (2010).

Uses 7

Statement usesFeasible fluxes of flux balance analysis · Optimal value of flux balance analysis

Proof usesWeak duality for flux balance analysis · Feasible flux balance problem attains its optimum · Finitely many dual solutions suffice · Dual feasibility for flux balance analysis · Dual objective of flux balance analysis

TheoremShadow prices are derivatives when unique#✓fully proved

If b is an interior point of the set of feasible right-hand sides and y is the only metabolite price vector of an optimal dual solution, then the optimal value is differentiable at b with derivative b' ↦ y ⬝ᵥ b'.

theorem hasFDerivAt_fbaValue_of_unique {S : Matrix (Fin m) (Fin n) ℝ}
    {l u c : Fin n → ℝ} {b : Fin m → ℝ}
    (hb : b ∈ interior {b' : Fin m → ℝ | (fbaFeasible S l u b').Nonempty}) {y : Fin m → ℝ}
    (huniq : ∀ y' : Fin m → ℝ, (∃ α β, fbaDualFeasible S c y' α β ∧
        ∀ y'' α'' β'', fbaDualFeasible S c y'' α'' β'' →
          fbaDualValue l u b y' α β ≤ fbaDualValue l u b y'' α'' β'') ↔ y' = y) :
    HasFDerivAt (fbaValue S l u c)
      (∑ i, y i • ContinuousLinearMap.proj (R := ℝ) (φ := fun _ : Fin m => ℝ) i) b

Sources

• Rockafellar (1970), Thm 25.1; Orth, Thiele & Palsson (2010).

Uses 7

Statement usesDual feasibility for flux balance analysis · Dual objective of flux balance analysis · Feasible fluxes of flux balance analysis · Optimal value of flux balance analysis

Proof usesWeak duality for flux balance analysis · Feasible flux balance problem attains its optimum · Finitely many dual solutions suffice

45 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.