Constant slice distributions

i. Overview

In this moudule we define the lift of distributions on Space d to distributions on Space d.succ which are constant between slices in the ith direction.

This is used, for example, to define distributions which are translationally invariant in the ith direction.

Examples of distributions which can be constructed in this way include the dirac deltas for lines and planes, rather then points.

ii. Key results

• sliceSchwartz : The continuous linear map which takes a Schwartz map on Space d.succ and gives a Schwartz map on Space d by integrating over the ith direction.
• constantSliceDist : The distribution on Space d.succ formed by a distribution on Space d which is translationally invariant in the ith direction.

iii. Table of contents

• A. Schwartz maps
  • A.1. Bounded condition for derivatives of Schwartz maps on slices
  • A.2. Integrability for of Schwartz maps on slices
  • A.3. Continiuity of integrations of slices of Schwartz maps
  • A.4. Derivative of integrations of slices of Schwartz maps
  • A.5. Differentiability as a slices of Schwartz maps
  • A.6. Smoothness as slices of Schwartz maps
  • A.7. Iterated derivatives of integrations of slices of Schwartz maps
  • A.8. The map integrating over one component of a Schwartz map
• B. Constant slice distribution
  • B.1. Derivative of constant slice distributions

iv. References

A. Schwartz maps

A.1. Bounded condition for derivatives of Schwartz maps on slices

theorem Space.schwartzMap_slice_bound {n m d : ℕ} (i : Fin d.succ) : ∃ (rt : ℕ), ∀ (η : SchwartzMap (Space d.succ) ℝ), ∃ (k : ℝ), MeasureTheory.Integrable (fun (x : ℝ) => ‖((1 + ‖x‖) ^ rt)⁻¹‖) MeasureTheory.volume ∧ (∀ (x : Space d) (r : ℝ), ‖(slice i).symm (r, x)‖ ^ m * ‖iteratedFDeriv ℝ n (⇑η) ((slice i).symm (r, x))‖ ≤ k * ‖(1 + ‖r‖) ^ rt‖⁻¹) ∧ k = 2 ^ (rt + m, n).1 * ((Finset.Iic (rt + m, n)).sup fun (m : ℕ × ℕ) => SchwartzMap.seminorm ℝ m.1 m.2) η

A.2. Integrability for of Schwartz maps on slices

theorem Space.schwartzMap_mul_iteratedFDeriv_integrable_slice_symm {d : ℕ} (n m : ℕ) (η : SchwartzMap (Space d.succ) ℝ) (x : Space d) (i : Fin d.succ) : MeasureTheory.Integrable (fun (r : ℝ) => ‖(slice i).symm (r, x)‖ ^ m * ‖iteratedFDeriv ℝ n (⇑η) ((slice i).symm (r, x))‖) MeasureTheory.volume

theorem Space.schwartzMap_integrable_slice_symm {d : ℕ} (i : Fin d.succ) (η : SchwartzMap (Space d.succ) ℝ) (x : Space d) : MeasureTheory.Integrable (fun (r : ℝ) => η ((slice i).symm (r, x))) MeasureTheory.volume

theorem Space.schwartzMap_fderiv_integrable_slice_symm {d : ℕ} (η : SchwartzMap (Space d.succ) ℝ) (x : Space d) (i : Fin d.succ) : MeasureTheory.Integrable (fun (r : ℝ) => fderiv ℝ (fun (x : Space d) => η ((slice i).symm (r, x))) x) MeasureTheory.volume

theorem Space.schwartzMap_fderiv_left_integrable_slice_symm {d : ℕ} (η : SchwartzMap (Space d.succ) ℝ) (x : Space d) (i : Fin d.succ) : MeasureTheory.Integrable (fun (r : ℝ) => (fderiv ℝ (fun (r : ℝ) => η ((slice i).symm (r, x))) r) 1) MeasureTheory.volume

