BoundedSpatialJetKernelDependence.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Dependence of finite-jet convolution operators on their integrable scalar kernels.

theorem OAI.ForcedComputation.BoundedSpatialJets.convolutionCLM_sub_kernel line 18

theorem OAI.ForcedComputation.BoundedSpatialJets.norm_convolutionCLM_sub_le line 38

Source documentation

L1 perturbations of the scalar kernel uniformly control the whole jet operator.

theorem norm_convolutionCLM_sub_le (k : ℕ) (μ : Measure E) (w v : E → ℝ)
    (hw : Integrable w μ) (hv : Integrable v μ) :
    ‖convolutionCLM E F k μ w hw - convolutionCLM E F k μ v hv‖ ≤
      ∫ y, |w y - v y| ∂μ := by
…

Mentions: OAI.ForcedComputation.BoundedSpatialJets.convolutionCLM

def OAI.ForcedComputation.BoundedSpatialJets.convolutionOperator line 46
Source documentation
The convolution operator in the fixed normed operator space.
```
def convolutionOperator (k : ℕ) (μ : Measure E) (w : E → ℝ) (hw : Integrable w μ) :
    Operator E F F k := convolutionCLM E F k μ w hw
```
Mentions: OAI.ForcedComputation.BoundedSpatialJets.Operator, OAI.ForcedComputation.BoundedSpatialJets.convolutionCLM
theorem OAI.ForcedComputation.BoundedSpatialJets.operatorEquiv_convolutionOperator line 49

theorem OAI.ForcedComputation.BoundedSpatialJets.tendsto_convolutionCLM line 55

Source documentation

L1 convergence of kernels implies convergence in operator norm at every finite jet order.

theorem tendsto_convolutionCLM {A : Type*} (l : Filter A) (k : ℕ) (μ : Measure E)
    (w : A → E → ℝ) (v : E → ℝ) (hw : ∀ a, Integrable (w a) μ)
    (hv : Integrable v μ)
    (h : Tendsto (fun a => ∫ y, |w a y - v y| ∂μ) l (𝓝 0)) :
    Tendsto (fun a => convolutionCLM E F k μ (w a) (hw a)) l
      (𝓝 (convolutionCLM E F k μ v hv)) := by
…

Mentions: OAI.ForcedComputation.BoundedSpatialJets.convolutionCLM

theorem OAI.ForcedComputation.BoundedSpatialJets.convolution_truncate line 76
Source documentation
Forgetting higher derivatives commutes exactly with convolution.
```
theorem convolution_truncate (k n : ℕ) (hkn : k ≤ n) (μ : Measure E)
    (w : E → ℝ) (hw : Integrable w μ) (J : Space E F n) :
    convolution E F k μ w hw (truncate E F k n hkn J) =
      truncate E F k n hkn (convolution E F n μ w hw J) := by
…
```
Mentions: OAI.ForcedComputation.BoundedSpatialJets.Space, OAI.ForcedComputation.BoundedSpatialJets.convolution, OAI.ForcedComputation.BoundedSpatialJets.truncate
theorem OAI.ForcedComputation.BoundedSpatialJets.convolutionCLM_truncate line 86
Source documentation
The exact operator identity used when comparing fixed points at different jet orders.
```
theorem convolutionCLM_truncate (k n : ℕ) (hkn : k ≤ n) (μ : Measure E)
    (w : E → ℝ) (hw : Integrable w μ) :
    (convolutionCLM E F k μ w hw).comp (truncateCLM E F k n hkn) =
      (truncateCLM E F k n hkn).comp (convolutionCLM E F n μ w hw) := by
…
```
Mentions: OAI.ForcedComputation.BoundedSpatialJets.convolutionCLM, OAI.ForcedComputation.BoundedSpatialJets.truncateCLM