GlueCurves.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem326.glue_hasDerivAt_of_open_cover line 16

Source documentation

Compatible differentiable curves on an open cover glue to one curve. The vector field may depend on time, and ordinary two-sided derivatives are preserved at all points.

theorem glue_hasDerivAt_of_open_cover {ι : Type uIota} {E : Type uE}
    [NormedAddCommGroup E] [NormedSpace ℝ E]
    (U : ι → Set ℝ) (hopen : ∀ i, IsOpen (U i))
    (hcover : ∀ t, ∃ i, t ∈ U i) (curve : ι → ℝ → E)
    (hcompat : ∀ i j, Set.EqOn (curve i) (curve j) (U i ∩ U j))
    (v : ℝ → E → E)
    (hderiv : ∀ i t, t ∈ U i → HasDerivAt (curve i) (v t (curve i t)) t) :
    ∃ x : ℝ → E, (∀ i, Set.EqOn x (curve i) (U i)) ∧
      ∀ t, HasDerivAt x (v t (x t)) t := by
…

theorem OAI.Problem326.symmetric_intervals_cover line 41
Source documentation
A family on expanding symmetric intervals is an open cover of real time.
```
theorem symmetric_intervals_cover (t : ℝ) :
    ∃ n : ℕ, t ∈ Set.Ioo (-(n : ℝ) - 1) ((n : ℝ) + 1) := by
…
```

theorem OAI.Problem326.glue_hasDerivAt_on_symmetric_intervals line 52

Source documentation

The countable-interval specialization used to globalize finite-horizon ODE solutions without losing differentiability at time zero.

theorem glue_hasDerivAt_on_symmetric_intervals {E : Type uE}
    [NormedAddCommGroup E] [NormedSpace ℝ E]
    (curve : ℕ → ℝ → E) (v : ℝ → E → E)
    (hcompat : ∀ m n, Set.EqOn (curve m) (curve n)
      (Set.Ioo (-(m : ℝ) - 1) ((m : ℝ) + 1) ∩
       Set.Ioo (-(n : ℝ) - 1) ((n : ℝ) + 1)))
    (hderiv : ∀ (n : ℕ) (t : ℝ), t ∈ Set.Ioo (-(n : ℝ) - 1) ((n : ℝ) + 1) →
      HasDerivAt (curve n) (v t (curve n t)) t) :
    ∃ x : ℝ → E,
      (∀ n, Set.EqOn x (curve n) (Set.Ioo (-(n : ℝ) - 1) ((n : ℝ) + 1))) ∧
      ∀ t, HasDerivAt x (v t (x t)) t :=
…