BoundedSpatialJetDifferentiation.lean`

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Bounded differentiation and linear maps commute with spatial convolution.

theorem OAI.ForcedComputation.BoundedSpatialJets.postcomposeCLM_convolution line 22
Source documentation
Fixed linear postcomposition commutes with convolution on each finite jet space.
```
theorem postcomposeCLM_convolution (k : ℕ) (L : F →L[ℝ] G)
    (μ : Measure E) (w : E → ℝ) (hw : Integrable w μ) (J : Space E F k) :
    postcomposeCLM E F G k L (convolution E F k μ w hw J) =
      convolution E G k μ w hw (postcomposeCLM E F G k L J) := by
…
```
Mentions: OAI.ForcedComputation.BoundedSpatialJets.Space, OAI.ForcedComputation.BoundedSpatialJets.postcomposeCLM, OAI.ForcedComputation.BoundedSpatialJets.convolution
theorem OAI.ForcedComputation.BoundedSpatialJets.derivativeCLM_convolution line 36
Source documentation
A bounded spatial derivative may be taken on the input of a convolution.
```
theorem derivativeCLM_convolution (k : ℕ)
    (μ : Measure E) (w : E → ℝ) (hw : Integrable w μ) (J : Space E F (k+1)) :
    derivativeCLM E F k (convolution E F (k+1) μ w hw J) =
      convolution E (E →L[ℝ] F) k μ w hw (derivativeCLM E F k J) := by
…
```
Mentions: OAI.ForcedComputation.BoundedSpatialJets.Space, OAI.ForcedComputation.BoundedSpatialJets.derivativeCLM, OAI.ForcedComputation.BoundedSpatialJets.convolution
theorem OAI.ForcedComputation.BoundedSpatialJets.directionalDerivativeCLM_convolution line 64
Source documentation
In particular, directional derivatives commute with spatial convolution.
```
theorem directionalDerivativeCLM_convolution (k : ℕ) (v : E)
    (μ : Measure E) (w : E → ℝ) (hw : Integrable w μ) (J : Space E F (k+1)) :
    directionalDerivativeCLM E F k v (convolution E F (k+1) μ w hw J) =
      convolution E F k μ w hw (directionalDerivativeCLM E F k v J) := by
…
```
Mentions: OAI.ForcedComputation.BoundedSpatialJets.Space, OAI.ForcedComputation.BoundedSpatialJets.directionalDerivativeCLM, OAI.ForcedComputation.BoundedSpatialJets.convolution