OAI/Analysis/MassAction/LocalExistence.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem326.exists_local_solution_of_contDiffAt line 15

   Source documentation

   A continuously differentiable autonomous vector field admits a solution on a closed interval of positive length, with ordinary derivatives at both endpoints.

   theorem exists_local_solution_of_contDiffAt
       {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
       {f : E → E} {z : E} (hf : ContDiffAt ℝ 1 f z) (t₀ : ℝ) :
       ∃ T : ℝ, 0 < T ∧ ∃ x : ℝ → E, x t₀ = z ∧
         ∀ t ∈ Icc (t₀ - T) (t₀ + T), HasDerivAt x (f (x t)) t := by
   …

2. theorem OAI.Problem326.exists_uniform_local_solution_on_compact line 29

   Source documentation

   The local existence time can be chosen uniformly over a compact set of initial states. This supplies fixed-size steps for compact trapping arguments.

   theorem exists_uniform_local_solution_on_compact
       {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
       {f : E → E} (hf : ContDiff ℝ 1 f) {K : Set E} (hK : IsCompact K)
       (t₀ : ℝ) :
       ∃ T : ℝ, 0 < T ∧ ∀ z ∈ K, ∃ x : ℝ → E, x t₀ = z ∧
         ∀ t ∈ Icc (t₀ - T) (t₀ + T), HasDerivAt x (f (x t)) t := by
   …