SolutionUniqueness.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem326.IsForwardSolutionOn.eqOn line 13

Source documentation

Uniqueness for finite forward solutions, including both endpoints.

theorem IsForwardSolutionOn.eqOn
    (hv : LocallyLipschitz (massAction N κ)) (hT : 0 ≤ T)
    (hx : IsForwardSolutionOn N κ z T x)
    (hy : IsForwardSolutionOn N κ z T y) :
    Set.EqOn x y (Set.Icc (0 : ℝ) T) :=
…

Mentions: OAI.Problem326.massAction, OAI.Problem326.IsForwardSolutionOn

theorem OAI.Problem326.isForwardInvariant_of_global_trajectories line 23
Source documentation
One invariant global trajectory from each initial point suffices for the full finite-segment and extension definition of forward invariance.
```
theorem isForwardInvariant_of_global_trajectories
    (hv : LocallyLipschitz (massAction N κ)) {K : Set (Fin d → ℝ)}
    (hK : ∀ z ∈ K, ∃ x : ℝ → (Fin d → ℝ),
      IsGlobalForwardSolution N κ z x ∧ ∀ t : ℝ, 0 ≤ t → x t ∈ K) :
    IsForwardInvariant N κ K := by
…
```
Mentions: OAI.Problem326.massAction, OAI.Problem326.IsGlobalForwardSolution, OAI.Problem326.IsForwardInvariant