Integration by parts for the literal whole-space Gaussian average.
theorem
EulerWholeSpaceGaussian.integrable_kernel_smul
{V : Type u_1}
[NormedAddCommGroup V]
[NormedSpace ℝ V]
(k : EulerSmoothLimit.Space → ℝ)
(hk : MeasureTheory.Integrable k MeasureTheory.volume)
(f : EulerSmoothLimit.Space → V)
(hf : Continuous f)
(C : ℝ)
(hb : ∀ (x : EulerSmoothLimit.Space), ‖f x‖ ≤ C)
:
MeasureTheory.Integrable (fun (x : EulerSmoothLimit.Space) => k x • f x) MeasureTheory.volume
theorem
EulerWholeSpaceGaussian.fderiv_translate
{V : Type u_1}
[NormedAddCommGroup V]
[NormedSpace ℝ V]
(f : EulerSmoothLimit.Space → V)
(hf : Differentiable ℝ f)
(x y : EulerSmoothLimit.Space)
:
theorem
EulerWholeSpaceGaussian.integration_by_parts
{V : Type u_1}
[NormedAddCommGroup V]
[NormedSpace ℝ V]
(k : EulerSmoothLimit.Space → ℝ)
(hk : Differentiable ℝ k)
(hki : MeasureTheory.Integrable k MeasureTheory.volume)
(a : EulerSmoothLimit.Space)
(hkai : MeasureTheory.Integrable (fun (x : EulerSmoothLimit.Space) => (fderiv ℝ k x) a) MeasureTheory.volume)
(f : EulerSmoothLimit.Space → V)
(hf : ContDiff ℝ (↑⊤) f)
(C₀ C₁ : ℝ)
(h₀ : ∀ (x : EulerSmoothLimit.Space), ‖f x‖ ≤ C₀)
(h₁ : ∀ (x : EulerSmoothLimit.Space), ‖fderiv ℝ f x‖ ≤ C₁)
(x : EulerSmoothLimit.Space)
:
Integration by parts uses genuine spatial derivatives and only the ordinary integrability of the scalar kernel and its derivative.
theorem
EulerWholeSpaceGaussian.average_first_identity
{V : Type u_1}
[NormedAddCommGroup V]
[NormedSpace ℝ V]
{t : ℝ}
(ht : 0 < t)
(f : EulerSmoothLimit.Space → V)
(hf : ContDiff ℝ (↑⊤) f)
(C₀ C₁ : ℝ)
(h₀ : ∀ (x : EulerSmoothLimit.Space), ‖f x‖ ≤ C₀)
(h₁ : ∀ (x : EulerSmoothLimit.Space), ‖fderiv ℝ f x‖ ≤ C₁)
(a x : EulerSmoothLimit.Space)
:
average t (fun (y : EulerSmoothLimit.Space) => (fderiv ℝ f y) a) x = -∫ (y : EulerSmoothLimit.Space), firstKernel t a y • f (x + y)
theorem
EulerWholeSpaceGaussian.directional_smooth
{V : Type u_1}
[NormedAddCommGroup V]
[NormedSpace ℝ V]
(f : EulerSmoothLimit.Space → V)
(hf : ContDiff ℝ (↑⊤) f)
(a : EulerSmoothLimit.Space)
:
theorem
EulerWholeSpaceGaussian.directional_fderiv
{V : Type u_1}
[NormedAddCommGroup V]
[NormedSpace ℝ V]
(f : EulerSmoothLimit.Space → V)
(hf : ContDiff ℝ (↑⊤) f)
(a x b : EulerSmoothLimit.Space)
:
theorem
EulerWholeSpaceGaussian.directional_fderiv_bound
{V : Type u_1}
[NormedAddCommGroup V]
[NormedSpace ℝ V]
(f : EulerSmoothLimit.Space → V)
(hf : ContDiff ℝ (↑⊤) f)
(C₂ : ℝ)
(h₂ : ∀ (x : EulerSmoothLimit.Space), ‖fderiv ℝ (fderiv ℝ f) x‖ ≤ C₂)
(a x : EulerSmoothLimit.Space)
:
theorem
EulerWholeSpaceGaussian.average_second_identity
{V : Type u_1}
[NormedAddCommGroup V]
[NormedSpace ℝ V]
{t : ℝ}
(ht : 0 < t)
(f : EulerSmoothLimit.Space → V)
(hf : ContDiff ℝ (↑⊤) f)
(C₀ C₁ C₂ : ℝ)
(h₀ : ∀ (x : EulerSmoothLimit.Space), ‖f x‖ ≤ C₀)
(h₁ : ∀ (x : EulerSmoothLimit.Space), ‖fderiv ℝ f x‖ ≤ C₁)
(h₂ : ∀ (x : EulerSmoothLimit.Space), ‖fderiv ℝ (fderiv ℝ f) x‖ ≤ C₂)
(a b x : EulerSmoothLimit.Space)
:
average t (fun (z : EulerSmoothLimit.Space) => (fderiv ℝ (fun (y : EulerSmoothLimit.Space) => (fderiv ℝ f y) b) z) a)
x = ∫ (y : EulerSmoothLimit.Space), secondKernel t a b y • f (x + y)
Both spatial derivatives are transferred to the actual Gaussian kernel.
theorem
EulerWholeSpaceGaussian.average_second_bound
{V : Type u_1}
[NormedAddCommGroup V]
[NormedSpace ℝ V]
{t : ℝ}
(ht : 0 < t)
(f : EulerSmoothLimit.Space → V)
(hf : ContDiff ℝ (↑⊤) f)
(C₀ C₁ C₂ : ℝ)
(h₀ : ∀ (x : EulerSmoothLimit.Space), ‖f x‖ ≤ C₀)
(h₁ : ∀ (x : EulerSmoothLimit.Space), ‖fderiv ℝ f x‖ ≤ C₁)
(h₂ : ∀ (x : EulerSmoothLimit.Space), ‖fderiv ℝ (fderiv ℝ f) x‖ ≤ C₂)
(a b x : EulerSmoothLimit.Space)
:
The genuine smoothed second derivative has a 1/t bound controlled only by the size of the original field. Bounds on its derivatives are used to justify integration by parts and do not enter the estimate.