BoundedSpatialJetProduct.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Bounded spatial jets of pointwise bilinear products.

The finite-order Leibniz estimate gives the constant 2^k. In particular, fixing a smooth bounded coefficient gives a bounded linear multiplication operator on the jet Banach space used in a Volterra equation.

def OAI.ForcedComputation.BoundedSpatialJets.ofFunctionFamily line 23
Source documentation
Bundle the actual derivatives of a function with bounded jets.
```
def ofFunctionFamily (k : ℕ) (f : E → F) (hf : ContDiff ℝ k f) (C : ℝ)
    (hC : ∀ n ≤ k, ∀ x, ‖iteratedFDeriv ℝ n f x‖ ≤ C) : Family E F k :=
…
```
Mentions: OAI.ForcedComputation.BoundedSpatialJets.Family
def OAI.ForcedComputation.BoundedSpatialJets.ofFunction line 33
Source documentation
A C^k function whose first k derivatives are uniformly bounded defines a jet.
```
def ofFunction (k : ℕ) (f : E → F) (hf : ContDiff ℝ k f) (C : ℝ)
    (hC : ∀ n ≤ k, ∀ x, ‖iteratedFDeriv ℝ n f x‖ ≤ C) : Space E F k := by
…
```
Mentions: OAI.ForcedComputation.BoundedSpatialJets.Space
theorem OAI.ForcedComputation.BoundedSpatialJets.ofFunction_apply line 43
theorem OAI.ForcedComputation.BoundedSpatialJets.function_ofFunction line 49
theorem OAI.ForcedComputation.BoundedSpatialJets.norm_ofFunction_le line 57
theorem OAI.ForcedComputation.BoundedSpatialJets.function_injective line 67
Source documentation
A compatible family is determined by its zeroth-order function.
```
theorem function_injective (k : ℕ) : Function.Injective (function E F k) := by
…
```
Mentions: OAI.ForcedComputation.BoundedSpatialJets.function

theorem OAI.ForcedComputation.BoundedSpatialJets.bilinear_derivative_bound line 83

Source documentation

The finite Leibniz estimate, uniformly in the spatial point.

theorem bilinear_derivative_bound (k : ℕ) (B : F →L[ℝ] G →L[ℝ] H)
    (J : Space E F k) (K : Space E G k) (n : ℕ) (hn : n ≤ k) (x : E) :
    ‖iteratedFDeriv ℝ n (fun y => B (function E F k J y) (function E G k K y)) x‖ ≤
      ‖B‖ * (2 : ℝ) ^ k * ‖J‖ * ‖K‖ := by
…

Mentions: OAI.ForcedComputation.BoundedSpatialJets.Space, OAI.ForcedComputation.BoundedSpatialJets.function

def OAI.ForcedComputation.BoundedSpatialJets.bilinear line 116
Source documentation
Pointwise application of a bounded bilinear map to two compatible jets.
```
def bilinear (k : ℕ) (B : F →L[ℝ] G →L[ℝ] H)
    (J : Space E F k) (K : Space E G k) : Space E H k :=
…
```
Mentions: OAI.ForcedComputation.BoundedSpatialJets.Space
theorem OAI.ForcedComputation.BoundedSpatialJets.function_bilinear line 123
theorem OAI.ForcedComputation.BoundedSpatialJets.norm_bilinear_le line 129