Global weak identities restricted to the half-space cylinder #
Product-coordinate integration by parts for fields supported in a target cylinder gives the corresponding spatial and time weak identities there.
theorem
ESS.bu_spatial_weak_identity_of_global
{Ω : Set CKN.Foundation.Parabolic.Vec3}
{I : Set ℝ}
{K : Set CKN.Foundation.Parabolic.ParabolicPoint}
(hKsub : K ⊆ CKN.spaceTimeSet Ω I)
(f g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ)
(hfzero : ∀ z ∉ K, f z = 0)
(hgzero : ∀ z ∉ K, g z = 0)
(j : Fin 3)
(hglobal :
∀ (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
∫ (q : CKN.Foundation.Parabolic.Vec3 × ℝ), f (CKN.Foundation.Parabolic.parabolicHomeomorph.symm q) * (fderiv ℝ ψ q) (CKN.basisVec j, 0) = -∫ (q : CKN.Foundation.Parabolic.Vec3 × ℝ), g (CKN.Foundation.Parabolic.parabolicHomeomorph.symm q) * ψ q)
(φ : CKN.Foundation.Parabolic.ParabolicPoint → ℝ)
(hφ : φ ∈ CKN.spaceTimeTestFunction Ω I)
:
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Ω I, f z * CKN.spatialPartial φ j z = -∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Ω I, g z * φ z
A global product-coordinate spatial identity restricts to any cylinder containing the supports of its two fields.
theorem
ESS.bu_time_weak_identity_of_global
{Ω : Set CKN.Foundation.Parabolic.Vec3}
{I : Set ℝ}
{K : Set CKN.Foundation.Parabolic.ParabolicPoint}
(hKsub : K ⊆ CKN.spaceTimeSet Ω I)
(f g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ)
(hfzero : ∀ z ∉ K, f z = 0)
(hgzero : ∀ z ∉ K, g z = 0)
(hglobal :
∀ (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
∫ (q : CKN.Foundation.Parabolic.Vec3 × ℝ), f (CKN.Foundation.Parabolic.parabolicHomeomorph.symm q) * (fderiv ℝ ψ q) (0, 1) = -∫ (q : CKN.Foundation.Parabolic.Vec3 × ℝ), g (CKN.Foundation.Parabolic.parabolicHomeomorph.symm q) * ψ q)
(φ : CKN.Foundation.Parabolic.ParabolicPoint → ℝ)
(hφ : φ ∈ CKN.spaceTimeTestFunction Ω I)
:
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Ω I, f z * CKN.timePartial φ z = -∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Ω I, g z * φ z
A global product-coordinate time identity restricts to any cylinder containing the supports of its two fields.