Imports
/-
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module
public import Physlib.SpaceAndTime.TimeAndSpace.Basic
public import Mathlib.Analysis.Calculus.ContDiff.FiniteDimensionDistributions 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
@[expose] public sectionA. Properties of time integrals of Schwartz maps
A.1. Continuity as a function of space
d:ℕη:𝓢(Time × Space d, ℝ)rt:ℕhrt:Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volumek:ℝhk:2 ^ (rt, 0).1 * ((Finset.Iic (rt, 0)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) η = kh0:∀ (a : Time) (b : Space d), (1 + max ‖a‖ ‖b‖) ^ rt * |η (a, b)| ≤ kh1:∀ (x : Space d) (t : Time), ‖η (t, x)‖ ≤ k * ‖(1 + ‖t‖) ^ rt‖⁻¹⊢ Continuous fun x => ∫ (t : Time), η (t, x)
d:ℕη:𝓢(Time × Space d, ℝ)rt:ℕhrt:Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volumek:ℝhk:2 ^ (rt, 0).1 * ((Finset.Iic (rt, 0)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) η = kh0:∀ (a : Time) (b : Space d), (1 + max ‖a‖ ‖b‖) ^ rt * |η (a, b)| ≤ kh1:∀ (x : Space d) (t : Time), ‖η (t, x)‖ ≤ k * ‖(1 + ‖t‖) ^ rt‖⁻¹⊢ ∀ (x : Space d), AEStronglyMeasurable (fun a => η (a, x)) volumed:ℕη:𝓢(Time × Space d, ℝ)rt:ℕhrt:Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volumek:ℝhk:2 ^ (rt, 0).1 * ((Finset.Iic (rt, 0)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) η = kh0:∀ (a : Time) (b : Space d), (1 + max ‖a‖ ‖b‖) ^ rt * |η (a, b)| ≤ kh1:∀ (x : Space d) (t : Time), ‖η (t, x)‖ ≤ k * ‖(1 + ‖t‖) ^ rt‖⁻¹⊢ ∀ (x : Space d), ∀ᵐ (a : Time), ‖η (a, x)‖ ≤ k * ‖(1 + ‖a‖) ^ rt‖⁻¹d:ℕη:𝓢(Time × Space d, ℝ)rt:ℕhrt:Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volumek:ℝhk:2 ^ (rt, 0).1 * ((Finset.Iic (rt, 0)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) η = kh0:∀ (a : Time) (b : Space d), (1 + max ‖a‖ ‖b‖) ^ rt * |η (a, b)| ≤ kh1:∀ (x : Space d) (t : Time), ‖η (t, x)‖ ≤ k * ‖(1 + ‖t‖) ^ rt‖⁻¹⊢ Integrable (fun t => k * ‖(1 + ‖t‖) ^ rt‖⁻¹) volumed:ℕη:𝓢(Time × Space d, ℝ)rt:ℕhrt:Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volumek:ℝhk:2 ^ (rt, 0).1 * ((Finset.Iic (rt, 0)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) η = kh0:∀ (a : Time) (b : Space d), (1 + max ‖a‖ ‖b‖) ^ rt * |η (a, b)| ≤ kh1:∀ (x : Space d) (t : Time), ‖η (t, x)‖ ≤ k * ‖(1 + ‖t‖) ^ rt‖⁻¹⊢ ∀ᵐ (a : Time), Continuous fun x => η (a, x)
d:ℕη:𝓢(Time × Space d, ℝ)rt:ℕhrt:Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volumek:ℝhk:2 ^ (rt, 0).1 * ((Finset.Iic (rt, 0)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) η = kh0:∀ (a : Time) (b : Space d), (1 + max ‖a‖ ‖b‖) ^ rt * |η (a, b)| ≤ kh1:∀ (x : Space d) (t : Time), ‖η (t, x)‖ ≤ k * ‖(1 + ‖t‖) ^ rt‖⁻¹⊢ ∀ (x : Space d), AEStronglyMeasurable (fun a => η (a, x)) volume d:ℕη:𝓢(Time × Space d, ℝ)rt:ℕhrt:Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volumek:ℝhk:2 ^ (rt, 0).1 * ((Finset.Iic (rt, 0)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) η = kh0:∀ (a : Time) (b : Space d), (1 + max ‖a‖ ‖b‖) ^ rt * |η (a, b)| ≤ kh1:∀ (x : Space d) (t : Time), ‖η (t, x)‖ ≤ k * ‖(1 + ‖t‖) ^ rt‖⁻¹x:Space d⊢ AEStronglyMeasurable (fun a => η (a, x)) volume
All goals completed! 🐙
d:ℕη:𝓢(Time × Space d, ℝ)rt:ℕhrt:Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volumek:ℝhk:2 ^ (rt, 0).1 * ((Finset.Iic (rt, 0)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) η = kh0:∀ (a : Time) (b : Space d), (1 + max ‖a‖ ‖b‖) ^ rt * |η (a, b)| ≤ kh1:∀ (x : Space d) (t : Time), ‖η (t, x)‖ ≤ k * ‖(1 + ‖t‖) ^ rt‖⁻¹⊢ ∀ (x : Space d), ∀ᵐ (a : Time), ‖η (a, x)‖ ≤ k * ‖(1 + ‖a‖) ^ rt‖⁻¹ d:ℕη:𝓢(Time × Space d, ℝ)rt:ℕhrt:Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volumek:ℝhk:2 ^ (rt, 0).1 * ((Finset.Iic (rt, 0)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) η = kh0:∀ (a : Time) (b : Space d), (1 + max ‖a‖ ‖b‖) ^ rt * |η (a, b)| ≤ kh1:∀ (x : Space d) (t : Time), ‖η (t, x)‖ ≤ k * ‖(1 + ‖t‖) ^ rt‖⁻¹x:Space d⊢ ∀ᵐ (a : Time), ‖η (a, x)‖ ≤ k * ‖(1 + ‖a‖) ^ rt‖⁻¹
d:ℕη:𝓢(Time × Space d, ℝ)rt:ℕhrt:Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volumek:ℝhk:2 ^ (rt, 0).1 * ((Finset.Iic (rt, 0)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) η = kh0:∀ (a : Time) (b : Space d), (1 + max ‖a‖ ‖b‖) ^ rt * |η (a, b)| ≤ kh1:∀ (x : Space d) (t : Time), ‖η (t, x)‖ ≤ k * ‖(1 + ‖t‖) ^ rt‖⁻¹x:Space dt:Time⊢ ‖η (t, x)‖ ≤ k * ‖(1 + ‖t‖) ^ rt‖⁻¹
All goals completed! 🐙
d:ℕη:𝓢(Time × Space d, ℝ)rt:ℕhrt:Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volumek:ℝhk:2 ^ (rt, 0).1 * ((Finset.Iic (rt, 0)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) η = kh0:∀ (a : Time) (b : Space d), (1 + max ‖a‖ ‖b‖) ^ rt * |η (a, b)| ≤ kh1:∀ (x : Space d) (t : Time), ‖η (t, x)‖ ≤ k * ‖(1 + ‖t‖) ^ rt‖⁻¹⊢ Integrable (fun t => k * ‖(1 + ‖t‖) ^ rt‖⁻¹) volume d:ℕη:𝓢(Time × Space d, ℝ)rt:ℕhrt:Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volumek:ℝhk:2 ^ (rt, 0).1 * ((Finset.Iic (rt, 0)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) η = kh0:∀ (a : Time) (b : Space d), (1 + max ‖a‖ ‖b‖) ^ rt * |η (a, b)| ≤ kh1:∀ (x : Space d) (t : Time), ‖η (t, x)‖ ≤ k * ‖(1 + ‖t‖) ^ rt‖⁻¹⊢ Integrable (fun x => ‖(1 + ‖x‖) ^ rt‖⁻¹) volume
All goals completed! 🐙
d:ℕη:𝓢(Time × Space d, ℝ)rt:ℕhrt:Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volumek:ℝhk:2 ^ (rt, 0).1 * ((Finset.Iic (rt, 0)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) η = kh0:∀ (a : Time) (b : Space d), (1 + max ‖a‖ ‖b‖) ^ rt * |η (a, b)| ≤ kh1:∀ (x : Space d) (t : Time), ‖η (t, x)‖ ≤ k * ‖(1 + ‖t‖) ^ rt‖⁻¹⊢ ∀ᵐ (a : Time), Continuous fun x => η (a, x) d:ℕη:𝓢(Time × Space d, ℝ)rt:ℕhrt:Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volumek:ℝhk:2 ^ (rt, 0).1 * ((Finset.Iic (rt, 0)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) η = kh0:∀ (a : Time) (b : Space d), (1 + max ‖a‖ ‖b‖) ^ rt * |η (a, b)| ≤ kh1:∀ (x : Space d) (t : Time), ‖η (t, x)‖ ≤ k * ‖(1 + ‖t‖) ^ rt‖⁻¹t:Time⊢ Continuous fun x => η (t, x)
All goals completed! 🐙A.2. Derivative a function of space