MassActionRegularity.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem326.contDiff_monomial line 10
Source documentation
Every mass-action monomial is smooth on the whole ambient real space.
```
theorem contDiff_monomial {d : ℕ} (y : Fin d → ℕ) :
    ContDiff ℝ ⊤ (fun x : Fin d → ℝ => monomial x y) := by
…
```
Mentions: OAI.Problem326.monomial
theorem OAI.Problem326.contDiff_massAction line 16
Source documentation
The mass-action vector field is polynomial, hence globally smooth.
```
theorem contDiff_massAction {d : ℕ} (N : ReactionNetwork d)
    (κ : Reaction N → ℝ) : ContDiff ℝ ⊤ (massAction N κ) := by
…
```
Mentions: OAI.Problem326.ReactionNetwork, OAI.Problem326.Reaction, OAI.Problem326.massAction
theorem OAI.Problem326.contDiff_one_massAction line 21
theorem OAI.Problem326.locallyLipschitz_massAction line 25