JetVolterraFixedPoint.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

A short-time Volterra contraction on continuous curves of bounded spatial jets.

theorem OAI.ForcedComputation.JetVolterra.affine_contracting line 17
def OAI.ForcedComputation.JetVolterra.solution line 27
Source documentation
The unique solution of the short-time linear Volterra equation.
```
def solution (a : A) (L : A →L[ℝ] A) (hL : ‖L‖ < 1) : A :=
…
```
theorem OAI.ForcedComputation.JetVolterra.solution_eq line 30
theorem OAI.ForcedComputation.JetVolterra.solution_unique line 34
theorem OAI.ForcedComputation.JetVolterra.exists_unique line 38
theorem OAI.ForcedComputation.JetVolterra.norm_solution_le line 43
theorem OAI.ForcedComputation.JetVolterra.solution_source_lipschitz line 49
Source documentation
Stability with respect to the inhomogeneous source, in the same path norm.
```
theorem solution_source_lipschitz (a b : A) (L : A →L[ℝ] A) (hL : ‖L‖ < 1) :
    ‖solution A a L hL - solution A b L hL‖ ≤ ‖a - b‖ / (1 - ‖L‖) := by
…
```
Mentions: OAI.ForcedComputation.JetVolterra.solution

theorem OAI.ForcedComputation.JetVolterra.solution_map line 59

Source documentation

An intertwining bounded linear map carries the high-order solution to the lower one.

theorem solution_map (a : A) (L : A →L[ℝ] A) (hL : ‖L‖ < 1)
    (P : A →L[ℝ] D) (M : D →L[ℝ] D) (hM : ‖M‖ < 1)
    (hcomm : P.comp L = M.comp P) :
    P (solution A a L hL) = solution D (P a) M hM := by
…

Mentions: OAI.ForcedComputation.JetVolterra.solution

def OAI.ForcedComputation.JetVolterra.Path line 78
Source documentation
Continuous finite-order jet curves on a closed short-time interval.
```
def Path (k : ℕ) (T : ℝ) := C(Set.Icc (0 : ℝ) T, BoundedSpatialJets.Space E F k)
```
Mentions: OAI.ForcedComputation.BoundedSpatialJets.Space
instance OAI.ForcedComputation.JetVolterra.(instance at line 80) line 80
instance OAI.ForcedComputation.JetVolterra.(instance at line 84) line 84
instance OAI.ForcedComputation.JetVolterra.(instance at line 87) line 87
def OAI.ForcedComputation.JetVolterra.pathEquiv line 90
instance OAI.ForcedComputation.JetVolterra.(instance at line 94) line 94
def OAI.ForcedComputation.JetVolterra.pathTruncate line 99
Source documentation
Pointwise truncation of continuous jet curves.
```
def pathTruncate (k n : ℕ) (hkn : k ≤ n) (T : ℝ) :
    Path E F n T →L[ℝ] Path E F k T :=
…
```
Mentions: OAI.ForcedComputation.JetVolterra.Path
theorem OAI.ForcedComputation.JetVolterra.pathTruncate_apply line 106
theorem OAI.ForcedComputation.JetVolterra.norm_pathTruncate_le_one line 110
theorem OAI.ForcedComputation.JetVolterra.exists_unique_path line 124
Source documentation
The abstract Volterra equation is uniquely solvable in the actual continuous jet-path space.
```
theorem exists_unique_path (k : ℕ) (T : ℝ) (a : Path E F k T)
    (L : Path E F k T →L[ℝ] Path E F k T) (hL : ‖L‖ < 1) :
    ∃! u : Path E F k T, u = a + L u := exists_unique _ a L hL
```
Mentions: OAI.ForcedComputation.JetVolterra.Path, OAI.ForcedComputation.JetVolterra.exists_unique

theorem OAI.ForcedComputation.JetVolterra.solution_truncate line 129

Source documentation

Compatible integral operators give compatible solutions across finite spatial orders.

theorem solution_truncate (k n : ℕ) (hkn : k ≤ n) (T : ℝ) (a : Path E F n T)
    (L : Path E F n T →L[ℝ] Path E F n T) (hL : ‖L‖ < 1)
    (M : Path E F k T →L[ℝ] Path E F k T) (hM : ‖M‖ < 1)
    (hcomm : (pathTruncate E F k n hkn T).comp L =
      M.comp (pathTruncate E F k n hkn T)) :
    pathTruncate E F k n hkn T (solution _ a L hL) =
      solution _ (pathTruncate E F k n hkn T a) M hM :=
…

Mentions: OAI.ForcedComputation.JetVolterra.Path, OAI.ForcedComputation.JetVolterra.pathTruncate, OAI.ForcedComputation.JetVolterra.solution