PlaneHeatSmoothing.lean`

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Gaussian convolution differentiates bounded continuous data by differentiating the kernel.

def OAI.ForcedComputation.PlaneHeat.heatConvolution line 19
Source documentation
The symmetric form of heat convolution, convenient for differentiating the kernel.
```
def heatConvolution (t : ℝ) (f : Plane → F) (x : Plane) : F :=
…
```
theorem OAI.ForcedComputation.PlaneHeat.heatConvolution_eq line 22
theorem OAI.ForcedComputation.PlaneHeat.integrand_integrable line 28
theorem OAI.ForcedComputation.PlaneHeat.derivativeIntegrand_continuous line 36
theorem OAI.ForcedComputation.PlaneHeat.derivativeIntegrand_integrable line 44
theorem OAI.ForcedComputation.PlaneHeat.hasFDerivAt_heatConvolution line 62
Source documentation
Differentiating under the integral is valid for bounded continuous data, without a spatial derivative assumption on that data.
```
theorem hasFDerivAt_heatConvolution {t : ℝ} (ht : 0 < t) (f : Plane → F)
    (hf : Continuous f) (C : ℝ) (hC : ∀ x, ‖f x‖ ≤ C) (x : Plane) :
    HasFDerivAt (heatConvolution F t f)
      (∫ y, (fderiv ℝ (kernel t) (x - y)).smulRight (f y)) x := by
…
```
Mentions: OAI.ForcedComputation.PlaneHeat.heatConvolution, OAI.ForcedComputation.PlaneHeat.kernel
theorem OAI.ForcedComputation.PlaneHeat.fderiv_heatConvolution_basis line 96
Source documentation
Each directional derivative is convolution against the corresponding integrable Gaussian derivative.
```
theorem fderiv_heatConvolution_basis {t : ℝ} (ht : 0 < t) (f : Plane → F)
    (hf : Continuous f) (C : ℝ) (hC : ∀ x, ‖f x‖ ≤ C) (x : Plane) (j : Fin 2) :
    fderiv ℝ (heatConvolution F t f) x (Pi.single j 1) =
      BoundedKernel.convolve Plane F volume (kernelDerivative t j) f x := by
…
```
Mentions: OAI.ForcedComputation.PlaneHeat.heatConvolution, OAI.ForcedComputation.BoundedKernel.convolve, OAI.ForcedComputation.PlaneHeat.kernelDerivative
theorem OAI.ForcedComputation.PlaneHeat.norm_fderiv_heatConvolution_basis_le line 107