Supports of space-time test functions

The integrability clauses of def:sws are stated on tsupport φ viewed as a subset of the parabolic space-time, while the test-function class CKN.spaceTimeTestFunction states its own support condition on the ordinary product Vec3 × ℝ. The two closed supports are the same set, but they are produced by two different topology instances, so a proof has to move between them explicitly; CKN.tsupport_parabolic_eq is the bridge, and this file packages the consequences that every clause lemma needs:

• the closed support is compact and lies inside the space-time carrier;
• Lebesgue measure restricted to a compact set is finite, which is what turns every exponent-lowering step into an application of Hölder's inequality;
• the first and second spatial derivatives and the time derivative of a test function again have compact support inside that of the test function, are smooth, and are therefore bounded.

Boundedness is the form in which the test function enters: an integrand of def:sws is an integrable field times a bounded factor coming from the test function.

Moving compactness between the parabolic and the product topology

theorem CKN.isCompact_prod_of_isCompact_parabolic {K : Set Foundation.Parabolic.ParabolicPoint} (hK : IsCompact K) : IsCompact (have this := K; this)

A parabolically compact set is compact for the product topology of the space and time factors: the identity is a homeomorphism between the two.

theorem CKN.isCompact_tsupport_parabolic {V : Type} [Zero V] {ψ : Foundation.Parabolic.Vec3 × ℝ → V} (hψc : HasCompactSupport ψ) : IsCompact (tsupport (have this := ψ; this))

The closed support of a compactly supported function on space-time is compact also when read in the parabolic topology, which is the form the integrability clauses of def:sws use.

theorem CKN.tsupport_parabolic_subset_spaceTimeSet {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {ψ : Foundation.Parabolic.Vec3 × ℝ → V} (hψ : ψ ∈ spaceTimeTestFunction Ω I) : tsupport (have this := ψ; this) ⊆ spaceTimeSet Ω I

The parabolic closed support of a space-time test function lies inside the space-time carrier.

theorem CKN.isFiniteMeasure_restrict_of_isCompact {K : Set Foundation.Parabolic.ParabolicPoint} (hK : IsCompact K) : MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict K)

Lebesgue measure restricted to a compact space-time set is a finite measure. Every use of Hölder's inequality below rests on this.

Supports of the derivatives of a test function

theorem CKN.tsupport_timePartial_subset (ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ) : (tsupport fun (z : Foundation.Parabolic.Vec3 × ℝ) => timePartial ψ z) ⊆ tsupport ψ

The closed support of a time derivative lies in that of the function.

theorem CKN.spatialSecondPartial_eq_zero_off_tsupport {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} {z : Foundation.Parabolic.Vec3 × ℝ} (hz : z ∉ tsupport ψ) (i j : Fin 3) : spatialSecondPartial ψ i j z = 0

A second spatial derivative vanishes off the closed support.

theorem CKN.tsupport_spatialSecondPartial_subset (ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ) (i j : Fin 3) : (tsupport fun (z : Foundation.Parabolic.Vec3 × ℝ) => spatialSecondPartial ψ i j z) ⊆ tsupport ψ

The closed support of a second spatial derivative lies in that of the function.

theorem CKN.hasCompactSupport_spatialPartial {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψc : HasCompactSupport ψ) (i : Fin 3) : HasCompactSupport fun (z : Foundation.Parabolic.Vec3 × ℝ) => spatialPartial ψ i z

A spatial derivative of a compactly supported function is compactly supported.

theorem CKN.hasCompactSupport_timePartial {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψc : HasCompactSupport ψ) : HasCompactSupport fun (z : Foundation.Parabolic.Vec3 × ℝ) => timePartial ψ z

The time derivative of a compactly supported function is compactly supported.

theorem CKN.hasCompactSupport_spatialSecondPartial {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψc : HasCompactSupport ψ) (i j : Fin 3) : HasCompactSupport fun (z : Foundation.Parabolic.Vec3 × ℝ) => spatialSecondPartial ψ i j z

A second spatial derivative of a compactly supported function is compactly supported.

Smoothness of the time derivative

theorem CKN.contDiff_timePartial {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) : ContDiff ℝ ↑⊤ fun (z : Foundation.Parabolic.Vec3 × ℝ) => timePartial (have this := ψ; this) z

The time derivative of a smooth function on space-time is smooth. This is the time analogue of CKN.spatialPartial_contDiff.

Bounds on a test function and its derivatives

theorem CKN.exists_bound_of_mem_spaceTimeTestFunction {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ψ ∈ spaceTimeTestFunction Ω I) : ∃ (C : ℝ), ∀ (z : Foundation.Parabolic.Vec3 × ℝ), ‖ψ z‖ ≤ C

A space-time test function is bounded.

theorem CKN.exists_bound_spatialPartial_of_mem_spaceTimeTestFunction {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ψ ∈ spaceTimeTestFunction Ω I) (i : Fin 3) : ∃ (C : ℝ), ∀ (z : Foundation.Parabolic.Vec3 × ℝ), ‖spatialPartial ψ i z‖ ≤ C

Each spatial derivative of a space-time test function is bounded.

theorem CKN.exists_bound_timePartial_of_mem_spaceTimeTestFunction {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ψ ∈ spaceTimeTestFunction Ω I) : ∃ (C : ℝ), ∀ (z : Foundation.Parabolic.Vec3 × ℝ), ‖timePartial ψ z‖ ≤ C

The time derivative of a space-time test function is bounded.

theorem CKN.exists_bound_spatialSecondPartial_of_mem_spaceTimeTestFunction {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ψ ∈ spaceTimeTestFunction Ω I) (i j : Fin 3) : ∃ (C : ℝ), ∀ (z : Foundation.Parabolic.Vec3 × ℝ), ‖spatialSecondPartial ψ i j z‖ ≤ C

Each second spatial derivative of a space-time test function is bounded.