OAI/Analysis/MassAction/CompactInvariance.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem326.global_bounds_of_compact_invariant line 13

   Source documentation

   The quantitative global conclusion only needs a compact positive forward-invariant set, not its polyhedral or convex structure.

   theorem global_bounds_of_compact_invariant {d : ℕ}
       (N : ReactionNetwork d) (κ : Reaction N → ℝ) (x0 : Fin d → ℝ)
       {K : Set (Fin d → ℝ)} (hK : IsCompact K) (hx0 : x0 ∈ K)
       (hpos : K ⊆ {x | PositiveState x}) (hinv : IsForwardInvariant N κ K) :
       ∃ ε : ℝ, 0 < ε ∧ ε < 1 ∧
         (∃ x : ℝ → (Fin d → ℝ), IsGlobalForwardSolution N κ x0 x) ∧
         ∀ x : ℝ → (Fin d → ℝ), IsGlobalForwardSolution N κ x0 x →
           ∀ t : ℝ, 0 ≤ t → ∀ i : Fin d, ε ≤ x t i ∧ x t i ≤ ε⁻¹ := by
   …

   Mentions: OAI.Problem326.ReactionNetwork, OAI.Problem326.Reaction, OAI.Problem326.PositiveState, OAI.Problem326.IsForwardInvariant, OAI.Problem326.IsGlobalForwardSolution