theorem Space.schwartzMap_iteratedFDeriv_norm_slice_symm_integrable {n d : ℕ} (η : SchwartzMap (Space d.succ) ℝ) (x : Space d) (i : Fin d.succ) : MeasureTheory.Integrable (fun (r : ℝ) => ‖iteratedFDeriv ℝ n (⇑η) ((slice i).symm (r, x))‖) MeasureTheory.volume

theorem Space.schwartzMap_iteratedFDeriv_slice_symm_integrable {n d : ℕ} (η : SchwartzMap (Space d.succ) ℝ) (x : Space d) (i : Fin d.succ) : MeasureTheory.Integrable (fun (r : ℝ) => iteratedFDeriv ℝ n (⇑η) ((slice i).symm (r, x))) MeasureTheory.volume

A.3. Continiuity of integrations of slices of Schwartz maps

theorem Space.continuous_schwartzMap_slice_integral {d : ℕ} (i : Fin d.succ) (η : SchwartzMap (Space d.succ) ℝ) : Continuous fun (x : Space d) => ∫ (r : ℝ), η ((slice i).symm (r, x))

A.4. Derivative of integrations of slices of Schwartz maps

theorem Space.schwartzMap_slice_integral_hasFDerivAt {d : ℕ} (η : SchwartzMap (Space d.succ) ℝ) (i : Fin d.succ) (x₀ : Space d) : HasFDerivAt (fun (x : Space d) => ∫ (r : ℝ), η ((slice i).symm (r, x))) (∫ (r : ℝ), fderiv ℝ (fun (x : Space d) => η ((slice i).symm (r, x))) x₀) x₀

A.5. Differentiability as a slices of Schwartz maps

theorem Space.schwartzMap_slice_integral_differentiable {d : ℕ} (η : SchwartzMap (Space d.succ) ℝ) (i : Fin d.succ) : Differentiable ℝ fun (x : Space d) => ∫ (r : ℝ), η ((slice i).symm (r, x))

A.6. Smoothness as slices of Schwartz maps

theorem Space.schwartzMap_slice_integral_contDiff {d : ℕ} (n : ℕ) (η : SchwartzMap (Space d.succ) ℝ) (i : Fin d.succ) : ContDiff ℝ ↑n fun (x : Space d) => ∫ (r : ℝ), η ((slice i).symm (r, x))

A.7. Iterated derivatives of integrations of slices of Schwartz maps

theorem Space.schwartzMap_slice_integral_iteratedFDeriv_apply {d : ℕ} (n : ℕ) (η : SchwartzMap (Space d.succ) ℝ) (i : Fin d.succ) (x : Space d) (y : Fin n → Space d) : (iteratedFDeriv ℝ n (fun (x : Space d) => ∫ (r : ℝ), η ((slice i).symm (r, x))) x) y = ∫ (r : ℝ), (iteratedFDeriv ℝ n (⇑η) ((slice i).symm (r, x))) fun (j : Fin n) => (slice i).symm (0, y j)

theorem Space.schwartzMap_slice_integral_iteratedFDeriv {d : ℕ} (n : ℕ) (η : SchwartzMap (Space d.succ) ℝ) (i : Fin d.succ) (x : Space d) : iteratedFDeriv ℝ n (fun (x : Space d) => ∫ (r : ℝ), η ((slice i).symm (r, x))) x = (∫ (r : ℝ), iteratedFDeriv ℝ n (⇑η) ((slice i).symm (r, x))).compContinuousLinearMap fun (x : Fin n) => (↑(slice i).symm).comp (ContinuousLinearMap.prod 0 (ContinuousLinearMap.id ℝ (Space d)))

theorem Space.schwartzMap_slice_integral_iteratedFDeriv_norm_le {d : ℕ} (n : ℕ) (η : SchwartzMap (Space d.succ) ℝ) (i : Fin d.succ) (x : Space d) : ‖iteratedFDeriv ℝ n (fun (x : Space d) => ∫ (r : ℝ), η ((slice i).symm (r, x))) x‖ ≤ (∫ (r : ℝ), ‖iteratedFDeriv ℝ n (⇑η) ((slice i).symm (r, x))‖) * ‖(↑(slice i).symm).comp (ContinuousLinearMap.prod 0 (ContinuousLinearMap.id ℝ (Space d)))‖ ^ n

