BoundedSpatialJetCurves.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform spatial derivative estimates give continuous coefficient curves in jet norm.

theorem OAI.ForcedComputation.BoundedSpatialJets.norm_sub_le_of_jets line 15

theorem OAI.ForcedComputation.BoundedSpatialJets.lipschitzWith_of_jets line 25

Source documentation

A common modulus for each derivative controls the Banach-space distance.

theorem lipschitzWith_of_jets {A : Type*} [PseudoMetricSpace A] (k : ℕ)
    (J : A → Space E F k) (L : ℝ≥0)
    (h : ∀ s t (i : Fin (k+1)) (x : E),
      ‖(J s).val i x - (J t).val i x‖ ≤ L * dist s t) : LipschitzWith L J := by
…

Mentions: OAI.ForcedComputation.BoundedSpatialJets.Space

def OAI.ForcedComputation.BoundedSpatialJets.ofFunctionCurve line 36

Source documentation

Bounded derivatives on a compact time interval, with a uniform time modulus.

def ofFunctionCurve (k : ℕ) (T : ℝ) (f : ℝ → E → F)
    (hf : ∀ t ∈ Set.Icc (0 : ℝ) T, ContDiff ℝ k (f t)) (C : ℝ)
    (hC : ∀ t ∈ Set.Icc (0 : ℝ) T, ∀ n ≤ k, ∀ x, ‖iteratedFDeriv ℝ n (f t) x‖ ≤ C)
    (L : ℝ≥0)
    (hL : ∀ s ∈ Set.Icc (0 : ℝ) T, ∀ t ∈ Set.Icc (0 : ℝ) T, ∀ n ≤ k, ∀ x,
      ‖iteratedFDeriv ℝ n (f s) x - iteratedFDeriv ℝ n (f t) x‖ ≤ L * |s-t|) :
    C(Set.Icc (0 : ℝ) T, Space E F k) where
…

Mentions: OAI.ForcedComputation.BoundedSpatialJets.Space

theorem OAI.ForcedComputation.BoundedSpatialJets.function_ofFunctionCurve line 53