Weak derivatives in affine parabolic coordinates #
Integration by parts transfers through the affine coordinates used in
lem:bu-iterate.
The affine map as a homeomorphism of parabolic space-time.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The parabolic affine homeomorphism acts by the prescribed coordinate formula.
theorem
ESS.bu_affine_locallyIntegrableOn
{E : Type u_1}
[NormedAddCommGroup E]
(τ scale : ℝ)
(hscale : 0 < scale)
(f : CKN.Foundation.Parabolic.ParabolicPoint → E)
(hf :
MeasureTheory.LocallyIntegrableOn f
(CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo τ (τ + scale ^ 2))) MeasureTheory.volume)
:
MeasureTheory.LocallyIntegrableOn (f ∘ buAffinePoint τ scale)
(CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo 0 1)) MeasureTheory.volume
Local integrability transfers through the affine homeomorphism of a positive half-space time slab.
theorem
ESS.bu_affine_weak_identity
(τ scale 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)))))
(hg :
MeasureTheory.AEStronglyMeasurable g
(MeasureTheory.volume.restrict
(CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo τ (τ + scale ^ 2)))))
(hDcont :
∀ φ ∈ CKN.spaceTimeTestFunction {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo τ (τ + scale ^ 2)),
Continuous (D φ))
(hDpull :
∀ ψ ∈ CKN.spaceTimeTestFunction {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo 0 1),
∀ (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)),
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo τ (τ + scale ^ 2)), f z * D φ z = -∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo τ (τ + scale ^ 2)), g z * φ z)
(ψ : CKN.Foundation.Parabolic.ParabolicPoint → ℝ)
(hψ : ψ ∈ CKN.spaceTimeTestFunction {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo 0 1))
:
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo 0 1), 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 0 1), c * d * g (buAffinePoint τ scale z) * ψ z
A scalar integration-by-parts identity transfers through affine parabolic coordinates when the test derivative has its chain-rule factor.
theorem
ESS.bu_affine_spatial_weak_identity
(τ scale 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)))))
(hg :
MeasureTheory.AEStronglyMeasurable g
(MeasureTheory.volume.restrict
(CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo τ (τ + scale ^ 2)))))
(hsource :
∀ φ ∈ CKN.spaceTimeTestFunction {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo τ (τ + scale ^ 2)),
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo τ (τ + scale ^ 2)), 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)), g z * φ z)
(ψ : CKN.Foundation.Parabolic.ParabolicPoint → ℝ)
(hψ : ψ ∈ CKN.spaceTimeTestFunction {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo 0 1))
:
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo 0 1), 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 0 1), 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
(τ scale 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)))))
(hg :
MeasureTheory.AEStronglyMeasurable g
(MeasureTheory.volume.restrict
(CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo τ (τ + scale ^ 2)))))
(hsource :
∀ φ ∈ CKN.spaceTimeTestFunction {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo τ (τ + scale ^ 2)),
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo τ (τ + scale ^ 2)), 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)), g z * φ z)
(ψ : CKN.Foundation.Parabolic.ParabolicPoint → ℝ)
(hψ : ψ ∈ CKN.spaceTimeTestFunction {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo 0 1))
:
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo 0 1), 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 0 1), c * scale ^ 2 * g (buAffinePoint τ scale z) * ψ z
The scalar weak time derivative identity transfers with two powers of the affine spatial scale.
theorem
ESS.bu_affine_weak_derivatives
(τ scale : ℝ)
(hτ : 0 ≤ τ)
(hscale : 0 < scale)
(hupper : τ + scale ^ 2 ≤ 1)
(w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3)
(Dw : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3)
(D2w : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3)
(Dtw : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3)
(hweak : CKN.HasSpaceTimeWeakDerivs {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo 0 1) w Dw D2w Dtw)
:
CKN.HasSpaceTimeWeakDerivs {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo 0 1) (buAffineField τ scale w)
(buAffineDw τ scale Dw) (buAffineD2w τ scale D2w) (buAffineDtw τ scale Dtw)
Weak spatial and time derivatives transfer to the normalized half-space cylinder under an affine parabolic change of variables.