BarrierTrapping.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem326.Barrier.affineMinimum line 15
Source documentation
The finite affine minimum used as a barrier. All minimizing labels are active; no tie-breaking convention is built into this definition.
```
def affineMinimum {d : ℕ} {ι : Type uIota} (s : Finset ι) (hs : s.Nonempty)
    (a : ι → Fin d → ℝ) (c : ι → ℝ) (z : Fin d → ℝ) : ℝ :=
…
```

theorem OAI.Problem326.Barrier.affine_minimum_traps_segment line 22

Source documentation

Finite-segment trapping for a vector field with nonnegative derivatives of every active affine branch. This theorem does not assume a global solution or any reaction-network property: those enter only when supplying hactive.

theorem affine_minimum_traps_segment
    {d : ℕ} {ι : Type uIota} (s : Finset ι) (hs : s.Nonempty)
    (a : ι → Fin d → ℝ) (c : ι → ℝ)
    {B : Set (Fin d → ℝ)} {M T : ℝ}
    {f : (Fin d → ℝ) → (Fin d → ℝ)} {x : ℝ → (Fin d → ℝ)}
    (hT : 0 ≤ T) (hB : IsClosed B)
    (hceil : ∀ z, affineMinimum s hs a c z ≤ M)
    (hboundary : ∀ z ∈ frontier B, affineMinimum s hs a c z ≠ M)
    (hactive : ∀ z ∈ B, ∀ i ∈ s,
      dot (a i) z + c i = affineMinimum s hs a c z →
      0 ≤ dot (a i) (f z))
    (hx : ContinuousOn x (Set.Icc 0 T))
…

Mentions: OAI.Problem326.Barrier.affineMinimum, OAI.Problem326.dot

theorem OAI.Problem326.Barrier.forward_solution_trapped line 55