Scalar weak identities on affine time intervals #
Integration by parts transports through the translated interval used in
lem:bu-small-time.
theorem
ESS.bu_affine_weak_identity_interval
(τ scale a b c d : ℝ)
(hscale : 0 < scale)
(hd : d ≠ 0)
(f g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ)
(D : (CKN.Foundation.Parabolic.ParabolicPoint → ℝ) → CKN.Foundation.Parabolic.ParabolicPoint → ℝ)
(hf :
MeasureTheory.AEStronglyMeasurable f
(MeasureTheory.volume.restrict
(CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2}
(Set.Ioo (τ + scale ^ 2 * a) (τ + scale ^ 2 * b)))))
(hg :
MeasureTheory.AEStronglyMeasurable g
(MeasureTheory.volume.restrict
(CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2}
(Set.Ioo (τ + scale ^ 2 * a) (τ + scale ^ 2 * b)))))
(hDcont :
∀
φ ∈
CKN.spaceTimeTestFunction {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2}
(Set.Ioo (τ + scale ^ 2 * a) (τ + scale ^ 2 * b)),
Continuous (D φ))
(hDpull :
∀ ψ ∈ CKN.spaceTimeTestFunction {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo a b),
∀ (z : CKN.Foundation.Parabolic.ParabolicPoint),
D
(have this := ψ ∘ ⇑(buAffineHomeomorph τ scale hscale).symm;
this)
(buAffinePoint τ scale z) = d⁻¹ * D ψ z)
(hsource :
∀
φ ∈
CKN.spaceTimeTestFunction {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2}
(Set.Ioo (τ + scale ^ 2 * a) (τ + scale ^ 2 * b)),
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2}
(Set.Ioo (τ + scale ^ 2 * a) (τ + scale ^ 2 * b)), f z * D φ z = -∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2}
(Set.Ioo (τ + scale ^ 2 * a) (τ + scale ^ 2 * b)), g z * φ z)
(ψ : CKN.Foundation.Parabolic.ParabolicPoint → ℝ)
(hψ : ψ ∈ CKN.spaceTimeTestFunction {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo a b))
:
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo a b), c * f (buAffinePoint τ scale z) * D ψ z = -∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo a b), c * d * g (buAffinePoint τ scale z) * ψ z
A scalar integration-by-parts identity transfers through an affine parabolic change of variables on corresponding time intervals.
theorem
ESS.bu_affine_spatial_weak_identity_interval
(τ scale a b c : ℝ)
(hscale : 0 < scale)
(f g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ)
(j : Fin 3)
(hf :
MeasureTheory.AEStronglyMeasurable f
(MeasureTheory.volume.restrict
(CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2}
(Set.Ioo (τ + scale ^ 2 * a) (τ + scale ^ 2 * b)))))
(hg :
MeasureTheory.AEStronglyMeasurable g
(MeasureTheory.volume.restrict
(CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2}
(Set.Ioo (τ + scale ^ 2 * a) (τ + scale ^ 2 * b)))))
(hsource :
∀
φ ∈
CKN.spaceTimeTestFunction {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2}
(Set.Ioo (τ + scale ^ 2 * a) (τ + scale ^ 2 * b)),
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2}
(Set.Ioo (τ + scale ^ 2 * a) (τ + scale ^ 2 * b)), f z * CKN.spatialPartial φ j z = -∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2}
(Set.Ioo (τ + scale ^ 2 * a) (τ + scale ^ 2 * b)), g z * φ z)
(ψ : CKN.Foundation.Parabolic.ParabolicPoint → ℝ)
(hψ : ψ ∈ CKN.spaceTimeTestFunction {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo a b))
:
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo a b), c * f (buAffinePoint τ scale z) * CKN.spatialPartial ψ j z = -∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo a b), c * scale * g (buAffinePoint τ scale z) * ψ z
The scalar spatial weak derivative identity transfers with one power of the affine spatial scale.
theorem
ESS.bu_affine_time_weak_identity_interval
(τ scale a b c : ℝ)
(hscale : 0 < scale)
(f g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ)
(hf :
MeasureTheory.AEStronglyMeasurable f
(MeasureTheory.volume.restrict
(CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2}
(Set.Ioo (τ + scale ^ 2 * a) (τ + scale ^ 2 * b)))))
(hg :
MeasureTheory.AEStronglyMeasurable g
(MeasureTheory.volume.restrict
(CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2}
(Set.Ioo (τ + scale ^ 2 * a) (τ + scale ^ 2 * b)))))
(hsource :
∀
φ ∈
CKN.spaceTimeTestFunction {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2}
(Set.Ioo (τ + scale ^ 2 * a) (τ + scale ^ 2 * b)),
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2}
(Set.Ioo (τ + scale ^ 2 * a) (τ + scale ^ 2 * b)), f z * CKN.timePartial φ z = -∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2}
(Set.Ioo (τ + scale ^ 2 * a) (τ + scale ^ 2 * b)), g z * φ z)
(ψ : CKN.Foundation.Parabolic.ParabolicPoint → ℝ)
(hψ : ψ ∈ CKN.spaceTimeTestFunction {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo a b))
:
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo a b), c * f (buAffinePoint τ scale z) * CKN.timePartial ψ z = -∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo a b), c * scale ^ 2 * g (buAffinePoint τ scale z) * ψ z
The scalar weak time derivative identity transfers with two powers of the affine spatial scale.