Distributions which are constant in time

i. Overview

in this module given a distribution on Space d, we define the associated distribution on Time × Space d which is constant in time.

This is defined by integrating Schwartz Maps on Time × Space d over the time coordinate, to get a Schwartz Map on Space d.

ii. Key results

• Space.timeIntegralSchwartz : the integral over time of a Schwartz map on Time × Space d to give a Schwartz map on Space d.
• Space.constantTime : the distribution on Time × Space d associated with a distribution on Space d, which is constant in time.

iii. Table of contents

• A. Properties of time integrals of Schwartz maps
  • A.1. Continuity as a function of space
  • A.2. Derivative a function of space
  • A.3. Differentiability as a function of space
  • A.4. Integrability of the derivative as a function of space
  • A.5. Smoothness as a function of space
• B. Properties of schwartz maps at a constant space point
  • B.1. Integrability
  • B.2. Integrability of powers times norm of iterated derivatives
    • B.2.1. Bounds on powers times norm of iterated derivatives
    • B.2.2. Integrability of powers times norm of iterated derivatives
  • B.3. Integrability of iterated derivatives
• C. Decay results for derivatives of the time integral
  • C.1. Moving the iterated derivative inside the time integral
  • C.2. Bound on the norm of iterated derivative
  • C.3. Bound on the norm of iterated derivative mul a power
• D. The time integral as a schwartz map
• E. Constant time distributions
  • E.1. Space derivatives of constant time distributions
  • E.2. Space gradient of constant time distributions
  • E.3. Space divergence of constant time distributions
  • E.4. Space curl of constant time distributions
  • E.5. Time derivative of constant time distributions

iv. References

A. Properties of time integrals of Schwartz maps

A.1. Continuity as a function of space

theorem Space.continuous_time_integral {d : ℕ} (η : SchwartzMap (Time × Space d) ℝ) : Continuous fun (x : Space d) => ∫ (t : Time), η (t, x)

A.2. Derivative a function of space

theorem Space.time_integral_hasFDerivAt {d : ℕ} (η : SchwartzMap (Time × Space d.succ) ℝ) (x₀ : Space d.succ) : HasFDerivAt (fun (x : Space d.succ) => ∫ (t : Time), η (t, x)) (∫ (t : Time), fderiv ℝ (fun (x : Space d.succ) => η (t, x)) x₀) x₀

A.3. Differentiability as a function of space

theorem Space.time_integral_differentiable {d : ℕ} (η : SchwartzMap (Time × Space d.succ) ℝ) : Differentiable ℝ fun (x : Space d.succ) => ∫ (t : Time), η (t, x)

A.4. Integrability of the derivative as a function of space

theorem Space.integrable_fderiv_space {d : ℕ} (η : SchwartzMap (Time × Space d.succ) ℝ) (x : Space d.succ) : MeasureTheory.Integrable (fun (t : Time) => fderiv ℝ (fun (x : Space d.succ) => η (t, x)) x) MeasureTheory.volume

A.5. Smoothness as a function of space

theorem Space.time_integral_contDiff {d : ℕ} (n : ℕ) (η : SchwartzMap (Time × Space d.succ) ℝ) : ContDiff ℝ ↑n fun (x : Space d.succ) => ∫ (t : Time), η (t, x)

B. Properties of schwartz maps at a constant space point

B.1. Integrability

theorem Space.integrable_time_integral {d : ℕ} (η : SchwartzMap (Time × Space d.succ) ℝ) (x : Space d.succ) : MeasureTheory.Integrable (fun (t : Time) => η (t, x)) MeasureTheory.volume

B.2. Integrability of powers times norm of iterated derivatives

B.2.1. Bounds on powers times norm of iterated derivatives

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

B.2.2. Integrability of powers times norm of iterated derivatives

theorem Space.iteratedFDeriv_norm_mul_pow_integrable {d : ℕ} (n m : ℕ) (η : SchwartzMap (Time × Space d.succ) ℝ) (x : Space d.succ) : MeasureTheory.Integrable (fun (t : Time) => ‖(t, x)‖ ^ m * ‖iteratedFDeriv ℝ n ⇑η (t, x)‖) MeasureTheory.volume

B.3. Integrability of iterated derivatives

theorem Space.iteratedFDeriv_norm_integrable {n d : ℕ} (η : SchwartzMap (Time × Space d.succ) ℝ) (x : Space d.succ) : MeasureTheory.Integrable (fun (t : Time) => ‖iteratedFDeriv ℝ n ⇑η (t, x)‖) MeasureTheory.volume

theorem Space.iteratedFDeriv_integrable {n d : ℕ} (η : SchwartzMap (Time × Space d.succ) ℝ) (x : Space d.succ) : MeasureTheory.Integrable (fun (t : Time) => iteratedFDeriv ℝ n ⇑η (t, x)) MeasureTheory.volume

