FlowPointwise.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Pointwise calculus on the compact path space used in the local flow proof. The continuous linear map below lifts a continuously varying linear map to continuous paths. No differential-equation hypothesis is used here.

def OAI.ForcedComputation.Flow.applyPath line 22
Source documentation
Apply a continuous family of linear maps pointwise to a path.
```
def applyPath (A : C(K, E →L[ℝ] F)) : C(K, E) →L[ℝ] C(K, F) :=
…
```
theorem OAI.ForcedComputation.Flow.applyPath_apply line 43
theorem OAI.ForcedComputation.Flow.applyPath_norm line 46
def OAI.ForcedComputation.Flow.applyPathL line 50
Source documentation
Pointwise application depends continuously and linearly on the family.
```
def applyPathL : C(K, E →L[ℝ] F) →L[ℝ] (C(K, E) →L[ℝ] C(K, F)) :=
…
```
theorem OAI.ForcedComputation.Flow.applyPathL_apply line 68

theorem OAI.ForcedComputation.Flow.remainder_bound line 72

Source documentation

A uniform derivative modulus bounds the first-order remainder on a segment.

theorem remainder_bound {f : E → F} {df : E → E →L[ℝ] F}
    (hf : ∀ z, HasFDerivAt f (df z) z) (x y : E) {ε : ℝ}
    (hε : ∀ z ∈ segment ℝ x y, ‖df z - df x‖ ≤ ε) :
    ‖f y - f x - df x (y - x)‖ ≤ ε * ‖y - x‖ := by
…