BoundedSpatialJets.lean`

30 declarations, 0 contain sorry, 0 declared as axioms

A Banach space of bounded continuous spatial jets of any finite order.

The ambient space is a finite product with the maximum of the uniform norms. Compatibility of consecutive jets is imposed by closed derivative graphs, so uniform convergence of every jet preserves the spatial derivatives.

def OAI.ForcedComputation.BoundedSpatialJets.Value line 24
Source documentation
Values of the spatial derivative of order n. The type synonym fixes one normed-space structure throughout the jet family.
```
def Value (n : ℕ) := ContinuousMultilinearMap ℝ (fun _ : Fin n => E) F
```
instance OAI.ForcedComputation.BoundedSpatialJets.(instance at line 26) line 26
instance OAI.ForcedComputation.BoundedSpatialJets.(instance at line 29) line 29
instance OAI.ForcedComputation.BoundedSpatialJets.(instance at line 32) line 32
def OAI.ForcedComputation.BoundedSpatialJets.curryMap line 36
Source documentation
Split the first slot of a jet value, with the fixed normed-space structures.
```
def curryMap (n : ℕ) : Value E F (n + 1) ≃ₗᵢ[ℝ] (E →L[ℝ] Value E F n) := by
…
```
Mentions: OAI.ForcedComputation.BoundedSpatialJets.Value
def OAI.ForcedComputation.BoundedSpatialJets.valueMap line 40
Source documentation
A zero-order multilinear value is an ordinary value.
```
def valueMap : Value E F 0 ≃ₗᵢ[ℝ] F := by
…
```
Mentions: OAI.ForcedComputation.BoundedSpatialJets.Value
abbrev OAI.ForcedComputation.BoundedSpatialJets.Family line 44
Source documentation
Bounded continuous candidate jets through order k.
```
abbrev Family (k : ℕ) := (i : Fin (k + 1)) → (E →ᵇ Value E F i.val)
```
Mentions: OAI.ForcedComputation.BoundedSpatialJets.Value
abbrev OAI.ForcedComputation.BoundedSpatialJets.firstIndex line 47
Source documentation
The zeroth index, avoiding modular reduction of a variable-sized Fin.
```
abbrev firstIndex (k : ℕ) : Fin (k + 1) := ⟨0, Nat.zero_lt_succ k⟩
```
theorem OAI.ForcedComputation.BoundedSpatialJets.firstIndex_val line 49
def OAI.ForcedComputation.BoundedSpatialJets.consecutive line 52
Source documentation
Extract two consecutive jets, currying the higher jet as a derivative.
```
def consecutive (k : ℕ) (i : Fin k) :
    Family E F k →L[ℝ]
      ((E →ᵇ Value E F i.val) × (E →ᵇ (E →L[ℝ] Value E F i.val))) :=
…
```
Mentions: OAI.ForcedComputation.BoundedSpatialJets.Family, OAI.ForcedComputation.BoundedSpatialJets.Value
theorem OAI.ForcedComputation.BoundedSpatialJets.consecutive_apply line 58
def OAI.ForcedComputation.BoundedSpatialJets.compatible line 64
Source documentation
Derivative compatibility is a closed linear condition on the finite family.
```
def compatible (k : ℕ) : ClosedSubmodule ℝ (Family E F k) :=
…
```
Mentions: OAI.ForcedComputation.BoundedSpatialJets.Family
theorem OAI.ForcedComputation.BoundedSpatialJets.mem_compatible line 67
abbrev OAI.ForcedComputation.BoundedSpatialJets.Space line 76
Source documentation
The Banach space of bounded continuous spatial jets through order k.
```
abbrev Space (k : ℕ) := compatible E F k
```
Mentions: OAI.ForcedComputation.BoundedSpatialJets.compatible
instance OAI.ForcedComputation.BoundedSpatialJets.(instance at line 78) line 78
def OAI.ForcedComputation.BoundedSpatialJets.projection line 81
Source documentation
Bounded linear extraction of any spatial jet.
```
def projection (k : ℕ) (i : Fin (k + 1)) :
    Space E F k →L[ℝ] (E →ᵇ Value E F i.val) :=
…
```
Mentions: OAI.ForcedComputation.BoundedSpatialJets.Space, OAI.ForcedComputation.BoundedSpatialJets.Value
theorem OAI.ForcedComputation.BoundedSpatialJets.projection_apply line 85
theorem OAI.ForcedComputation.BoundedSpatialJets.norm_projection_le_one line 88
theorem OAI.ForcedComputation.BoundedSpatialJets.hasFDerivAt line 96
Source documentation
Every consecutive pair in a compatible family is an actual derivative pair.
```
theorem hasFDerivAt (k : ℕ) (J : Space E F k) (i : Fin k) (x : E) :
    HasFDerivAt (J.val i.castSucc) ((curryMap E F i.val) (J.val i.succ x)) x :=
…
```
Mentions: OAI.ForcedComputation.BoundedSpatialJets.Space, OAI.ForcedComputation.BoundedSpatialJets.curryMap
theorem OAI.ForcedComputation.BoundedSpatialJets.norm_jet_le line 101
Source documentation
The Banach norm controls every spatial jet uniformly in the base point.
```
theorem norm_jet_le (k : ℕ) (J : Space E F k) (i : Fin (k + 1)) (x : E) :
    ‖J.val i x‖ ≤ ‖J‖ :=
…
```
Mentions: OAI.ForcedComputation.BoundedSpatialJets.Space
theorem OAI.ForcedComputation.BoundedSpatialJets.jet_contDiff line 106
Source documentation
Each jet has the differentiability supplied by the remaining higher jets.
```
theorem jet_contDiff (k : ℕ) (J : Space E F k) (n m : ℕ) (h : n + m ≤ k) :
    ContDiff ℝ m (J.val ⟨n, by omega⟩) := by
…
```
Mentions: OAI.ForcedComputation.BoundedSpatialJets.Space
def OAI.ForcedComputation.BoundedSpatialJets.function line 122
Source documentation
The ordinary function represented by the zeroth jet.
```
def function (k : ℕ) (J : Space E F k) : E →ᵇ F :=
…
```
Mentions: OAI.ForcedComputation.BoundedSpatialJets.Space
theorem OAI.ForcedComputation.BoundedSpatialJets.function_apply line 126
theorem OAI.ForcedComputation.BoundedSpatialJets.function_contDiff line 129
theorem OAI.ForcedComputation.BoundedSpatialJets.norm_function_le line 133
def OAI.ForcedComputation.BoundedSpatialJets.functionMap line 139
Source documentation
Bounded linear extraction of the represented function.
```
def functionMap (k : ℕ) : Space E F k →L[ℝ] (E →ᵇ F) :=
…
```
Mentions: OAI.ForcedComputation.BoundedSpatialJets.Space
theorem OAI.ForcedComputation.BoundedSpatialJets.functionMap_apply line 143
theorem OAI.ForcedComputation.BoundedSpatialJets.norm_functionMap_le_one line 146
theorem OAI.ForcedComputation.BoundedSpatialJets.iteratedFDeriv_function line 154
Source documentation
The supplied jets are the actual iterated spatial derivatives.
```
theorem iteratedFDeriv_function (k : ℕ) (J : Space E F k) (n : ℕ) (hn : n ≤ k) :
    iteratedFDeriv ℝ n (function E F k J) = J.val ⟨n, by omega⟩ := by
…
```
Mentions: OAI.ForcedComputation.BoundedSpatialJets.Space, OAI.ForcedComputation.BoundedSpatialJets.function
theorem OAI.ForcedComputation.BoundedSpatialJets.norm_iteratedFDeriv_le line 176