C. Decay results for derivatives of the time integral

C.1. Moving the iterated derivative inside the time integral

theorem Space.time_integral_iteratedFDeriv_apply {d : ℕ} (n : ℕ) (η : SchwartzMap (Time × Space d.succ) ℝ) (x : Space d.succ) (y : Fin n → Space d.succ) : (iteratedFDeriv ℝ n (fun (x : Space d.succ) => ∫ (t : Time), η (t, x)) x) y = ∫ (t : Time), (iteratedFDeriv ℝ n ⇑η (t, x)) fun (i : Fin n) => (0, y i)

theorem Space.time_integral_iteratedFDeriv_eq {d : ℕ} (n : ℕ) (η : SchwartzMap (Time × Space d.succ) ℝ) (x : Space d.succ) : iteratedFDeriv ℝ n (fun (x : Space d.succ) => ∫ (t : Time), η (t, x)) x = (∫ (t : Time), iteratedFDeriv ℝ n ⇑η (t, x)).compContinuousLinearMap fun (x : Fin n) => ContinuousLinearMap.prod 0 (ContinuousLinearMap.id ℝ (Space d.succ))

C.2. Bound on the norm of iterated derivative

theorem Space.time_integral_iteratedFDeriv_norm_le {d : ℕ} (n : ℕ) (η : SchwartzMap (Time × Space d.succ) ℝ) (x : Space d.succ) : ‖iteratedFDeriv ℝ n (fun (x : Space d.succ) => ∫ (t : Time), η (t, x)) x‖ ≤ (∫ (t : Time), ‖iteratedFDeriv ℝ n ⇑η (t, x)‖) * ‖ContinuousLinearMap.prod 0 (ContinuousLinearMap.id ℝ (Space d.succ))‖ ^ n

C.3. Bound on the norm of iterated derivative mul a power

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

D. The time integral as a schwartz map

def Space.timeIntegralSchwartz {d : ℕ} : SchwartzMap (Time × Space d.succ) ℝ →L[ℝ] SchwartzMap (Space d.succ) ℝ

The continuous linear map taking Schwartz maps on Time × Space d to space d by integrating over time.

Equations

• Space.timeIntegralSchwartz = SchwartzMap.mkCLM (fun (η : SchwartzMap (Time × Space d.succ) ℝ) (x : Space d.succ) => ∫ (t : Time), η (t, x)) ⋯ ⋯ ⋯ ⋯

theorem Space.timeIntegralSchwartz_apply {d : ℕ} (η : SchwartzMap (Time × Space d.succ) ℝ) (x : Space d.succ) : (timeIntegralSchwartz η) x = ∫ (t : Time), η (t, x)

E. Constant time distributions

def Space.constantTime {M : Type} [NormedAddCommGroup M] [NormedSpace ℝ M] {d : ℕ} : ((Space d.succ)→d[ℝ] M) →ₗ[ℝ] (Time × Space d.succ)→d[ℝ] M

Distributions on Time × Space d from distributions on Space d. These distributions are constant in time.

Equations

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

theorem Space.constantTime_apply {M : Type} [NormedAddCommGroup M] [NormedSpace ℝ M] {d : ℕ} (f : (Space d.succ)→d[ℝ] M) (η : SchwartzMap (Time × Space d.succ) ℝ) : (constantTime f) η = f (timeIntegralSchwartz η)

E.1. Space derivatives of constant time distributions

theorem Space.constantTime_spaceDerivD {M : Type} {d : ℕ} [NormedAddCommGroup M] [NormedSpace ℝ M] (i : Fin d.succ) (f : (Space d.succ)→d[ℝ] M) : (spaceDerivD i) (constantTime f) = constantTime ((derivD i) f)

E.2. Space gradient of constant time distributions

theorem Space.constantTime_spaceGradD {d : ℕ} (f : (Space d.succ)→d[ℝ] ℝ) : spaceGradD (constantTime f) = constantTime (gradD f)

E.3. Space divergence of constant time distributions

theorem Space.constantTime_spaceDivD {d : ℕ} (f : (Space d.succ)→d[ℝ] EuclideanSpace ℝ (Fin d.succ)) : spaceDivD (constantTime f) = constantTime (divD f)

E.4. Space curl of constant time distributions

theorem Space.constantTime_spaceCurlD (f : Space→d[ℝ] EuclideanSpace ℝ (Fin 3)) : spaceCurlD (constantTime f) = constantTime (curlD f)

E.5. Time derivative of constant time distributions

@[simp]

theorem Space.constantTime_timeDerivD {M : Type} [NormedAddCommGroup M] [NormedSpace ℝ M] {d : ℕ} (f : (Space d.succ)→d[ℝ] M) : timeDerivD (constantTime f) = 0