BoundedDerivativeGraph.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The graph of spatial differentiation in the uniform norm is closed.

Both the function and its proposed derivative are bounded continuous maps. This is the basic completeness lemma for finite families of bounded spatial jets.

theorem OAI.ForcedComputation.isClosed_boundedDerivativeGraph line 23
Source documentation
Uniform limits of a function and its derivative remain a derivative pair.
```
theorem isClosed_boundedDerivativeGraph :
    IsClosed {p : (E →ᵇ F) × (E →ᵇ (E →L[ℝ] F)) |
      ∀ x, HasFDerivAt p.1 (p.2 x) x} := by
…
```
def OAI.ForcedComputation.boundedDerivativeGraph line 38
Source documentation
The bounded derivative graph, with its inherited uniform product norm.
```
def boundedDerivativeGraph :
    ClosedSubmodule ℝ ((E →ᵇ F) × (E →ᵇ (E →L[ℝ] F))) where
…
```
theorem OAI.ForcedComputation.mem_boundedDerivativeGraph line 53
abbrev OAI.ForcedComputation.BoundedC1 line 58
Source documentation
A bounded function with bounded continuous derivative, in its graph norm.
```
abbrev BoundedC1 := boundedDerivativeGraph E F
```
Mentions: OAI.ForcedComputation.boundedDerivativeGraph
instance OAI.ForcedComputation.(instance at line 60) line 60