theorem Space.schwartzMap_mul_pow_slice_integral_iteratedFDeriv_norm_le {d : ℕ} (n m : ℕ) (i : Fin d.succ) : ∃ (rt : ℕ), ∀ (η : SchwartzMap (Space d.succ) ℝ) (x : Space d), MeasureTheory.Integrable (fun (x : ℝ) => ‖((1 + ‖x‖) ^ rt)⁻¹‖) MeasureTheory.volume ∧ ‖x‖ ^ m * ‖iteratedFDeriv ℝ n (fun (x : Space d) => ∫ (r : ℝ), η ((slice i).symm (r, x))) x‖ ≤ (∫ (r : ℝ), ‖((1 + ‖r‖) ^ rt)⁻¹‖) * ‖(↑(slice i).symm).comp (ContinuousLinearMap.prod 0 (ContinuousLinearMap.id ℝ (Space d)))‖ ^ n * (2 ^ (rt + m, n).1 * ((Finset.Iic (rt + m, n)).sup fun (m : ℕ × ℕ) => SchwartzMap.seminorm ℝ m.1 m.2) η)

A.8. The map integrating over one component of a Schwartz map

def Space.sliceSchwartz {d : ℕ} (i : Fin d.succ) : SchwartzMap (Space d.succ) ℝ →L[ℝ] SchwartzMap (Space d) ℝ

The continuous linear map taking a Schwartz map and integrating over the ith component, to give a Schwartz map of one dimension lower.

Equations

• Space.sliceSchwartz i = SchwartzMap.mkCLM (fun (η : SchwartzMap (Space d.succ) ℝ) (x : Space d) => ∫ (r : ℝ), η ((Space.slice i).symm (r, x))) ⋯ ⋯ ⋯ ⋯

theorem Space.sliceSchwartz_apply {d : ℕ} (i : Fin d.succ) (η : SchwartzMap (Space d.succ) ℝ) (x : Space d) : ((sliceSchwartz i) η) x = ∫ (r : ℝ), η ((slice i).symm (r, x))

B. Constant slice distribution

def Space.constantSliceDist {M : Type} [NormedAddCommGroup M] [NormedSpace ℝ M] {d : ℕ} (i : Fin d.succ) : ((Space d)→d[ℝ] M) →ₗ[ℝ] (Space d.succ)→d[ℝ] M

Distributions on Space d.succ from distributions on Space d given a direction i. These distributions are constant on slices in the i direction..

Equations

• Space.constantSliceDist i = { toFun := fun (f : (Space d)→d[ℝ] M) => ContinuousLinearMap.comp f (Space.sliceSchwartz i), map_add' := ⋯, map_smul' := ⋯ }

theorem Space.constantSliceDist_apply {M : Type} [NormedAddCommGroup M] [NormedSpace ℝ M] {d : ℕ} (i : Fin d.succ) (f : (Space d)→d[ℝ] M) (η : SchwartzMap (Space d.succ) ℝ) : ((constantSliceDist i) f) η = f ((sliceSchwartz i) η)

B.1. Derivative of constant slice distributions

theorem Space.distDeriv_constantSliceDist_same {M : Type} [NormedAddCommGroup M] [NormedSpace ℝ M] {d : ℕ} (i : Fin d.succ) (f : (Space d)→d[ℝ] M) : (distDeriv i) ((constantSliceDist i) f) = 0

theorem Space.distDeriv_constantSliceDist_succAbove {M : Type} [NormedAddCommGroup M] [NormedSpace ℝ M] {d : ℕ} (i : Fin d.succ) (j : Fin d) (f : (Space d)→d[ℝ] M) : (distDeriv (i.succAbove j)) ((constantSliceDist i) f) = (constantSliceDist i) ((distDeriv j) f)