ClampExtension.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem326.coordinateClamp line 12
Source documentation
Coordinatewise projection onto a closed finite-dimensional box.
```
def coordinateClamp {ι : Type uIota} (a b : ι → ℝ) (hab : a ≤ b)
    (x : ι → ℝ) : ι → ℝ :=
…
```
theorem OAI.Problem326.coordinateClamp_mem line 16
theorem OAI.Problem326.coordinateClamp_eq_self line 24
theorem OAI.Problem326.coordinateClamp_lipschitz line 29

theorem OAI.Problem326.exists_bounded_lipschitz_extension line 49

Source documentation

A continuously differentiable field has a globally bounded, globally Lipschitz extension of its restriction to any nonempty closed box. This permits global ODE existence to be separated from first-exit trapping.

theorem exists_bounded_lipschitz_extension {ι : Type uIota} {F : Type uF} [Fintype ι]
    [NormedAddCommGroup F] [NormedSpace ℝ F]
    {f : (ι → ℝ) → F} (hf : ContDiff ℝ 1 f)
    (a b : ι → ℝ) (hab : a ≤ b) :
    ∃ (g : (ι → ℝ) → F) (K : NNReal) (L : ℝ), 0 < L ∧
      LipschitzWith K g ∧ (∀ x, ‖g x‖ ≤ L) ∧ Set.EqOn g f (Set.Icc a b) := by
…