MassActionDot.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem326.dot_massAction line 11
Source documentation
Pairing the mass-action vector field with a fixed normal commutes with its finite reaction sum. This is the algebraic bridge to ordered-cut flux.
```
theorem dot_massAction {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.hasDerivAt_dot line 29

Source documentation

The derivative of a fixed linear functional along a differentiable curve.

theorem hasDerivAt_dot {d : ℕ} {x : ℝ → (Fin d → ℝ)}
    {v : Fin d → ℝ} {t : ℝ} (hx : HasDerivAt x v t)
    (r : Fin d → ℝ) :
    HasDerivAt (fun s => dot r (x s)) (dot r v) t := by
…

Mentions: OAI.Problem326.dot

theorem OAI.Problem326.hasDerivAt_affineLabel line 38

Source documentation

Affine labels have the expected derivative along solution curves.

theorem hasDerivAt_affineLabel {d : ℕ} {x : ℝ → (Fin d → ℝ)}
    {v : Fin d → ℝ} {t : ℝ} (hx : HasDerivAt x v t)
    (r : Fin d → ℝ) (c : ℝ) :
    HasDerivAt (fun s => dot r (x s) + c) (dot r v) t := by
…

Mentions: OAI.Problem326.dot

theorem OAI.Problem326.IsForwardSolutionOn.hasDerivAt_affineLabel line 46

Source documentation

The derivative of an affine label along a local mass-action solution, expressed in the scalar form used by the finite graph estimate.

theorem IsForwardSolutionOn.hasDerivAt_affineLabel {d : ℕ}
    {N : ReactionNetwork d} {κ : Reaction N → ℝ}
    {x0 : Fin d → ℝ} {T : ℝ} {x : ℝ → (Fin d → ℝ)}
    (hx : IsForwardSolutionOn N κ x0 T x) {t : ℝ}
    (ht : t ∈ Set.Ioo (0 : ℝ) T) (r : Fin d → ℝ) (c : ℝ) :
    HasDerivAt (fun s => dot r (x s) + c)
      (∑ e : Reaction N, κ e * monomial (x t) e.val.1 *
        (dot r (fun i => (e.val.2 i : ℝ)) -
          dot r (fun i => (e.val.1 i : ℝ)))) t := by
…

Mentions: OAI.Problem326.ReactionNetwork, OAI.Problem326.Reaction, OAI.Problem326.IsForwardSolutionOn, OAI.Problem326.dot, OAI.Problem326.monomial