BarrierInvariance.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem326.BarrierConstruction.AffineBarrierData.isForwardInvariant line 20
Source documentation
The exact forward-invariance predicate follows from the constructed barrier, with no separate global-solvability or regularity assumption.
```
theorem isForwardInvariant (A : AffineBarrierData N κ x₀) :
    Problem326.IsForwardInvariant N κ A.plateau := by
…
```
Mentions: OAI.Problem326.BarrierConstruction.AffineBarrierData, OAI.Problem326.IsForwardInvariant
theorem OAI.Problem326.BarrierConstruction.compact_convex_invariant_polytope_of_uniform line 68
Source documentation
Uniform arbitrary-tolerance affine approximation gives a compact convex forward-invariant polytope with extension of every finite solution segment.
```
theorem compact_convex_invariant_polytope_of_uniform {d : ℕ}
    (happroximation : UniformAffineApproximation d)
    (N : ReactionNetwork d) (κ : Reaction N → ℝ)
    (hweak : WeaklyReversible N) (hκ : ∀ e, 0 < κ e)
    (x₀ : Fin d → ℝ) (hx₀ : PositiveState x₀) :
    ∃ K : Set (Fin d → ℝ), IsCompact K ∧ Convex ℝ K ∧ IsFinitePolyhedron K ∧
      x₀ ∈ K ∧ K ⊆ {x | PositiveState x} ∧ IsForwardInvariant N κ K := by
…
```
Mentions: OAI.Problem326.BarrierConstruction.UniformAffineApproximation, OAI.Problem326.ReactionNetwork, OAI.Problem326.Reaction, OAI.Problem326.WeaklyReversible, OAI.Problem326.PositiveState, OAI.Problem326.IsFinitePolyhedron, OAI.Problem326.IsForwardInvariant