MassActionFlux.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Application of the finite directed-cut inequality to the exact qualified mass-action vector field.

theorem OAI.Problem326.dot_massAction_eq_flux line 17
Source documentation
Pairing the mass-action field with a normal gives the corresponding weighted difference of complex levels.
```
theorem dot_massAction_eq_flux {d : ℕ} (N : ReactionNetwork d)
    (κ : Reaction N → ℝ) (x r : Fin d → ℝ) :
    dot r (massAction N κ x) =
      ∑ e : Reaction N, κ e * monomial x e.val.1 *
        (dot r (fun i => (e.val.2 i : ℝ)) - dot r (fun i => (e.val.1 i : ℝ))) := by
…
```
Mentions: OAI.Problem326.ReactionNetwork, OAI.Problem326.Reaction, OAI.Problem326.dot, OAI.Problem326.massAction, OAI.Problem326.monomial

theorem OAI.Problem326.massAction_inward_of_monomial_order line 35

Source documentation

All-pairs monomial domination for the network supplies an inward mass-action derivative in the specified direction. Positivity of species and rates is the only analytical input to this finite estimate.

theorem massAction_inward_of_monomial_order {d : ℕ} (N : ReactionNetwork d)
    (κ : Reaction N → ℝ) (x r : Fin d → ℝ) (δ : ℝ)
    (hweak : WeaklyReversible N) (hx : PositiveState x)
    (hκ : ∀ e, 0 < κ e) (hδ : 0 ≤ δ)
    (horder : ∀ y ∈ N.complexes, ∀ z ∈ N.complexes,
      dot r (fun i => (y i : ℝ)) < dot r (fun i => (z i : ℝ)) →
      monomial x z ≤ δ * monomial x y)
    (hrate : ∀ e, δ * (∑ f, κ f) < κ e) :
    0 ≤ dot r (massAction N κ x) := by
…

Mentions: OAI.Problem326.ReactionNetwork, OAI.Problem326.Reaction, OAI.Problem326.WeaklyReversible, OAI.Problem326.PositiveState, OAI.Problem326.dot, OAI.Problem326.monomial, OAI.Problem326.massAction