BoundedSpatialJetConvolution.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Convolution by an integrable scalar kernel on the Banach space of finite spatial jets.

The construction integrates each jet pointwise. It therefore does not assume that spatial translations act strongly continuously on the uniform norm of the highest derivative.

theorem OAI.ForcedComputation.BoundedSpatialJets.continuous_convolve line 24
def OAI.ForcedComputation.BoundedSpatialJets.kernelMass line 39
Source documentation
The kernel mass controlling every jet, with absolute values for signed kernels.
```
def kernelMass (μ : Measure E) (w : E → ℝ) : ℝ := ∫ y, |w y| ∂μ
…
```
theorem OAI.ForcedComputation.BoundedSpatialJets.kernelMass_nonneg line 43
def OAI.ForcedComputation.BoundedSpatialJets.convolutionFamily line 47
Source documentation
Pointwise convolution of the finite family of bounded derivatives.
```
def convolutionFamily (k : ℕ) (μ : Measure E) (w : E → ℝ) (hw : Integrable w μ)
    (J : Space E F k) : Family E F k := fun i =>
…
```
Mentions: OAI.ForcedComputation.BoundedSpatialJets.Space, OAI.ForcedComputation.BoundedSpatialJets.Family
theorem OAI.ForcedComputation.BoundedSpatialJets.convolutionFamily_compatible line 58
Source documentation
The consecutive derivatives remain compatible after convolution.
```
theorem convolutionFamily_compatible (k : ℕ) (μ : Measure E) (w : E → ℝ)
    (hw : Integrable w μ) (J : Space E F k) :
    convolutionFamily E F k μ w hw J ∈ compatible E F k := by
…
```
Mentions: OAI.ForcedComputation.BoundedSpatialJets.Space, OAI.ForcedComputation.BoundedSpatialJets.convolutionFamily, OAI.ForcedComputation.BoundedSpatialJets.compatible
def OAI.ForcedComputation.BoundedSpatialJets.convolution line 86
Source documentation
Convolution as an element of the same finite-order jet space.
```
def convolution (k : ℕ) (μ : Measure E) (w : E → ℝ) (hw : Integrable w μ)
    (J : Space E F k) : Space E F k :=
…
```
Mentions: OAI.ForcedComputation.BoundedSpatialJets.Space
theorem OAI.ForcedComputation.BoundedSpatialJets.convolution_jet line 90
theorem OAI.ForcedComputation.BoundedSpatialJets.function_convolution line 94
theorem OAI.ForcedComputation.BoundedSpatialJets.norm_convolution_le line 107
def OAI.ForcedComputation.BoundedSpatialJets.convolutionCLM line 121
Source documentation
The bounded linear heat/convolution operator; its norm is at most the kernel's L1 mass.
```
def convolutionCLM (k : ℕ) (μ : Measure E) (w : E → ℝ) (hw : Integrable w μ) :
    Space E F k →L[ℝ] Space E F k :=
…
```
Mentions: OAI.ForcedComputation.BoundedSpatialJets.Space
theorem OAI.ForcedComputation.BoundedSpatialJets.convolutionCLM_apply line 151
theorem OAI.ForcedComputation.BoundedSpatialJets.norm_convolutionCLM_le line 155